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.


One thought on “Generalised elements in regular categories

  1. Just for the record, not keeping track of the domains prevents constructing morphisms using the naive element-based language (as opposed to merely verifying some properties of already-given morphisms). This happens even in the abelian case.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s