Commit 2025-10-13 07:43 ef523e28

View on Github →

chore(CategoryTheory): split Limits.Presentation (#29903) The part of the code involving "set theory" (via finitely presentable objects) is moved to CategoryTheory.Presentable.ColimitPresentation. As ColimitPresentation is going to be used more widely, this will reduce dependencies to set theory for some files.

depends on: #29851
depends on: #29849
depends on: #29843

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Presentation.lean

deleted def CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp

deleted structure CategoryTheory.Limits.ColimitPresentation.Total.Hom

deleted theorem CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom

deleted def CategoryTheory.Limits.ColimitPresentation.Total

deleted def CategoryTheory.Limits.ColimitPresentation.bind

Modified Mathlib/CategoryTheory/ObjectProperty/Ind.lean

Created Mathlib/CategoryTheory/Presentable/ColimitPresentation.lean

added def CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp

added structure CategoryTheory.Limits.ColimitPresentation.Total.Hom

added theorem CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom

added def CategoryTheory.Limits.ColimitPresentation.Total

added def CategoryTheory.Limits.ColimitPresentation.bind