isIso_cyclesMap_of_isIso_of_mono'

English

Let φ : S1 → S2 be a morphism of ShortComplexes such that φ.τ₂ is an isomorphism and φ.τ₃ is mono, with S1 and S2 possessing left homology data. Then the cycles map φ is an isomorphism.

Русский

Пусть φ : S1 → S2 — морфизм коротких комплексов, для которого φ.τ₂ является изоморфизмом, а φ.τ₃ — мономоризм, причём у S1 и S2 есть данные левой гомологии. Тогда отображение cyclesMap φ является изоморфизмом.

LaTeX

$$$ (IsIso \phi.\tau_2) \land (Mono \phi.\tau_3) \rightarrow IsIso (cyclesMap \phi) $$$

Lean4

theorem isIso_cyclesMap_of_isIso_of_mono' (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₃ : Mono φ.τ₃) [S₁.HasLeftHomology]
    [S₂.HasLeftHomology] : IsIso (cyclesMap φ) :=
  isIso_cyclesMap'_of_isIso_of_mono φ h₂ h₃ _ _

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