Commit 2024-10-29 22:45 39a385b5

View on Github →

feat(CategoryTheory/Comma): limit properties of subcategories defined by morphism properties (#18134) We show that under suitable assumptions on P the full subcategory of Over X defined by P has terminal objects and pullbacks.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Comma/Basic.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/Comma.lean

Created Mathlib/CategoryTheory/Limits/MorphismProperty.lean

added theorem CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_discrete_empty

added theorem CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape

added theorem CategoryTheory.MorphismProperty.Comma.hasLimitsOfShape_of_closedUnderLimitsOfShape

added theorem CategoryTheory.MorphismProperty.Over.hasPullbacks

added def CategoryTheory.MorphismProperty.Over.mkIdTerminal

added theorem CategoryTheory.Over.closedUnderLimitsOfShape_discrete_empty

added theorem CategoryTheory.Over.closedUnderLimitsOfShape_pullback

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

added theorem CategoryTheory.IsPullback.of_isLimit_cone

added theorem CategoryTheory.IsPushout.of_isColimit_cocone

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

added theorem CategoryTheory.MorphismProperty.comma_iso_iff

Modified Mathlib/CategoryTheory/MorphismProperty/Comma.lean

added theorem CategoryTheory.MorphismProperty.Comma.Hom.hom_left

added theorem CategoryTheory.MorphismProperty.Comma.Hom.hom_right

added theorem CategoryTheory.MorphismProperty.costructuredArrow_iso_iff

added theorem CategoryTheory.MorphismProperty.over_iso_iff