Lean4
/-- The canonical `RightHomologyData` of a short complex `S` in an abelian category, for
which the `H` field is `Abelian.image (kernel.ι S.g ≫ cokernel.π S.f)`. -/
@[simps]
noncomputable def ofAbelian : S.RightHomologyData :=
by
let γ := kernel.ι S.g ≫ cokernel.π S.f
let g' := cokernel.desc S.f S.g S.zero
have hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' (by simp [γ, g']) := by rw [cokernel.π_desc]
have wι : kernel.ι (cokernel.π γ) ≫ g' = 0 := by rw [hg', kernel.condition_assoc, zero_comp]
let e : cokernel γ ≅ Abelian.coimage S.g :=
IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) S.cokernelToAbelianCoimageIsCokernel
have he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage :=
IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one
have fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g :=
by
rw [hg', reassoc_of% he]
simp only [γ, g', cokernel.π_desc, ← cancel_epi (cokernel.π S.f), cokernel_π_comp_cokernelToAbelianCoimage_assoc]
have hι : IsLimit (KernelFork.ofι _ wι) :=
KernelFork.IsLimit.ofι _ _
(fun x hx =>
kernel.lift _ x
(by
simpa only [← cancel_mono e.hom, ← cancel_mono (Abelian.factorThruCoimage S.g), assoc, zero_comp, fac] using
hx))
(fun x hx => kernel.lift_ι _ _ _) (fun x hx b hb => equalizer.hom_ext (by simp only [hb, kernel.lift_ι]))
exact
{ Q := cokernel S.f, H := Abelian.image (kernel.ι S.g ≫ cokernel.π S.f)
p := cokernel.π _
ι := kernel.ι _
wp := cokernel.condition _
hp := cokernelIsCokernel _
wι := wι
hι := hι }
