homologyMap'_nullHomotopic — Mathlib

English

If a morphism is null-homotopic, the homology map is zero.

Русский

Если морфизм гомотопен нулю, гомологическая карта равна нулю.

LaTeX

$$$\mathrm{homologyMap}'(\mathrm{nullHomotopic}\,\ldots)=0$$$

Lean4

@[simp]
theorem homologyMap'_nullHomotopic (H₁ : S₁.HomologyData) (H₂ : S₂.HomologyData) (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₃) H₁ H₂ = 0 := by apply leftHomologyMap'_nullHomotopic

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