isIso_of_components — Mathlib

English

If a morphism f between two HomologicalComplexes has each component f.f n an isomorphism, then f is an isomorphism of chain complexes: IsIso f.

Русский

Если морфизм f между двумя гомологическими комплексами имеет каждую компоненту f.f n изоморфизмом, то сам морфизм f является изоморфизмом комплекс: IsIso f.

LaTeX

$$$\\forall n,\\ IsIso(f.f n)\\ \\Rightarrow\\ IsIso(f)$$$

Lean4

theorem isIso_of_components (f : C₁ ⟶ C₂) [∀ n : ι, IsIso (f.f n)] : IsIso f :=
  (HomologicalComplex.Hom.isoOfComponents fun n => asIso (f.f n)).isIso_hom

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