opcyclesMap_eq — Mathlib

English

Given RightHomology data h1,h2 and γ, we have opcyclesMap φ = h1.opcyclesIso.hom ≫ γ.φQ ≫ h2.opcyclesIso.inv.

Русский

Пусть дано правое гомологическое данные h1,h2 и γ. Тогда opcyclesMap φ = h1.opcyclesIso.hom ≫ γ.φQ ≫ h2.opcyclesIso.inv.

LaTeX

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

Lean4

theorem opcyclesMap_eq [S₁.HasRightHomology] [S₂.HasRightHomology] :
    opcyclesMap φ = h₁.opcyclesIso.hom ≫ γ.φQ ≫ h₂.opcyclesIso.inv :=
  by
  dsimp [RightHomologyData.opcyclesIso, cyclesMapIso']
  rw [← γ.opcyclesMap'_eq, ← opcyclesMap'_comp, ← opcyclesMap'_comp, id_comp, comp_id]
  rfl

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