llp_rlp_of_isCardinalForSmallObjectArgument

English

The same cardinal-for-small-object-argument assumptions yield the same equality between llp and the retracts of transfinite compositions of pushouts of coproducts of maps in I.

Русский

При тех же допущениях равенство llp и retracts транфинитных композиций pushouts coproducts отображений из I сохраняется.

LaTeX

$$$I.rlp.llp = (\\text{transfiniteCompositions}(\\text{coproducts } I).pushouts).retracts$$$

Lean4

/-- If `κ` is a suitable cardinal for the small object argument for `I : MorphismProperty C`,
then the class `I.rlp.llp` is exactly the class of morphisms that are retracts
of transfinite compositions of pushouts of coproducts of maps in `I`. -/
theorem llp_rlp_of_isCardinalForSmallObjectArgument :
    I.rlp.llp = (transfiniteCompositions.{w} (coproducts.{w} I).pushouts).retracts :=
  by
  refine le_antisymm ?_ (retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp I)
  rw [llp_rlp_of_isCardinalForSmallObjectArgument' I κ]
  apply retracts_monotone
  apply transfiniteCompositionsOfShape_le_transfiniteCompositions

Похожие утверждения