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 qAq \in A or pqp \ne q whenever pAp \in A. 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. 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.

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 and quotient rings by modding out by normal antisubgroups and two-sided ideals. In general, this works for any Omega-group structure.

Conversely, any strongly extensional map f:XYf\colon X \to Y between algebras with apartness gives rise to an anticongruence kerf\ker f on XX, where (p,q)kerf(p, q) \in \ker f iff f(p)f(q)f(p) \ne f(q). The quotient algebra X/(kerf)X/(\ker f) is a subalgebra (not an antisubalgebra!) of YY; the maps XX/(kerf)YX \twoheadrightarrow X/(\ker f) \hookrightarrow Y are strongly extensional.

Revised on August 26, 2015 14:23:01 by Toby Bartels (