homologyMap_nullHomotopic — Mathlib

English

Let S1 and S2 be short complexes with homology. The homology map of a null-homotopic morphism is zero.

Русский

Пусть S1 и S2 — краткие комплексы с гомологией. Карта гомологии нулевой гомотопии равна нулю.

LaTeX

$$$\\operatorname{homologyMap}\\big(\\text{nullHomotopic}_{S_1,S_2}(h_0,h_0\\_f,h_1,h_2,h_3,g\\_3)\\big) = 0$$$

Lean4

@[simp]
theorem homologyMap_nullHomotopic [S₁.HasHomology] [S₂.HasHomology] (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) :
    homologyMap (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0 := by apply homologyMap'_nullHomotopic

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