leftHomologyDataOfIsLimitKernelFork

Lean4
/-- Given an exact short complex `S` and a limit kernel fork `kf` for `S.g`, this is the
left homology data for `S` with `K := kf.pt` and `H := 0`. -/
@[simps]
noncomputable def leftHomologyDataOfIsLimitKernelFork (hS : S.Exact) [HasZeroObject C] (kf : KernelFork S.g)
    (hkf : IsLimit kf) : S.LeftHomologyData where
  K := kf.pt
  H := 0
  i := kf.ι
  π := 0
  wi := kf.condition
  hi := IsLimit.ofIsoLimit hkf (Fork.ext (Iso.refl _) (by simp))
  wπ := comp_zero
  hπ :=
    CokernelCofork.IsColimit.ofEpiOfIsZero _
      (by
        have := hS.hasHomology
        refine ((MorphismProperty.epimorphisms C).arrow_mk_iso_iff ?_).1 hS.epi_toCycles
        refine Arrow.isoMk (Iso.refl _) (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf) ?_
        apply Fork.IsLimit.hom_ext hkf
        simp [IsLimit.conePointUniqueUpToIso])
      (isZero_zero C)
Похожие утверждения