Commit 2025-02-15 13:09 38f496fe

View on Github →

feat(CategoryTheory): cardinals that are suitable for the small object argument (#21865) In this PR, we package the technical assumptions that are needed for the small object argument in a typeclass IsCardinalForSmallObjectArgument I κ where I is a class of morphisms and κ is a suitable regular cardinal. In a follow-up PR, it shall be proved that HasFunctorialFactorization I.rlp.llp I.rlp holds.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/SmallObject/Construction.lean

added theorem CategoryTheory.SmallObject.functorObj_isPushout

added theorem CategoryTheory.SmallObject.ιFunctorObj_extension'

Created Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

added theorem CategoryTheory.SmallObject.hasColimitsOfShape_discrete

added theorem CategoryTheory.SmallObject.hasCoproducts

added theorem CategoryTheory.SmallObject.hasIterationOfShape

added theorem CategoryTheory.SmallObject.hasPushouts

added theorem CategoryTheory.SmallObject.isSmall

added theorem CategoryTheory.SmallObject.locallySmall

added theorem CategoryTheory.SmallObject.preservesColimit

added def CategoryTheory.SmallObject.propArrow

added theorem CategoryTheory.SmallObject.succStruct_prop_le_propArrow

added theorem CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration_F

Modified Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

added def CategoryTheory.SmallObject.SuccStruct.prop.arrowIso

Modified Mathlib/SetTheory/Ordinal/Basic.lean