ofNullHomotopic — Mathlib

Lean4
/-- The left homology map data expressing that null homotopic maps induce the zero
morphism in left homology. -/
def ofNullHomotopic (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (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) :
    LeftHomologyMapData (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂
    where
  φK := H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) (by simp)
  φH := 0
  commf' := by
    rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc, nullHomotopic_τ₁, add_comp,
      add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i, right_eq_add, h₀_f]
  commπ := by rw [H₂.liftK_π_eq_zero_of_boundary (H₁.i ≫ h₁ ≫ S₂.f) (H₁.i ≫ h₁) (by rw [assoc]), comp_zero]
Похожие утверждения