rightHomologyMap'_op — Mathlib

English

For φ: S1 ⟶ S2 with right homology data, (rightHomologyMap' φ h1 h2).op equals leftHomologyMap' (opMap φ) h2.op h1.op.

Русский

Пусть φ: S1 ⟶ S2 имеет данные правой гомологии. Тогда (rightHomologyMap' φ h1 h2).op = leftHomologyMap' (opMap φ) h2.op h1.op.

LaTeX

$$(rightHomologyMap'(φ)\, h1\, h2).op = leftHomologyMap'(opMap φ) h2.op h1.op$$

Lean4

@[simp]
theorem rightHomologyMap'_op (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op :=
  by
  let γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
  simp only [γ.rightHomologyMap'_eq, γ.op.leftHomologyMap'_eq, RightHomologyMapData.op_φH]

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