# Generalised elements in regular categories

In [Categories for the working mathematician, Ch. VIII, §4], Mac Lane introduces the method of members for interpreting diagram chases in an abelian category. We can (try to) generalise this to arbitrary regular categories as follows:

• A generalised element of an object X is a morphism with codomain X.
• Given two generalised elements of X, say x0 and x1, we define x0 =X x1 to mean that there exist regular epimorphisms e0 and e1 such that x0e0 = x1e1 (in the usual sense of morphisms).

It is straightforward to see that x0 =X x1 if and only if x0 and x1 have the same image in X, so generalised elements of X up to =X are the same as subobjects of X up to isomorphism.

We can then prove this lemma:

Lemma. A morphism f : XY is a regular epimorphism if and only if, for each generalised element y of Y, there exists a generalised element x of X such that fx =Y y.

The obvious next thing to try to prove is the following:

Claim. A morphism f : XY is a monomorphism if and only if fx0 =Y fx1 implies x0 =X x1.

It is certainly true if the category is abelian (cf. Mac Lane), and it is also true when there are “enough subterminal objects” (e.g. sheaves on a topological space). Unfortunately it is false in general. Given a non-trivial group G, the category of G-sets is a regular category (indeed, a topos), but the unique morphism G → 1 is not a monomorphism despite satisfying the condition on generalised elements.

One way of repairing this is to abandon the equivalence relations =X. This leads to the forcing semantics for regular logic in regular categories. Roughly:

• Ux0 =X x1 means that x0 and x1 are equal as morphisms UX.
• Uφψ means that both Uφ and Uψ hold.
• U ⊩ ∃x : X. φ, where x is a free variable in φ, means that there exist a regular epimorphism e : VU and a morphism x : VX such that Ve*φ, where e*φ is the result of replacing every generalised element y appearing in φ with ye.
• Uφψ means that, for any morphism f : VU, Vf*φ implies Vf*ψ.

Note that ⇒ is not a logical connective in regular logic, so it can only appear in the outermost level. Under this interpretation, given a morphism f : XY, we have Y ⊩ ∃x : X. fx =Y idY if and only if f is a regular epimorphism, and X × Xfx0 =Y fx1x0 =X x1, where x0, x1 : X × XX are the two projections, if and only if f is a monomorphism.

However, one is left wondering whether there might be a simplification of the forcing semantics that does not require us to keep track of the domains of our generalised elements, as in the method of members.