rightHomologyMap_nullHomotopic — Mathlib

English

Let S1 and S2 be short complexes with right homology. If a morphism data yields a null-homotopic comparison, then the induced right homology map vanishes.

Русский

Пусть S1 и S2 — краткие комплексы с правой гомологией. Если сравнение между ними является нулевой гомотопией, то индуцированная карта правой гомологии равна нулю.

LaTeX

$$$\\operatorname{rightHomologyMap}\\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 rightHomologyMap_nullHomotopic [S₁.HasRightHomology] [S₂.HasRightHomology] (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) :
    rightHomologyMap (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0 := by apply rightHomologyMap'_nullHomotopic

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