homologyπ_naturality — Mathlib

English

For φ: S1 → S2, the naturality of homology: homologyπ on S1 followed by homologyMap φ equals cyclesMap φ followed by homologyπ on S2.

Русский

Для φ: S1 → S2 естественность гомологии: homologyπ на S1 затем homologyMap φ равны cyclesMap φ затем homologyπ на S2.

LaTeX

$$$S_1.homologyπ \circ \mathrm{homologyMap}(\phi) = \mathrm{cyclesMap}(\phi) \circ S_2.homologyπ$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyπ_naturality (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] :
    S₁.homologyπ ≫ homologyMap φ = cyclesMap φ ≫ S₂.homologyπ :=
  by
  simp only [← cancel_mono S₂.leftHomologyIso.inv, assoc, ← leftHomologyIso_inv_naturality φ,
    homologyπ_comp_leftHomologyIso_inv]
  simp only [homologyπ, assoc, Iso.hom_inv_id_assoc, leftHomologyπ_naturality]

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