Commit 2026-02-04 20:33 89d836ac

View on Github →

feat(CategoryTheory): Being equifibered is closed under limits (#34694)

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.Over.mkIdTerminal_from_left

added theorem CategoryTheory.Under.mkIdInitial_to_right

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

added theorem CategoryTheory.NatTrans.Coequifibered.of_isIso

modified def CategoryTheory.NatTrans.Coequifibered

deleted theorem CategoryTheory.NatTrans.Coequifibered_of_isIso

added theorem CategoryTheory.NatTrans.Equifibered.of_isIso

modified def CategoryTheory.NatTrans.Equifibered

added theorem CategoryTheory.NatTrans.coequifibered_op_iff

added theorem CategoryTheory.NatTrans.coequifibered_unop_iff

deleted theorem CategoryTheory.NatTrans.equifibered_of_isIso

added theorem CategoryTheory.NatTrans.equifibered_op_iff

added theorem CategoryTheory.NatTrans.equifibered_unop_iff

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/EquifiberedLimits.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/ObjectProperty/ColimitsOfShape.lean

added theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_inverseImage_iff

Modified Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean

added theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff