cyclesMap_comm — Mathlib

English

For φ: S1⟶S2 with left homologies, cyclesMap φ ≫ h2.cyclesIso.hom = h1.cyclesIso.hom ≫ γ.φK.

Русский

Для φ: S1⟶S2 с левой гомологией, cyclesMap φ следует из равенств циклических изоморфизмов и γ.

LaTeX

$$$cyclesMap\,\varphi \;\circ\; h_{2}.cyclesIso.hom = h_{1}.cyclesIso.hom \circ γ.φK$$$

Lean4

theorem cyclesMap_comm [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    cyclesMap φ ≫ h₂.cyclesIso.hom = h₁.cyclesIso.hom ≫ γ.φK := by
  simp only [γ.cyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]

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