of_iso — Mathlib

English

If F1 is homological and F1 is isomorphic to F2, then F2 is homological.

Русский

Если F1 гомологичен и F1 изоморфен F2, то F2 также гомологичен.

LaTeX

$$$F_1\text{ is Homological} \wedge F_1 \cong F_2 \Rightarrow F_2 \text{ is Homological}$$$

Lean4

theorem of_iso {F₁ F₂ : C ⥤ A} [F₁.IsHomological] (e : F₁ ≅ F₂) : F₂.IsHomological :=
  have := preservesZeroMorphisms_of_iso e
  ⟨fun T hT => ShortComplex.exact_of_iso (ShortComplex.mapNatIso _ e) (F₁.map_distinguished_exact T hT)⟩

Похожие утверждения