leftHomologyMap_nullHomotopic — Mathlib

English

For a homotopy h, φ1 = φ2 + nullHomotopic h (with appropriate data) holds.

Русский

Для гомотопии h выполняется φ1 = φ2 + nullHomotopic h (с соответствующими данными).

LaTeX

$$$\varphi_1 = \varphi_2 + \text{nullHomotopic}_{S_1,S_2}(h)$$$

Lean4

@[simp]
theorem leftHomologyMap_nullHomotopic [S₁.HasLeftHomology] [S₂.HasLeftHomology] (h₀ : S₁.X₁ ⟶ S₂.X₁)
    (h₀_f : h₀ ≫ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : S₁.g ≫ h₃ = 0) :
    leftHomologyMap (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0 := by apply leftHomologyMap'_nullHomotopic

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