English
For a morphism g: X → Y in an Abelian category, g is epi with an injective kernel if and only if there exists an injective object I and a morphism f: I → X with f ∘ g = 0, such that the short complex I → X → Y splits.
Русский
Для морфизма g: X → Y в абелевой категории gcd является эпиморфизмом с инъективным ядром тогда и только тогда существует инъективный объект I и морфизм f: I → X, удовлетворяющий f ∘ g = 0, и короткая последовательность I → X → Y распадается на прямую сумму.
LaTeX
$$$\\mathrm{epiWithInjectiveKernel}(g) \\iff \\exists I\\; (Injective\\; I)\\; \\exists f:I\\to X\\; (f \\circ g = 0)\\;\\text{and }\\mathrm{ShortComplex.mk}(f,g,w)\\text{ splits}$$$
Lean4
/-- A morphism `g : X ⟶ Y` is epi with an injective kernel iff there exists a morphism
`f : I ⟶ X` with `I` injective such that `f ≫ g = 0` and
the short complex `I ⟶ X ⟶ Y` has a splitting. -/
theorem epiWithInjectiveKernel_iff {X Y : C} (g : X ⟶ Y) :
epiWithInjectiveKernel g ↔
∃ (I : C) (_ : Injective I) (f : I ⟶ X) (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting :=
by
constructor
· rintro ⟨_, _⟩
let S := ShortComplex.mk (kernel.ι g) g (by simp)
exact
⟨_, inferInstance, _, S.zero,
⟨ShortComplex.Splitting.ofExactOfRetraction S (S.exact_of_f_is_kernel (kernelIsKernel g))
(Injective.factorThru (𝟙 _) (kernel.ι g)) (by simp [S]) inferInstance⟩⟩
· rintro ⟨I, _, f, w, ⟨σ⟩⟩
have : IsSplitEpi g := ⟨σ.s, σ.s_g⟩
let e : I ≅ kernel g := IsLimit.conePointUniqueUpToIso σ.shortExact.fIsKernel (limit.isLimit _)
exact ⟨inferInstance, Injective.of_iso e inferInstance⟩
