Commit 2025-04-02 15:28 541c95f6

View on Github →

chore(CategoryTheory/Limits): split Types.lean (#23346) The file CategoryTheory.Limits.Types is split in several files Limits, Colimits, Images, Yoneda. The file Limits.TypesFiltered is moved to Limits.Types.Filtered, and Limits.Shapes.Types is moved to Limits.Types.Shapes. This prepares for a refactor of colimits of types following #23339.

Estimated changes

Modified Mathlib.lean

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

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

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

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

Modified Mathlib/CategoryTheory/Category/Cat/Limit.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Filtered/Final.lean

Modified Mathlib/CategoryTheory/Filtered/OfColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/Limits/ColimitLimit.lean

Modified Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Elements.lean

Modified Mathlib/CategoryTheory/Limits/Filtered.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Limits/FintypeCat.lean

Modified Mathlib/CategoryTheory/Limits/FunctorToTypes.lean

Modified Mathlib/CategoryTheory/Limits/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/Pi.lean

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

Modified Mathlib/CategoryTheory/Limits/Set.lean

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

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

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

Deleted Mathlib/CategoryTheory/Limits/Types.lean

deleted theorem CategoryTheory.Limits.Types.Colimit.w_apply'

deleted theorem CategoryTheory.Limits.Types.Colimit.w_apply

deleted theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply'

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

deleted theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply'

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

deleted theorem CategoryTheory.Limits.Types.Image.lift_fac

deleted def CategoryTheory.Limits.Types.Image.ι

deleted def CategoryTheory.Limits.Types.Image

deleted theorem CategoryTheory.Limits.Types.Limit.lift_π_apply'

deleted theorem CategoryTheory.Limits.Types.Limit.lift_π_apply

deleted theorem CategoryTheory.Limits.Types.Limit.map_π_apply'

deleted theorem CategoryTheory.Limits.Types.Limit.map_π_apply

deleted theorem CategoryTheory.Limits.Types.Limit.w_apply'

deleted theorem CategoryTheory.Limits.Types.Limit.w_apply

deleted theorem CategoryTheory.Limits.Types.Limit.π_mk

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 theorem CategoryTheory.Limits.Types.Small.limitCone_pt_ext

deleted def CategoryTheory.Limits.Types.TypeMax.colimitCocone

deleted def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit

deleted theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply

deleted theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply

deleted theorem CategoryTheory.Limits.Types.colimit_eq

deleted theorem CategoryTheory.Limits.Types.colimit_sound'

deleted theorem CategoryTheory.Limits.Types.colimit_sound

deleted def CategoryTheory.Limits.Types.coneOfSection

deleted theorem CategoryTheory.Limits.Types.hasColimit_iff_small_quot

deleted theorem CategoryTheory.Limits.Types.hasLimit_iff_small_sections

deleted theorem CategoryTheory.Limits.Types.isColimit_iff_bijective_desc

deleted theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply

deleted theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply

deleted theorem CategoryTheory.Limits.Types.isLimit_iff

deleted theorem CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone

deleted theorem CategoryTheory.Limits.Types.jointly_surjective'

deleted theorem CategoryTheory.Limits.Types.jointly_surjective

deleted theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit

deleted theorem CategoryTheory.Limits.Types.limitEquivSections_apply

deleted theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply

deleted theorem CategoryTheory.Limits.Types.limit_ext'

deleted theorem CategoryTheory.Limits.Types.limit_ext

deleted theorem CategoryTheory.Limits.Types.limit_ext_iff'

deleted def CategoryTheory.Limits.Types.monoFactorisation

deleted theorem CategoryTheory.Limits.Types.nonempty_of_nonempty_colimit

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_ι

deleted def CategoryTheory.Limits.Types.sectionOfCone

deleted theorem CategoryTheory.Limits.Types.small_quot_of_hasColimit

deleted theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map

deleted theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux

deleted def CategoryTheory.Limits.Types.toCocone

deleted def CategoryTheory.Limits.compCoyonedaSectionsEquiv

deleted def CategoryTheory.Limits.compYonedaSectionsEquiv

deleted def CategoryTheory.Limits.opCompYonedaSectionsEquiv

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

added theorem CategoryTheory.Limits.Types.Colimit.w_apply'

added theorem CategoryTheory.Limits.Types.Colimit.w_apply

added theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply'

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

added theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply'

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

added 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_quotQuotUliftEquiv

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

added def CategoryTheory.Limits.Types.Quot

added def CategoryTheory.Limits.Types.TypeMax.colimitCocone

added def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit

added theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply

added theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply

added theorem CategoryTheory.Limits.Types.colimit_eq

added theorem CategoryTheory.Limits.Types.colimit_sound'

added 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.jointly_surjective'

added theorem CategoryTheory.Limits.Types.jointly_surjective

added theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit

added theorem CategoryTheory.Limits.Types.nonempty_of_nonempty_colimit

added def CategoryTheory.Limits.Types.quotQuotUliftEquiv

added def CategoryTheory.Limits.Types.quotToQuotUlift

added theorem CategoryTheory.Limits.Types.quotToQuotUlift_ι

added def CategoryTheory.Limits.Types.quotUliftToQuot

added theorem CategoryTheory.Limits.Types.quotUliftToQuot_ι

added theorem CategoryTheory.Limits.Types.small_quot_of_hasColimit

added def CategoryTheory.Limits.Types.toCocone

Renamed Mathlib/CategoryTheory/Limits/TypesFiltered.lean to Mathlib/CategoryTheory/Limits/Types/Filtered.lean

Created Mathlib/CategoryTheory/Limits/Types/Images.lean

added theorem CategoryTheory.Limits.Types.Image.lift_fac

added def CategoryTheory.Limits.Types.Image.ι

added def CategoryTheory.Limits.Types.Image

added def CategoryTheory.Limits.Types.monoFactorisation

added theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map

added theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux

Created Mathlib/CategoryTheory/Limits/Types/Limits.lean

added theorem CategoryTheory.Limits.Types.Limit.lift_π_apply'

added theorem CategoryTheory.Limits.Types.Limit.lift_π_apply

added theorem CategoryTheory.Limits.Types.Limit.map_π_apply'

added theorem CategoryTheory.Limits.Types.Limit.map_π_apply

added theorem CategoryTheory.Limits.Types.Limit.w_apply'

added theorem CategoryTheory.Limits.Types.Limit.w_apply

added theorem CategoryTheory.Limits.Types.Limit.π_mk

added theorem CategoryTheory.Limits.Types.Small.limitCone_pt_ext

added def CategoryTheory.Limits.Types.coneOfSection

added theorem CategoryTheory.Limits.Types.hasLimit_iff_small_sections

added theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply

added theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply

added theorem CategoryTheory.Limits.Types.isLimit_iff

added theorem CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone

added theorem CategoryTheory.Limits.Types.limitEquivSections_apply

added theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply

added theorem CategoryTheory.Limits.Types.limit_ext'

added theorem CategoryTheory.Limits.Types.limit_ext

added theorem CategoryTheory.Limits.Types.limit_ext_iff'

added def CategoryTheory.Limits.Types.sectionOfCone

Renamed Mathlib/CategoryTheory/Limits/Shapes/Types.lean to Mathlib/CategoryTheory/Limits/Types/Shapes.lean

Created Mathlib/CategoryTheory/Limits/Types/Yoneda.lean

added def CategoryTheory.Limits.compCoyonedaSectionsEquiv

added def CategoryTheory.Limits.compYonedaSectionsEquiv

added def CategoryTheory.Limits.opCompYonedaSectionsEquiv

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

Modified Mathlib/CategoryTheory/Presentable/Limits.lean

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

Modified Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

Modified Mathlib/CategoryTheory/Subpresheaf/Image.lean

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

Modified Mathlib/Topology/Category/TopCat/Yoneda.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean