English
If the small object argument holds for I, then the LLP against RLP with respect to I consists exactly of retracts of transfinite compositions of pushouts of coproducts of arrows in C, indexed by I.smallObjectκ.ord.toType.
Русский
Если выполнен малый объектный аргумент для I, то класc LLP против RLP относительно I совпадает с повторными retract-предметами трансфинитных композициях, образованных из толкований свободных объединений и взятиями пушаутов coproducts стрел в C, индексированных ord типа I.smallObjectκ.
LaTeX
$$$ I.rlp.llp = \left(\text{transfiniteCompositionsOfShape}( \text{coproducts}(I).pushouts\, I.smallObjectκ.ord.toType) \right).retracts $$$
Lean4
/-- If `I : MorphismProperty C` permits the small object argument,
then the class of morphism that have the left lifting property with respect to
the maps that have the right lifting property with respect to `I` are
exactly the retracts of transfinite compositions (indexed by `I.smallObjectκ.ord.toType`)
of pushouts of coproducts of morphisms in `C`. -/
theorem llp_rlp_of_hasSmallObjectArgument' :
I.rlp.llp = (transfiniteCompositionsOfShape (coproducts.{w} I).pushouts I.smallObjectκ.ord.toType).retracts :=
llp_rlp_of_isCardinalForSmallObjectArgument' I I.smallObjectκ
