opcyclesMap_comm — Mathlib

English

For γ from RightHomologyMapData φ h1 h2, we have opcyclesMap φ ≫ h2.opcyclesIso.hom = h1.opcyclesIso.hom ≫ γ.φQ.

Русский

Пусть γ — RightHomologyMapData φ h1 h2. Тогда opcyclesMap φ ≫ h2.opcyclesIso.hom = h1.opcyclesIso.hom ≫ γ.φQ.

LaTeX

$$opcyclesMap(\varphi) ≫ h2.opcyclesIso.hom = h1.opcyclesIso.hom ≫ γ.φQ$$

Lean4

theorem opcyclesMap_comm [S₁.HasRightHomology] [S₂.HasRightHomology] :
    opcyclesMap φ ≫ h₂.opcyclesIso.hom = h₁.opcyclesIso.hom ≫ γ.φQ := by
  simp only [γ.opcyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]

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