Commit 2024-03-12 20:09 d73713b9

View on Github →

refactor: generalize universes for colimits in Type (#11148) This is a smaller version of #7020. Before this PR, for limits, we gave instances for small indexing categories, but for colimits, we gave instances for TypeMax. This PR changes so that we give instances for small indexing categories in both cases. This is more general and also more uniform.

Estimated changes

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

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

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

modified def MonCat.FilteredColimits.coconeMorphism

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

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

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

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

Modified Mathlib/CategoryTheory/Limits/Types.lean

modified theorem CategoryTheory.Limits.Types.Colimit.w_apply

modified theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply

modified theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply

modified def CategoryTheory.Limits.Types.Quot.Rel

added def CategoryTheory.Limits.Types.Quot.desc

added theorem CategoryTheory.Limits.Types.Quot.desc_colimitCocone

added theorem CategoryTheory.Limits.Types.Quot.desc_toCocone_desc

added theorem CategoryTheory.Limits.Types.Quot.jointly_surjective

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

added def CategoryTheory.Limits.Types.Quot.ι

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

modified def CategoryTheory.Limits.Types.Quot

added theorem CategoryTheory.Limits.Types.Small.hasLimit_iff_small_sections

modified theorem CategoryTheory.Limits.Types.Small.limitCone_pt_ext

added def CategoryTheory.Limits.Types.TypeMax.colimitCocone

added def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit

deleted def CategoryTheory.Limits.Types.colimitCocone

deleted def CategoryTheory.Limits.Types.colimitCoconeIsColimit

modified theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply

modified theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply

modified theorem CategoryTheory.Limits.Types.colimit_eq

modified theorem CategoryTheory.Limits.Types.colimit_sound'

modified theorem CategoryTheory.Limits.Types.colimit_sound

added theorem CategoryTheory.Limits.Types.hasColimit_iff_small_quot

added theorem CategoryTheory.Limits.Types.isColimit_iff_bijective_desc

added theorem CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone

modified theorem CategoryTheory.Limits.Types.jointly_surjective'

modified theorem CategoryTheory.Limits.Types.jointly_surjective

added def CategoryTheory.Limits.Types.toCocone

Modified Mathlib/CategoryTheory/Types.lean

added theorem CategoryTheory.Functor.sections_ext_iff

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