English
Let S be a short complex in a preadditive category with HasHomology, and assume HasKernel for the morphism g. Then S is exact if and only if the kernel lift map ker ne l i f t? kernel.lift(S.g, S.f, S.zero) is epi. In other words, exactness is characterized by the epimorphic nature of the lift from the kernel of g to the source.
Русский
Пусть S — краткая цепь в предаддитивной категории и обладает гомологией; предположим существование ядра для морфизма g. Тогда S является точной тогда и только тогда, когда морфизм kernel.lift(S.g, S.f, S.zero) является эпиморфизмом.
LaTeX
$$$S^\text{Exact} \iff \mathrm{Epi}(\mathrm{kernel.lift} S.g S.f S.zero)$$$
Lean4
theorem exact_iff_epi_kernel_lift [S.HasHomology] [HasKernel S.g] : S.Exact ↔ Epi (kernel.lift S.g S.f S.zero) :=
by
rw [exact_iff_epi_toCycles]
apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
exact Arrow.isoMk (Iso.refl _) S.cyclesIsoKernel (by cat_disch)
