leftHomologyMap'_op — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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