Superfluous subobjects and projective covers in an abelian category

Let $\mathcal{C}$ be an abelian category (Abelian category) and let $n:N\to P$ be a monomorphism, regarded as the subobject $[n]$ of $P$ (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms). The subobject $[n]$ is superfluous when for every subobject $[m]:M\to P$ whose join with $[n]$ satisfies

$[n]\vee [m]=[1_P]$

one already has $[m]=[1_P]$ (The join of two subobjects in an abelian category). Here $[1_P]$ is the subobject represented by the identity of $P$. An essential epimorphism $\pi :Q\to X$ is an epimorphism whose kernel, taken as a morphism $\ker \pi \to Q$ (Kernels and cokernels in a category with zero morphisms as equalizers and coequalizers, Monomorphism and epimorphism by left and right cancellation), represents a superfluous subobject of $Q$. A projective cover of $X$ is an essential epimorphism $\pi :Q\to X$ with $Q$ projective in the sense of Projective object.

As elsewhere on this page, the bracket notation abbreviates statements about representatives: $[m]=[1_P]$ says that $m$ and $1_P$ mutually factor (Subobject and quotient object as mutual-factorisation classes of monomorphisms and epimorphisms), and such a factorisation of $1_P$ through the monomorphism $m$ exhibits $m$ as an isomorphism onto $P$. Thus in a module category the condition "$[n]\vee [m]=[1_P]$ implies $[m]=[1_P]$" reads "$N+M=P$ implies $M=P$", where the join of subobjects of a module is the sum of the corresponding submodules, and this is precisely the superfluous-kernel condition of the module notion of An essential epimorphism is a surjection with superfluous kernel, and a projective cover is a projective source with such a map, with the same projective-source requirement. The class-and-size conventions used by the bracket notation are those of Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why $\mathbf{C}\mathbf{A}\mathbf{T}$ is not formed.

This is the general form of the projective-cover clause of Finite k-linear abelian categories, whose phrasing "every simple object has a projective cover" is the module-scoped language of An essential epimorphism is a surjection with superfluous kernel, and a projective cover is a projective source with such a map read in an abstract abelian category. The definition asserts no existence of covers, selects no object, and uses no choice; each later existence statement is an explicit hypothesis.