Commit 2023-03-24 13:33 507eaf9e

View on Github →

feat: port CategoryTheory.Limits.ConcreteCategory (#3023)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

Created Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

added theorem CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq

added theorem CategoryTheory.Limits.Concrete.colimit_exists_rep

added theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists

added theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists

added theorem CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit

added theorem CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq

added theorem CategoryTheory.Limits.Concrete.isColimit_exists_rep

added theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists

added theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists

added theorem CategoryTheory.Limits.Concrete.isLimit_ext

added theorem CategoryTheory.Limits.Concrete.limit_ext

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.to_product_injective_of_isLimit

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

added theorem CategoryTheory.Limits.cokernel_funext