English
Under the small object-argument assumptions, the class I.rlp.llp is precisely the class of retracts of transfinite compositions of pushouts of coproducts of maps in I.
Русский
При предположениях малого объектного аргумента класс I.rlp.llp точно равен классу склонений к простым предельным композициям пушаутов coproducts картиновых отображений из I.
LaTeX
$$$I.RLP\\;\\mathrm{llp} = (\\mathrm{transfiniteCompositions}\\{\\mathrm{pushouts}\\(\\mathrm{coproducts}\\; I\\)\\}).\\mathrm{retracts}$$$
Lean4
@[reassoc (attr := simp)]
theorem πObj_naturality {f g : Arrow C} (φ : f ⟶ g) : objMap I κ φ ≫ πObj I κ g.hom = πObj I κ f.hom ≫ φ.right :=
by
let e₁ := asIso ((ιIteration I κ).app (Arrow.mk f.hom)).right
let e₂ := asIso ((ιIteration I κ).app (Arrow.mk g.hom)).right
change _ ≫ _ ≫ e₂.inv = (_ ≫ e₁.inv) ≫ _
have h₁ := ((iteration I κ).map φ).w =≫ e₂.inv
have h₂ : φ.right ≫ e₂.hom = e₁.hom ≫ ((iteration I κ).map φ).right :=
((Functor.whiskerRight (ιIteration I κ) Arrow.rightFunc).naturality φ)
dsimp at h₁
rw [assoc] at h₁
apply h₁.trans
simp only [← cancel_mono e₂.hom, assoc, e₂.inv_hom_id, h₂, e₁.inv_hom_id_assoc]
rw [← assoc]
apply comp_id
