Commit 2025-05-13 14:46 f9166867

View on Github →

chore(CategoryTheory): make MorphismProperty.IsStableUnderColimitsOfShape a class (#24773)

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean

deleted theorem CategoryTheory.MorphismProperty.isStableUnderColimitsOfShape_monomorphisms

Modified Mathlib/CategoryTheory/Localization/FiniteProducts.lean

Modified Mathlib/CategoryTheory/MorphismProperty/FunctorCategory.lean

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.functorCategory

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.functorCategory

Modified Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

deleted theorem CategoryTheory.MorphismProperty.llp_isStableUnderCoproductsOfShape

deleted theorem CategoryTheory.MorphismProperty.rlp_isStableUnderProductsOfShape

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.colimMap

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.colimitsOfShape_le

deleted def CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.limMap

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.limitsOfShape_le

deleted def CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape

added theorem CategoryTheory.MorphismProperty.colimitsOfShape.mk'

added theorem CategoryTheory.MorphismProperty.colimitsOfShape_le

deleted theorem CategoryTheory.MorphismProperty.isStableUnderCoproductsOfShape_of_isStableUnderCoproducts

deleted theorem CategoryTheory.MorphismProperty.isStableUnderCoproductsOfShape_of_isStableUnderFiniteCoproducts

deleted theorem CategoryTheory.MorphismProperty.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts

added theorem CategoryTheory.MorphismProperty.limitsOfShape.mk'

added theorem CategoryTheory.MorphismProperty.limitsOfShape_le

Modified Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean