Commit 2023-03-08 06:41 a223779f

View on Github →

feat: port CategoryTheory.Limits.Constructions.Equalizers (#2700)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone

added def CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit

added def CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer

added theorem CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr

added def CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer

added def CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone

added def CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerConeIsLimit

added theorem CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd

added theorem CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts

added theorem CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products

added def CategoryTheory.Limits.preservesCoequalizersOfPreservesPushoutsAndBinaryCoproducts

added def CategoryTheory.Limits.preservesEqualizersOfPreservesPullbacksAndBinaryProducts

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

added theorem CategoryTheory.Limits.hasPullback_of_preservesPullback

deleted theorem CategoryTheory.Limits.hasPullback_of_preserves_pullback

added theorem CategoryTheory.Limits.hasPushout_of_preservesPushout

deleted theorem CategoryTheory.Limits.hasPushout_of_preserves_pushout