leftHomologyData — Mathlib

Lean4
/-- The left homology data on a short complex equipped with a splitting. -/
@[simps]
noncomputable def leftHomologyData [HasZeroObject C] (s : S.Splitting) : LeftHomologyData S :=
  by
  have hi :=
    KernelFork.IsLimit.ofι S.f S.zero (fun x _ => x ≫ s.r)
      (fun x hx => by simp only [assoc, s.r_f, comp_sub, comp_id, sub_eq_self, reassoc_of% hx, zero_comp])
      (fun x _ b hb => by simp only [← hb, assoc, f_r, comp_id])
  let f' := hi.lift (KernelFork.ofι S.f S.zero)
  have hf' : f' = 𝟙 _ := by
    apply Fork.IsLimit.hom_ext hi
    dsimp
    erw [Fork.IsLimit.lift_ι hi]
    simp only [Fork.ι_ofι, id_comp]
  have wπ : f' ≫ (0 : S.X₁ ⟶ 0) = 0 := comp_zero
  have hπ : IsColimit (CokernelCofork.ofπ 0 wπ) :=
    CokernelCofork.IsColimit.ofEpiOfIsZero _ (by rw [hf']; infer_instance) (isZero_zero _)
  exact
    { K := S.X₁
      H := 0
      i := S.f
      wi := S.zero
      hi := hi
      π := 0
      wπ := wπ
      hπ := hπ }
Похожие утверждения