homologyMap'_congr — Mathlib

English

If two morphisms φ1, φ2 are homotopic, the induced homology maps with data h1,h2 are equal.

Русский

Если φ1 и φ2 гомотопны, индуцированные карты гомологии с данными h1,h2 совпадают.

LaTeX

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

Lean4

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

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