Commit 2024-02-09 20:27 1d066860

View on Github →

feat(CategoryTheory/Limits): pushouts in the category of sets (#9992) This PR studies pushouts in the category of types. Specific properties of the pushout when one of the morphisms is injective are obtained. This PR partly removes the reference to the issue https://github.com/leanprover-community/mathlib4/issues/5752 : the HasPushouts (Type _) instance can now be found automatically, but not HasPullbacks.

Estimated changes

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

added def CategoryTheory.Limits.Types.Pushout'

added theorem CategoryTheory.Limits.Types.Pushout.Rel'.symm

added inductive CategoryTheory.Limits.Types.Pushout.Rel'

added inductive CategoryTheory.Limits.Types.Pushout.Rel

added def CategoryTheory.Limits.Types.Pushout.cocone

added theorem CategoryTheory.Limits.Types.Pushout.condition

added def CategoryTheory.Limits.Types.Pushout.equivPushout'

added theorem CategoryTheory.Limits.Types.Pushout.equivalence_rel'

added def CategoryTheory.Limits.Types.Pushout.inl

added theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff

added theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff

added theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff

added def CategoryTheory.Limits.Types.Pushout.inr

added theorem CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff

added def CategoryTheory.Limits.Types.Pushout.isColimitCocone

added theorem CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff

added def CategoryTheory.Limits.Types.Pushout

added theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit

added theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso

added theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso