rightHomologyDataOfIsColimitCokernelCofork

Lean4
/-- Given an exact short complex `S` and a colimit cokernel cofork `cc` for `S.f`, this is the
right homology data for `S` with `Q := cc.pt` and `H := 0`. -/
@[simps]
noncomputable def rightHomologyDataOfIsColimitCokernelCofork (hS : S.Exact) [HasZeroObject C] (cc : CokernelCofork S.f)
    (hcc : IsColimit cc) : S.RightHomologyData where
  Q := cc.pt
  H := 0
  p := cc.π
  ι := 0
  wp := cc.condition
  hp := IsColimit.ofIsoColimit hcc (Cofork.ext (Iso.refl _) (by simp))
  wι := zero_comp
  hι :=
    KernelFork.IsLimit.ofMonoOfIsZero _
      (by
        have := hS.hasHomology
        refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2 hS.mono_fromOpcycles
        refine Arrow.isoMk (IsColimit.coconePointUniqueUpToIso hcc S.opcyclesIsCokernel) (Iso.refl _) ?_
        apply Cofork.IsColimit.hom_ext hcc
        simp [IsColimit.coconePointUniqueUpToIso])
      (isZero_zero C)
Похожие утверждения