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 x0 ∘ e0 = x1 ∘ e1 (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 : X → Y 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 f ∘ x =Y y.
The obvious next thing to try to prove is the following:
Claim. A morphism f : X → Y is a monomorphism if and only if f ∘ x0 =Y f ∘ x1 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:
- U ⊩ x0 =X x1 means that x0 and x1 are equal as morphisms U → X.
- 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 : V → U and a morphism x : V → X such that V ⊩ e*φ, where e*φ is the result of replacing every generalised element y appearing in φ with y ∘ e.
- U ⊩ φ ⇒ ψ means that, for any morphism f : V → U, V ⊩ f*φ implies V ⊩ f*ψ.
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 : X → Y, we have Y ⊩ ∃x : X. f ∘ x =Y idY if and only if f is a regular epimorphism, and X × X ⊩ f ∘ x0 =Y f ∘ x1 ⇒ x0 =X x1, where x0, x1 : X × X → X 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.