leftHomologyMap'_congr — Mathlib

English

If two morphisms φ1, φ2 are homotopic, then the left homology map with data h1,h2 is unchanged.

Русский

Если два морфизма φ1, φ2 гомотопны, то левая карта гомологии с данными h1,h2 сохраняется неизменной.

LaTeX

$$$\\text{leftHomologyMap}'(\\phi_1,h_1,h_2) = \\text{leftHomologyMap}'(\\phi_2,h_1,h_2)$$$

Lean4

theorem leftHomologyMap'_congr (h : Homotopy φ₁ φ₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂ := by
  rw [h.eq_add_nullHomotopic, leftHomologyMap'_add, leftHomologyMap'_nullHomotopic, add_zero]

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