Commit 2025-09-30 18:42 77be2401

View on Github →

chore(CategoryTheory/Limits): generalise from Over to CostructuredArrow (#30074) We generalise the limit results for connected categories from Over to CostructuredArrow. Also the naming is adapted to the naming convention. From Proetale.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean

added def CategoryTheory.CostructuredArrow.CreatesConnected.isLimitRaiseCone

added theorem CategoryTheory.CostructuredArrow.CreatesConnected.mapCone_raiseCone

added def CategoryTheory.CostructuredArrow.CreatesConnected.natTransInCostructuredArrow

added def CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone

added def CategoryTheory.CostructuredArrow.Over.conePost

added def CategoryTheory.CostructuredArrow.Over.conePostIso

added def CategoryTheory.CostructuredArrow.Over.isLimitConePost

deleted def CategoryTheory.Over.CreatesConnected.natTransInOver

deleted def CategoryTheory.Over.CreatesConnected.raiseCone

deleted def CategoryTheory.Over.CreatesConnected.raisedConeIsLimit

deleted theorem CategoryTheory.Over.CreatesConnected.raised_cone_lowers_to_original

deleted def CategoryTheory.Over.conePost

deleted def CategoryTheory.Over.conePostIso

deleted def CategoryTheory.Over.isLimitConePost