homologyι_naturality — Mathlib

English

If φ has epi on τ1, iso on τ2, and mono on τ3, then the homology map φ is an isomorphism.

Русский

Если φ имеет эпиморфизм на τ1, изоморфизм на τ2 и моно на τ3, то отображение гомологии φ является изоморфизмом.

LaTeX

$$$\text{epi}(\tau_1) \land \text{IsIso}(\tau_2) \land \text{Mono}(\tau_3) \Rightarrow \mathrm{IsIso}(\mathrm{homologyMap}(\phi))$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyι_naturality (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] :
    homologyMap φ ≫ S₂.homologyι = S₁.homologyι ≫ S₁.opcyclesMap φ :=
  by
  simp only [← cancel_epi S₁.rightHomologyIso.hom, rightHomologyIso_hom_naturality_assoc φ,
    rightHomologyIso_hom_comp_homologyι, rightHomologyι_naturality]
  simp only [homologyι, assoc, Iso.hom_inv_id_assoc]

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