English
Suppose there are arrows φ: S1 → S2 and φ′: S3 → S4 together with an isomorphism between Arrow.mk φ and Arrow.mk φ′, and φ is a quasi-isomorphism. Then φ′ is a quasi-isomorphism.
Русский
Пусть существуют стрелы φ: S1 → S2 и φ′: S3 → S4 и имеется изоморфизм между стрелами Arrow.mk φ и Arrow.mk φ′; если φ — квазиизоморфизм, то φ′ также является квазиизомоморфизм.
LaTeX
$$$\text{If } φ: S_1 \to S_2,\ φ': S_3 \to S_4\text{ and } Arrow.mk φ \cong Arrow.mk φ',\text{ with } φ\text{ a quasi-iso, then } φ'\text{ is a quasi-iso.}$$$
Lean4
theorem quasiIso_of_arrow_mk_iso (φ : S₁ ⟶ S₂) (φ' : S₃ ⟶ S₄) (e : Arrow.mk φ ≅ Arrow.mk φ') [hφ : QuasiIso φ] :
QuasiIso φ' := by
let α : S₃ ⟶ S₁ := e.inv.left
let β : S₂ ⟶ S₄ := e.hom.right
suffices φ' = α ≫ φ ≫ β by
rw [this]
infer_instance
simp only [α, β, Arrow.w_mk_right_assoc, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom, ← Arrow.comp_right,
e.inv_hom_id, Arrow.id_right, comp_id]
