Commit 2024-11-03 13:44 3a51a909

View on Github →

feat(CategoryTheory): Colimits on the Grothendieck construction (#18442) This PR should provide some necessary constructions to use colimits on the Grothendieck construction as a replacement for double colimits with an inner shape that depends on the outer index.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

added theorem CategoryTheory.Grothendieck.eqToHom_eq

added def CategoryTheory.Grothendieck.ιNatTrans

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

added theorem CategoryTheory.Limits.colimit.eqToHom_comp_ι

added theorem CategoryTheory.Limits.limit.π_comp_eqToHom

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

added def CategoryTheory.Limits.coconeFiberwiseColimitOfCocone

added def CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit

added def CategoryTheory.Limits.colimitFiberwiseColimitIso

added def CategoryTheory.Limits.fiberwiseColimit

added theorem CategoryTheory.Limits.hasColimit_fiberwiseColimit

added theorem CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit

added theorem CategoryTheory.Limits.hasColimit_ι_comp

added theorem CategoryTheory.Limits.hasColimitsOfShape_grothendieck

added def CategoryTheory.Limits.isColimitCoconeFiberwiseColimitOfCocone

added def CategoryTheory.Limits.isColimitCoconeOfFiberwiseCocone

added def CategoryTheory.Limits.natTransIntoForgetCompFiberwiseColimit

added theorem CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom

added theorem CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_inv