rightHomologyMap_comm — Mathlib

English

For φ: S1 ⟶ S2 with right homology, opcyclesMap φ equals h1.opcyclesIso.hom ≫ γ.φQ ≫ h2.opcyclesIso.inv.

Русский

Пусть φ: S1 ⟶ S2 имеет правую гомологию; opcyclesMap φ = h1.opcyclesIso.hom ≫ γ.φQ ≫ h2.opcyclesIso.inv.

LaTeX

$$opcyclesMap(\phi) = h1.opcyclesIso.hom \circ γ.φQ \circ h2.opcyclesIso.inv$$

Lean4

theorem rightHomologyMap_comm [S₁.HasRightHomology] [S₂.HasRightHomology] :
    rightHomologyMap φ ≫ h₂.rightHomologyIso.hom = h₁.rightHomologyIso.hom ≫ γ.φH := by
  simp only [γ.rightHomologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

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