


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. 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; however, for a few results, we will need a special case of these that we will call having well-behaved constants:

  • each arity is either 00 or at least 11 (so each operation either is a constant or has at least one operand), and
  • the number of constants is Kuratowski-finite (so there is an exhaustive list c 1,c 2,c 3,c nc_1, c_2, c_3, \ldots c_n of constants for some natural number nn, where it remains possible that c i=c jc_i = c_j might be an equational law).

The first item is true of all derived operations in the theory as long as it is true of the fundamental operations in the signature; but in this last item, we're counting all derived constants, not just the fundamental ones. For example, the theory of (unital) rings does not have well-behaved constants, because there are infinitely many constants (one for each integer).

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. An algebra XX with these properties is called an inequality algebra. (For much of the theory we don’t need the apartness to be tight, but for some purposes it is necessary.)

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, but we cannot (in general) start with a subalgebra SS and get an antisubalgebra AA. (Impredicatively, we can take the antisubalgebra generated, as described below, by the \ne-complement of SS, that is the set of those elements of XX that \ne every element of SS, but its complement will generally only be a superset of SS.)




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 the theory has well-behaved constants, then we can 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 this case the definition can be simplified a bit: a subset AA of an inequality group 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 from strong extensionality of the group operations on XX and the stronger form of the nullary anticlosure condition (“p1p \ne 1 whenever pAp \in A” is a strengthening of the condition ¬(1A)\neg (1\in A) that would be the literal nullary case of the general definition.) 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.) Again we can omit \ne-openness by strengthening the nullary condition. 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 (or antiprime) if it is proper and prqAp r q \in A for some rr whenever pAp \in A and qAq \in A; in the commutative case, we can say that pqAp q \in A whenever pAp \in A and qaq \in a. AA is minimal (or antimaximal) 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); of course, we only need one of these two inequalities in the commutative case. The trivial antiideal is the \ne-complement of {0}\{0\}.


In some cases, we may prefer to anti-generate: given any subset BB of XX, the antisubalgebra antigenerated by BB is the union of all antisubalgebras whose elements are all distinct from (\ne) each element of BB, in other words the antisubalgebra generated by the \ne-complement of BB. For example, the trivial antisubgroup of a group is antigenerated by {1}\{1\}, and the trivial antiideal of a ring is antigenerated by {0}\{0\}. More generally than these examples, we may talk of the cyclic antisubgroup? or principal antiideal antigenerated by a given element of the group or ring.

Quotient algebras



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 (because the apartness of YY is tight) the kernel in the usual sense of universal algebra. Thus, 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, aimf\aim f should be the \ne-complement of imf\im f. 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.

Localic point of view

As noted at apartness relation, an apartness relation on a set XX is equivalent to a (strongly) closed equivalence relation on the corresponding discrete locale, and the \ne-open subsets are those whose complementary closed sublocales are stable under this equivalence relation, and the \ne-topology itself is the corresponding quotient locale. From this point of view, an algebra structure is strongly extensional if it respects the equivalence relation, hence passes to the quotient; and an antisubalgebra is an \ne-open set whose complementary closed sublocale is additionally a localic subalgebra, since the operation C\mathsf{C} from open sublocales to closed ones takes arbitrary (not only finite) unions to intersections.

In other words, antisubalgebras of an inequality algebra are equivalent to closed subalgebras of a localic algebra, in the case when the latter is the quotient of a discrete algebra by a closed localic congruence.


According to Troelstra and van Dalen:

The study of algebraic structures in an intuitionistic setting was undertaken by Heyting (1941)… in full generality, equipped with an apartness relation. The notion of an antisubstructure, implicit in Heyting’s treatment of ideals in polynomial rings, was formulated explicitly by D.S. Scott (1979) (N.B. the first draft of this paper contains a good deal more than the published version). Ruitenburg (1982, 1982A) deals with intuitionistic algebra in the spirit of Heyting and Scott.

  • Arend Heyting, Untersuchungen über intuitionistische Algebra, 1941

  • Dana Scott, Identity and existence in intuitionistic logic, 1979

  • Wim Ruitenberg?, Intuitionistic Algebra, Ph.D. Thesis, Rijksuniversiteit Utrecht, 1982

  • Wim Ruitenberg?, Primality and invertibility of polynomials, 1982

  • Surprisingly, antisubalgebras make hardly any appearence in Ray Mines?, Fred Richman, Wim Ruitenburg?. A Course in Constructive Algebra. Springer, 1987.

  • More can be found in Anne Troelstra and Dirk van Dalen?, Constructivism in Mathematics (volume 2).

Last revised on August 31, 2018 at 02:31:59. See the history of this page for a list of all contributions to it.