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 .
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. (There is no need, in general, to require that any arity be finite or that there be finitely many .)
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 ; then may be recovered as the -complement of (the set of those such that whenever ). However, we cannot start with an arbitrary subalgebra and get an antisubalgebra in this way, as we cannot (in general) prove openness. (Impredicatively, we can take the antisubalgebra generated by the -complement of , as described below, 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 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 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 detail, a subset of is an antisubgroup if whenever , or whenever , and whenever . (We need not assume that is open; this can be proved.) An antisubgroup is normal if whenever . The trivial antisubgroup is the -complement of .
Instead of ideals (of rings), use antiideals. 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 if it is proper and whenever and ; is minimal 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.
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 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 between algebras with apartness gives rise to an anticongruence on (the antikernel of ), where iff . The quotient algebra is naturally isomorphic? to a subalgebra of ; the maps are strongly extensional. We would like to say that there is an antisubalgebra of corresponding to ; in principle, should belong to this antisubalgebra iff for every in . 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 .
A sequence is strongly exact if is the complement of , where means the antikernel as in the previous paragraph.