English
If the small object argument holds, then LLP against RLP with I equals retracts of transfinite compositions of pushouts of coproducts of arrows in C.
Русский
Если выполняется малый объектный аргумент, то LLP против RLP относительно I совпадает с retract-обобщениями трансфинитной композиции пушаутов coproducts стрел в C.
LaTeX
$$$ I.rlp.llp = (transfiniteCompositions.{w} (coproducts.{w} I).pushouts).retracts $$$
Lean4
@[reassoc]
theorem ι_functorMapTgt (i : I) (t : A i ⟶ X) (b : B i ⟶ S) (w : t ≫ πX = f i ≫ b) (b' : B i ⟶ T)
(hb' : b ≫ τ.right = b') (t' : A i ⟶ Y) (ht' : t ≫ τ.left = t') :
Sigma.ι _ (FunctorObjIndex.mk i t b w) ≫ functorMapTgt f τ =
Sigma.ι (functorObjTgtFamily f πY)
(FunctorObjIndex.mk i t' b'
(by
have := τ.w
dsimp at this
rw [← hb', ← reassoc_of% w, ← ht', assoc, this])) :=
by
subst hb' ht'
simp [functorMapTgt]
