English
Equality between I.rlp.llp and retracts of transfinite compositions of pushouts and coproducts holds, establishing an equivalence of these two perspectives under the cardinal regularity assumption.
Русский
Согласованность между двумя подходами к llp: I.rlp.llp и редактируемые трансфинитные композиции; эквивалентность выполняется при условии регулярности кардинала.
LaTeX
$$I.rlp.llp = (transfiniteCompositionsOfShape (coproducts I).pushouts κ.ord.toType).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 shape `κ.ord.toType`) of pushouts of coproducts
of maps in `I`. -/
theorem llp_rlp_of_isCardinalForSmallObjectArgument' :
I.rlp.llp = (transfiniteCompositionsOfShape (coproducts.{w} I).pushouts κ.ord.toType).retracts :=
by
refine le_antisymm ?_ (retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp I κ.ord.toType)
intro X Y f hf
have sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 _) := ⟨by simp⟩
have := hf _ (rlp_πObj I κ f)
refine ⟨_, _, _, ?_, transfiniteCompositionsOfShape_ιObj I κ f⟩
exact
{ i := Arrow.homMk (𝟙 _) sq.lift
r := Arrow.homMk (𝟙 _) (πObj I κ f) }
