Commit 2025-07-09 00:31 25043da6

View on Github →

refactor(CategoryTheory/Limits): colimits in Type (#25823) Colimits in Type are refactored so as to relate them with the non categorical constructions introduced in #23339.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Basic.lean

added def CommGrp.fullyFaithfulForget₂ToGrp

added def Grp.fullyFaithfulForget₂ToMonCat

Modified Mathlib/Algebra/Category/Grp/FilteredColimits.lean

added theorem Grp.FilteredColimits.colimit_mul_mk_eq'

added theorem Grp.FilteredColimits.colimit_mul_mk_eq

added theorem Grp.FilteredColimits.colimit_one_eq

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

added def ModuleCat.FilteredColimits.M.mk

added theorem ModuleCat.FilteredColimits.M.mk_map

added theorem ModuleCat.FilteredColimits.M.mk_surjective

added def ModuleCat.FilteredColimits.M

added theorem ModuleCat.FilteredColimits.colimit_add_mk_eq'

added theorem ModuleCat.FilteredColimits.colimit_add_mk_eq

added theorem ModuleCat.FilteredColimits.colimit_zero_eq

added theorem ModuleCat.FilteredColimits.ι_colimitDesc

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

added def CommMonCat.fullyFaithfulForgetToMonCat

Modified Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

added theorem MonCat.FilteredColimits.M.map_mk

added theorem MonCat.FilteredColimits.M.mk_surjective

added theorem MonCat.FilteredColimits.colimit_mul_mk_eq'

Modified Mathlib/Algebra/Category/Ring/Basic.lean

added def CommRingCat.fullyFaithfulForget₂ToRingCat

added def CommSemiRingCat.fullyFaithfulForget₂ToSemiRingCat

added def RingCat.fullyFaithfulForget₂ToSemiRingCat

Modified Mathlib/Algebra/Category/Ring/FilteredColimits.lean

modified def CommRingCat.FilteredColimits.colimitCoconeIsColimit

modified def CommSemiRingCat.FilteredColimits.colimitCoconeIsColimit

modified def RingCat.FilteredColimits.colimitCoconeIsColimit

added def SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom

added theorem SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk

added def SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom

added theorem SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_apply_eq

added theorem SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk

Modified Mathlib/CategoryTheory/Limits/Final.lean

added theorem CategoryTheory.Functor.Final.zigzag_of_eqvGen_colimitTypeRel

deleted theorem CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel

Modified Mathlib/CategoryTheory/Limits/FintypeCat.lean

added theorem CategoryTheory.Limits.FintypeCat.finite_of_isColimit

Modified Mathlib/CategoryTheory/Limits/IsConnected.lean

added theorem CategoryTheory.Limits.Types.zigzag_of_eqvGen_colimitTypeRel

deleted theorem CategoryTheory.Limits.Types.zigzag_of_eqvGen_quot_rel

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

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

deleted theorem CategoryTheory.Limits.SingleObj.Types.Quot.Rel.iff_orbitRel

deleted def CategoryTheory.Limits.SingleObj.Types.Quot.equivOrbitRelQuotient

added def CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient

added theorem CategoryTheory.Limits.SingleObj.colimitTypeRel_iff_orbitRel

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

added theorem CategoryTheory.Functor.CoconeTypes.IsColimit.precompose

added def CategoryTheory.Functor.CoconeTypes.IsColimitCore.precompose

added theorem CategoryTheory.Functor.CoconeTypes.isColimit_precompose_iff

added def CategoryTheory.Functor.CoconeTypes.precompose

added theorem CategoryTheory.Functor.ιColimitType_eq_iff

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

added theorem CategoryTheory.Functor.CoconeTypes.isColimit_iff

added def CategoryTheory.Functor.coconeTypesEquiv

deleted def CategoryTheory.Limits.Types.Quot.Rel

deleted def CategoryTheory.Limits.Types.Quot.desc

deleted theorem CategoryTheory.Limits.Types.Quot.desc_colimitCocone

deleted theorem CategoryTheory.Limits.Types.Quot.desc_quotQuotUliftEquiv

deleted theorem CategoryTheory.Limits.Types.Quot.desc_toCocone_desc

deleted theorem CategoryTheory.Limits.Types.Quot.jointly_surjective

deleted theorem CategoryTheory.Limits.Types.Quot.map_ι

deleted def CategoryTheory.Limits.Types.Quot.ι

deleted theorem CategoryTheory.Limits.Types.Quot.ι_desc

deleted def CategoryTheory.Limits.Types.Quot

deleted def CategoryTheory.Limits.Types.TypeMax.colimitCocone

deleted def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit

added theorem CategoryTheory.Limits.Types.colimitEquivColimitType_apply

added theorem CategoryTheory.Limits.Types.colimitEquivColimitType_symm_apply

deleted theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply

deleted theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply

added theorem CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType

deleted theorem CategoryTheory.Limits.Types.hasColimit_iff_small_quot

deleted theorem CategoryTheory.Limits.Types.isColimit_iff_bijective_desc

added theorem CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit

deleted def CategoryTheory.Limits.Types.quotQuotUliftEquiv

deleted def CategoryTheory.Limits.Types.quotToQuotUlift

deleted theorem CategoryTheory.Limits.Types.quotToQuotUlift_ι

deleted def CategoryTheory.Limits.Types.quotUliftToQuot

deleted theorem CategoryTheory.Limits.Types.quotUliftToQuot_ι

added theorem CategoryTheory.Limits.Types.small_colimitType_of_hasColimit

deleted theorem CategoryTheory.Limits.Types.small_quot_of_hasColimit

deleted def CategoryTheory.Limits.Types.toCocone

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

added theorem CategoryTheory.Limits.Types.FilteredColimit.eqvGen_colimitTypeRel_of_rel

deleted theorem CategoryTheory.Limits.Types.FilteredColimit.eqvGen_quot_rel_of_rel

added theorem CategoryTheory.Limits.Types.FilteredColimit.rel_of_colimitTypeRel

deleted theorem CategoryTheory.Limits.Types.FilteredColimit.rel_of_quot_rel

Modified Mathlib/CategoryTheory/Types.lean

added theorem CategoryTheory.FunctorToTypes.naturality_symm

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

added theorem TopCat.hasColimit_iff_small_colimitType

deleted theorem TopCat.hasColimit_iff_small_quot