Commit 2023-03-11 14:23 07ab9d6a

View on Github →

feat: port CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (#2764)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean

added def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit

added def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit

added def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit

added def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit

added theorem CategoryTheory.Limits.hasColimit_of_coequalizer_and_coproduct

added theorem CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts

added theorem CategoryTheory.Limits.hasFiniteColimits_of_hasInitial_and_pushouts

added theorem CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products

added theorem CategoryTheory.Limits.hasFiniteLimits_of_hasTerminal_and_pullbacks

added theorem CategoryTheory.Limits.hasLimit_of_equalizer_and_product

added theorem CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts

added theorem CategoryTheory.Limits.has_limits_of_hasEqualizers_and_products

Modified Mathlib/CategoryTheory/Limits/Preserves/Finite.lean