Commit 2025-09-08 19:22 f810beb8

View on Github →

feat(CategoryTheory/Limits): colimit presentations (#29382) Given categories J and C and an object X : C, we add a structure ColimitPresentation J X that contains the data of a diagram with colimit X. Under certain compactness conditions, we show that colimit presentations compose. This will be used to define the ind-closure of an object property.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

added def CategoryTheory.Over.isLimitLiftCone

added def CategoryTheory.Over.liftCone

added def CategoryTheory.Under.isColimitLiftCocone

added def CategoryTheory.Under.liftCocone

Created Mathlib/CategoryTheory/Limits/Presentation.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

added def CategoryTheory.Limits.ColimitPresentation.map

added def CategoryTheory.Limits.ColimitPresentation.ofIso

added def CategoryTheory.Limits.ColimitPresentation.self

added structure CategoryTheory.Limits.ColimitPresentation

Modified Mathlib/CategoryTheory/Presentable/Finite.lean

added theorem CategoryTheory.IsFinitelyPresentable.exists_eq_of_isColimit

added theorem CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit

added theorem CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under