Injective objects and split monomorphisms

An object X of an abelian category is injective exactly when every monomorphism out of X splits. One direction holds in any category: a retraction of a monomorphism f : X ⟶ Y extends 𝟙 X along f. For the other, a morphism g : A ⟶ X is extended along a monomorphism f : A ⟶ B by pushing f out along g. In an abelian category the leg X ⟶ pushout f g is again a monomorphism, and composing the other leg with a retraction of it extends g.

This is how injectivity is checked when splittings are what one can produce, as in a finite semisimple category, where a monomorphism out of a simple object splits.

theorem TauCeti.injective_iff_forall_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) : CategoryTheory.Injective X ↔ ∀ ⦃Y : C⦄ (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.IsSplitMono f

An object of an abelian category is injective exactly when every monomorphism out of it splits.