In constructive mathematics, we often do algebra by equipping an algebra with a tight apartness (and requiring the algebraic operations to be strongly extensional). In this context, it is convenient to replace subalgebras with anti-subalgebras, which classically are simply the complements of subalgebras.


Let us work in the context of universal algebra, so an algebra is a set XX equipped with a family of functions f i:X n iXf_i\colon X^{n_i} \to X (where each arity? n in_i is a cardinal number) that satisfy certain equational identities (which are irrelevant here). As usual, a subalgebra of XX is a subset SS such that f i(p 1,,p n i)Sf_i(p_1,\ldots,p_{n_i}) \in S whenever each p kSp_k \in S.

Now we require SS to have a tight apartness \ne, which induces a tight apartness on each X n iX^{n_i} (via existential quantification), and we require the operations f if_i to be strongly extensional. (There is no need, in general, to require that any arity n in_i be finite or that there be finitely many f if_i.)

A subset AA of XX is open (or \ne-open) if, whenever pAp \in A, qAq \in A or pqp \ne q. An antisubalgebra of XX is an open subset AA such that p jAp_j \in A for some jj whenever f i(p 1,,p n i)Af_i(p_1,\ldots,p_{n_i}) \in A for any ii. By taking the contrapositive, we see that the complement of AA is a subalgebra SS; then AA may be recovered as the \ne-complement of SS (the set of those pp such that pqp \ne q whenever qSq \in S). However, we cannot start with an arbitrary subalgebra SS and get an antisubalgebra AA in this way, as we cannot (in general) prove openness. (Impredicatively, we can take the antisubalgebra generated by the \ne-complement of SS, as described below, but its complement will generally only be a superset of SS.)


Unless otherwise noted, all of the constructions in these examples should be predicative.

The empty subset of any algebra is an antisubalgebra, the empty antisubalgebra or improper antisubalgebra, whose complement is the improper subalgebra (which is all of XX). An antisubalgebra is proper if it is inhabited; the ability to have a positive definition of when an antisubalgebra is proper is a significant motivation for the concept.

If AA is an antisubalgebra and cc is a constant (given by an operation X 0XX^0 \to X or a composite of same with other operations), then pcp \ne c whenever pAp \in A. If there are only Kuratowski-finitely many constants (which is needed to prove openness), we define the trivial antisubalgebra to be the subset of those elements pp such that pcp \ne c for each constant cc (the \ne-complement of the trivial subalgebra). In general, we may also take the trivial antisubalgebra to be the union of all antisubalgebras (but this is not predicative).

Instead of subgroups, use antisubgroups. In detail, a subset AA of XX is an antisubgroup if p1p \ne 1 whenever pAp \in A, pAp \in A or qAq \in A whenever pqAp q \in A, and pAp \in A whenever p 1Ap^{-1} \in A. (We need not assume that AA is open; this can be proved.) An antisubgroup AA is normal if pqAp q \in A whenever qpAq p \in A. The trivial antisubgroup is the \ne-complement of {1}\{1\}.

Instead of ideals (of rings), use antiideals. (Technically, these are antisubalgebras of the ring as a module over itself.) In detail, a subset AA of XX is a two-sided antiideal (or simply an antiideal in the commutative case) if p0p \ne 0 whenever pAp \in A, pAp \in A or qAq \in A whenever p+qAp + q \in A, and pAp \in A and qAq \in A whenever pqAp q \in A. AA is a left antiideal if instead the last condition requires only that pAp \in A, and AA is a right antiideal if instead the last condition requires only that qAq \in A. It follows that an antiideal AA is proper iff 1A1 \in A. AA is prime if it is proper and pqAp q \in A whenever pAp \in A and qAq \in A; AA is minimal if it is proper and, for each pAp \in A, for some qq, for each rAr \in A, pq+r1p q + r \ne 1 and qp+r1q p + r \ne 1 (which is constructively stronger than being prime and minimal among proper ideals). The trivial antiideal is the \ne-complement of {0}\{0\}.

Note that a union of antisubalgebras is again an antisubalgebra. Given any subset BB of XX, the antisubalgebra generated by BB is the union of all antisubalgebras contained in BB. (This construction is not predicative, although it may still be true predicatively that the generated subalgebra exists in some situations.)

Quotient algebras

To form a quotient group or a quotient ring, it's enough to have a normal subgroup or a two-sided ideal. However, if we want the quotient algebra to inherit an apartness from the original algebra, then we need antisubgroups and antiideals.

In general, instead of congruence relations, use anticongruence relations. An anticongruence relation KK on XX is an apartness relation on XX that is also an antisubalgebra of K×KK \times K. Given this, let RR be the negation of KK; then RR is a congruence relation, giving a quotient algebra X/RX/R. Furthermore, KK becomes a tight apartness on X/RX/R, relative to which the algebra operations on X/RX/R are strongly extensional. We denote the resulting algebra-with-apartness by X/KX/K. (This notation should cause no confusion; if an apartness relation on a set XX is also an equivalence relation, then XX must be the empty set, which has a unique apartness and at most one algebra structure, and the only quotient set of the empty set is itself.) The quotient map XX/KX \twoheadrightarrow X/K is also strongly extensional.

Conversely, any strongly extensional map f:XYf\colon X \to Y between algebras with apartness gives rise to an anticongruence akerf\aker f on XX (the antikernel of ff), where (p,q)akerf(p, q) \in \aker f iff f(p)f(q)f(p) \ne f(q). The complement of the antikernel is the kernel in the usual sense of universal algebra, so the quotient algebra X/(akerf)X/(\aker f) is naturally isomorphic to a subalgebra imfim f of YY; the maps XX/(akerf)imfYX \twoheadrightarrow X/(\aker f) \cong \im f \hookrightarrow Y are strongly extensional. Similarly, a sequence XfYgZX \overset{f}\to Y \overset{g} \to Z is exact iff imf\im f is the complement of akerg\aker g.

(We would like to say that there is an antisubalgebra aimf\aim f of YY whose complement is imf\im f; then we could, for example, define a stronger notion of exactness requiring that akerg\aker g equal the antiimage of ff. In principle, aa should belong to aimf\aim f iff af(p)a \ne f(p) for every pp in XX. If XX is Kuratowski-finite, then this works, but in general, we can prove neither that this is open nor that its complement is all of imf\im f.)

Given a group-with-apartness and a normal antisubgroup AA, we define an anticongruence KK, where (p,q)K(p, q) \in K iff pq 1Ap q^{-1} \in A. Similarly, given a ring-with-apartness and a two-sided antiideal AA, we define an anticongruence KK, where (p,q)K(p, q) \in K iff pqAp - q \in A. This allows us to form quotient groups or quotient rings by modding out by normal antisubgroups or two-sided antiideals. Conversely, we can interpret the antikernel as a normal antisubgroup or two-sided antiideal: pakerfp \in \aker f iff f(p)1f(p) \ne 1, pakerfp \in \aker f iff f(p)0f(p) \ne 0, etc. In general, this works for any Omega-group structure.


These concepts play a large role in

  • Ray Mines?, Fred Richman, Wim Ruitenburg?. A Course in Constructive Algebra. Springer, 1987.

But I can't be sure that everything above appears in this reference.

Revised on January 17, 2017 12:56:52 by Toby Bartels (