Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The pages apartness relation and antisubalgebra disagree about the definition of an antiideal: do we assume or ? Presumably there is a similar question for antisubgroups, etc. In particular, the general universal-algebraic definition at antisubalgebra would give as the definition (since is a constant and is a nullary disjunction), contradicting the explicit definition of antiideal later on the same page.
Does this have something to do with whether -openness is assumed explicitly or not? The page apartness relation claims that, at least for antiideals, openness is automatic as long as the ring operations are strongly extensional. But antisubalgebra assumes openness explicitly, in addition to strong extensionality of the algebraic operations.
Finally, do we ever really need the apartness to be tight?
Okay, it’s easy to prove that if is -open, then anything not in it is apart from everything in it, i.e. its logical complement and -complement agree. Thus, assuming -openness ensures that implies the stronger and similarly for all constants. Conversely, for theories containing a group operation with identity constant (such as groups and rings), if we assume , then is necessarily -open, since if then , hence or , and in the latter case and so . So in the general case, we need to assume -openness explicitly, but in some familiar cases we can get away without it by strengthening the nullary anti-closure condition.
I edited the two pages to clarify this point. However I have another question: antisubalgebra claims that can be recovered as the -complement of its complementary subalgebra, but I don’t see why.
Yes, #2 is correct. If you read things like Richman et al's book, they make their antisubalgebras -open in this way, by saying instead of . But in the general case, -openness is a separate condition.
Finally, do we ever really need the apartness to be tight?
You need it to be tight in order to say things like ‘it’s easy to prove that if is -open, then anything not in it is apart from everything in it, i.e. its logical complement and -complement agree’ (comment #2). That is open only proves half of that; that is tight proves the other half.
More generally, if I have an algebra equipped with an apartness relation relative to which the operations are all strongly extensional, then I'm really really tempted to replace it with a quotient algebra on which becomes tight.
@#3: You're right, that statement is wrong. In a theory where every arity is at least (to keep it simple), if is any proposition, then is an antisubalgebra; its complementary subalgebra is ; and the -complement of this is .
You need it to be tight in order to say things like ‘it’s easy to prove that if is -open, then anything not in it is apart from everything in it, i.e. its logical complement and -complement agree’ (comment #2). That is open only proves half of that; that is tight proves the other half.
Hmm. If is -open and and , then -openness applied to gives , hence since . In the other direction, if is -open and , then in particular by irreflexivity of , hence . Where did I use tightness?
if I have an algebra equipped with an apartness relation relative to which the operations are all strongly extensional, then I'm really really tempted to replace it with a quotient algebra on which becomes tight.
Topologically, I guess this means passing to the quotient. Which is of course not unreasonable (in particular, it’s part of sobrification), but as part of a general theory there’s often no need to assume .
Hmm, I guess you need the apartness to be tight in order for the complement of the antikernel to be the kernel. I’m not sure whether anyone thinks about topological algebra for non- spaces or what the right notion of “kernel” would be in such a case, but in any case that makes tightness seem more reasonable to me.
Would it work, impredicatively, to define the anti-image of a morphism as the antisubalgebra generated by the complement or -complement of the image? In general, how is a subalgebra related to the antisubalgebra generated by its complement?
Here’s an interesting fact I just noticed: for an inequality group, the symmetry and comparison axioms are automatic. That is, if has an irreflexive relation and a group structure that is strongly extensional with respect to , then is automatically an apartness relation.
To prove comparison, if and , then by strong extensionality of multiplication, either (impossible) or . Then by the same argument, either or , and in the former case while in the latter case .
To prove symmetry, if , then as above, hence either (impossible) or ; and in the latter case, by strong extensionality of inversion.
I just got a copy of the Mines-Richman-Ruitenberg book A Course in Constructive Algebra, and was surprised to find no antisubalgebras in it at all! I haven’t read it page by page, but if they’re there at all then they’re well-hidden. The closest thing I was able to find was a remark in passing that “In rings with a positive notion of inequality… it is natural to define an ideal to be prime if whenever then ” (where means for all , i.e. is in the inequality complement of ); but the definition of “prime ideal” that they actually use is “if then or .
So I updated the page antisubalgebra and added a reference to Troelstra + van Dalen, who do discuss antisubalgebras to a certain extent at least.
Have removed all !redirect
-commands for variants of “anti-ideal”, making them instead point to a little separate entry anti-ideal to be created in a moment…
added publication details for
and made the intended link to this item work
1 to 13 of 13