Lean4
/-- The canonical `LeftHomologyData` of a short complex `S` in an abelian category, for
which the `H` field is `Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f)`. -/
@[simps]
noncomputable def ofAbelian : S.LeftHomologyData :=
by
let γ := kernel.ι S.g ≫ cokernel.π S.f
let f' := kernel.lift S.g S.f S.zero
have hf' : f' = kernel.lift γ f' (by simp [γ, f']) ≫ kernel.ι γ := by rw [kernel.lift_ι]
have wπ : f' ≫ cokernel.π (kernel.ι γ) = 0 := by
rw [hf']
simp only [assoc, cokernel.condition, comp_zero]
let e : Abelian.image S.f ≅ kernel γ :=
IsLimit.conePointUniqueUpToIso S.abelianImageToKernelIsKernel (limit.isLimit _)
have he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel :=
IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingParallelPair.zero
have fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ :=
by
rw [hf', he]
simp only [γ, f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g), assoc]
have hπ : IsColimit (CokernelCofork.ofπ _ wπ) :=
CokernelCofork.IsColimit.ofπ _ _
(fun x hx =>
cokernel.desc _ x
(by
simpa only [← cancel_epi e.hom, ← cancel_epi (Abelian.factorThruImage S.f), comp_zero, fac, assoc] using
hx))
(fun x hx => cokernel.π_desc _ _ _) (fun x hx b hb => coequalizer.hom_ext (by simp only [hb, cokernel.π_desc]))
exact
{ K := kernel S.g, H := Abelian.coimage (kernel.ι S.g ≫ cokernel.π S.f)
i := kernel.ι _, π := cokernel.π _
wi := kernel.condition _
hi := kernelIsKernel _
wπ := wπ
hπ := hπ }
