English
If Φ.IsRightDerivabilityStructure, then TwoSquare.GuitartExact ((Φ.catCommSq L₁ L₂).iso).hom.
Русский
Если Φ обладает правой деривируемостью, то соответствующий изоморфизм даёт точность Гитурата.
LaTeX
$$$[\Phi.IsRightDerivabilityStructure] \Rightarrow TwoSquare.GuitartExact\big((\Phi.catCommSq L_1 L_2).iso\big).hom$$$
Lean4
theorem hasRightResolutions_arrow_of_functorial_resolutions : Φ.arrow.HasRightResolutions := fun f ↦
⟨{ X₁ := Arrow.mk (ρ.map f.hom)
w := Arrow.homMk (i.app _) (i.app _) (i.naturality f.hom).symm
hw := ⟨hi _, hi _⟩ }⟩
