Commit 2025-09-26 06:47 4abe24d7

View on Github →

feat(CategoryTheory): limit presentations (#29849) This PR introduces LimitPresentation which is the dual notion to ColimitPresentation introduced in #29382.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Presentation.lean

added def CategoryTheory.Limits.ColimitPresentation.changeDiag

added theorem CategoryTheory.Limits.ColimitPresentation.hasColimit

added def CategoryTheory.Limits.LimitPresentation.changeDiag

added theorem CategoryTheory.Limits.LimitPresentation.hasLimit

added def CategoryTheory.Limits.LimitPresentation.map

added def CategoryTheory.Limits.LimitPresentation.ofIso

added def CategoryTheory.Limits.LimitPresentation.reindex

added def CategoryTheory.Limits.LimitPresentation.self

added structure CategoryTheory.Limits.LimitPresentation