English
In an abelian category, exactness is equivalent to epi(imageToKernel' f g 0).
Русский
В абелевой категории точность эквивалентна эпиморфизму изображения-ядра'.
LaTeX
$$$S.Exact \\iff \\mathrm{Epi}(\\mathrm{imageToKernel'}(S.f,S.g,S.zero))$$$
Lean4
/-- A functor preserving zero morphisms, epis, and kernels preserves homology. -/
theorem preservesHomology_of_preservesEpis_and_kernels [PreservesZeroMorphisms L] [PreservesEpimorphisms L]
[∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L] : PreservesHomology L :=
by
apply preservesHomology_of_map_exact
intro S hS
let φ : S.map L ⟶ (ShortComplex.mk _ _ (Abelian.image_ι_comp_eq_zero S.zero)).map L :=
{ τ₁ := L.map (Abelian.factorThruImage S.f)
τ₂ := 𝟙 _
τ₃ := 𝟙 _
comm₁₂ := by
dsimp
rw [Category.comp_id, ← L.map_comp, kernel.lift_ι] }
apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).2
apply ShortComplex.exact_of_f_is_kernel
exact KernelFork.mapIsLimit _ ((S.exact_iff_exact_image_ι).1 hS).fIsKernel L
