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 equipped with a family of functions (where each arity? is a cardinal number) that satisfy certain equational identities (which are irrelevant here). As usual, a subalgebra of is a subset such that whenever each . There is no need, in general, to require that any arity be finite or that there be finitely many ; however, for a few results, we will need a special case of these that we will call having well-behaved constants:
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 to have a tight apartness , which induces a tight apartness on each (via existential quantification), and we require the operations to be strongly extensional. An algebra 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 of is open (or -open) if, whenever , or . An antisubalgebra of is an open subset such that for some whenever for any . By taking the contrapositive, we see that the complement of is a subalgebra , but we cannot (in general) start with a subalgebra and get an antisubalgebra . (Impredicatively, we can take the antisubalgebra generated, as described below, by the -complement of , that is the set of those elements of that every element of , but its complement will generally only be a superset of .)
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 ). 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 is an antisubalgebra and is a constant (given by an operation or a composite of same with other operations), then whenever . If the theory has well-behaved constants, then we can define the trivial antisubalgebra to be the subset of those elements such that for each constant (the -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 of an inequality group is an antisubgroup if whenever , or whenever , and whenever . We need not assume that is open; this can be proved from strong extensionality of the group operations on and the stronger form of the nullary anticlosure condition (“ whenever ” is a strengthening of the condition that would be the literal nullary case of the general definition.) An antisubgroup is normal if whenever . The trivial antisubgroup is the -complement of .
Instead of ideals (of rings), use antiideals. (Technically, these are antisubalgebras of the ring as a module over itself.) Again we can omit -openness by strengthening the nullary condition. In detail, a subset of is a two-sided antiideal (or simply an antiideal in the commutative case) if whenever , or whenever , and and whenever . is a left antiideal if instead the last condition requires only that , and is a right antiideal if instead the last condition requires only that . It follows that an antiideal is proper iff . is prime (or antiprime) if it is proper and whenever and ; is minimal (or antimaximal) if it is proper and, for each , for some , for each , and (which is constructively stronger than being prime and minimal among proper ideals). The trivial antiideal is the -complement of .
Note that a union of antisubalgebras is again an antisubalgebra. Given any subset of , the antisubalgebra generated by is the union of all antisubalgebras contained in . (This construction is not predicative, although it may still be true predicatively that the generated subalgebra exists in some situations.)
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 on is an apartness relation on that is also an antisubalgebra of . Given this, let be the negation of ; then is a congruence relation, giving a quotient algebra . Furthermore, becomes a tight apartness on , relative to which the algebra operations on are strongly extensional. We denote the resulting algebra-with-apartness by . (This notation should cause no confusion; if an apartness relation on a set is also an equivalence relation, then 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 is also strongly extensional.
Conversely, any strongly extensional map between algebras with apartness gives rise to an anticongruence on (the antikernel of ), where iff . The complement of the antikernel is (because the apartness of is tight) the kernel in the usual sense of universal algebra. Thus, the quotient algebra is naturally isomorphic to a subalgebra of ; the maps are strongly extensional. Similarly, a sequence is exact iff is the complement of .
(We would like to say that there is an antisubalgebra of whose complement is ; then we could, for example, define a stronger notion of exactness requiring that equal the antiimage of . In principle, should be the -complement of . If is Kuratowski-finite, then this works, but in general, we can prove neither that this is open nor that its complement is all of .)
Given a group-with-apartness and a normal antisubgroup , we define an anticongruence , where iff . Similarly, given a ring-with-apartness and a two-sided antiideal , we define an anticongruence , where iff . 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: iff , iff , etc. In general, this works for any Omega-group structure.
As noted at apartness relation, an apartness relation on a set is equivalent to a (strongly) closed equivalence relation on the corresponding discrete locale, and the -open subsets are those whose complementary closed sublocales are stable under this equivalence relation, and the -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 -open set whose complementary closed sublocale is additionally a localic subalgebra, since the operation 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.
These concepts play a large role in
But I can't be sure that everything above appears in this reference.