Commit 2023-11-25 09:44 e9d46c6c

View on Github →

feat(CategoryTheory): description of products and pullbacks in concrete categories (#8507)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/ModuleCat.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

deleted def CategoryTheory.Limits.Concrete.multiequalizerEquivAux

deleted theorem CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply

deleted theorem CategoryTheory.Limits.Concrete.multiequalizer_ext

deleted theorem CategoryTheory.Limits.Concrete.widePullback_ext'

deleted theorem CategoryTheory.Limits.Concrete.widePullback_ext

deleted theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep'

deleted theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep

deleted theorem CategoryTheory.Limits.cokernel_funext

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Created Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

added theorem CategoryTheory.Limits.Concrete.cokernel_funext

added def CategoryTheory.Limits.Concrete.multiequalizerEquivAux

added theorem CategoryTheory.Limits.Concrete.multiequalizerEquiv_apply

added theorem CategoryTheory.Limits.Concrete.multiequalizer_ext

added theorem CategoryTheory.Limits.Concrete.prodEquiv_apply_fst

added theorem CategoryTheory.Limits.Concrete.prodEquiv_apply_snd

added theorem CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_fst

added theorem CategoryTheory.Limits.Concrete.prodEquiv_symm_apply_snd

added theorem CategoryTheory.Limits.Concrete.productEquiv_apply_apply

added theorem CategoryTheory.Limits.Concrete.productEquiv_symm_apply_π

added theorem CategoryTheory.Limits.Concrete.pullbackMk_fst

added theorem CategoryTheory.Limits.Concrete.pullbackMk_snd

added theorem CategoryTheory.Limits.Concrete.pullbackMk_surjective

added theorem CategoryTheory.Limits.Concrete.widePullback_ext'

added theorem CategoryTheory.Limits.Concrete.widePullback_ext

added theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep'

added theorem CategoryTheory.Limits.Concrete.widePushout_exists_rep

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean