rightHomologyData — Mathlib

Lean4
/-- The right homology data on a short complex equipped with a splitting. -/
@[simps]
noncomputable def rightHomologyData [HasZeroObject C] (s : S.Splitting) : RightHomologyData S :=
  by
  have hp :=
    CokernelCofork.IsColimit.ofπ S.g S.zero (fun x _ => s.s ≫ x)
      (fun x hx => by simp only [s.g_s_assoc, sub_comp, id_comp, sub_eq_self, assoc, hx, comp_zero])
      (fun x _ b hb => by simp only [← hb, s.s_g_assoc])
  let g' := hp.desc (CokernelCofork.ofπ S.g S.zero)
  have hg' : g' = 𝟙 _ := by
    apply Cofork.IsColimit.hom_ext hp
    dsimp
    erw [Cofork.IsColimit.π_desc hp]
    simp only [Cofork.π_ofπ, comp_id]
  have wι : (0 : 0 ⟶ S.X₃) ≫ g' = 0 := zero_comp
  have hι : IsLimit (KernelFork.ofι 0 wι) :=
    KernelFork.IsLimit.ofMonoOfIsZero _ (by rw [hg']; dsimp; infer_instance) (isZero_zero _)
  exact
    { Q := S.X₃
      H := 0
      p := S.g
      wp := S.zero
      hp := hp
      ι := 0
      wι := wι
      hι := hι }
Похожие утверждения