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.
I added to field a mention of some other constructive variants of the definition, with a couple more references.
I fixed up the DOI link for Johnstone’s paper (at field and at local ring), since the geniuses at Elsevier use parentheses in their DOIs, which break markdown syntax.
For reference, one needs to replace (nn)
in the DOI url by %28nn%29
.
Thanks! I’ve noticed that before, but always forget about it.
cross-linked the discussion of weakly initial sets in the category of fields with the corresponding example at multi-adjoint
added pointer to:
There appears to be an error in the section on construction notions of a field. Specifically, the claim is that a residue field is discrete iff equality is decidable. But this seems not to be true.
In fact, the statement “A residue field with decidable equality is a Heyting field” is equivalent to excluded middle.
To see this, consider a proposition $p$. Consider the set $R_p = \mathbb{Z} \cup \{x \in \mathbb{Q} \mid p\}$, which is a subring of $\mathbb{Q}$. Since $R_p$ is a subset of $\mathbb{Q}$ and $\mathbb{Q}$ has decidable equality, $R_p$ also has decidable equality. And of course $0 \neq 1$ in $R_p$.
I claim that $R_p$ is a residue field iff $\neg \neg p$. For suppose $\neg \neg p$, and consider some $x \in R_p$. Suppose $x$ does not have a multiplicative inverse. Now suppose $x \neq 0$. Then we see that $x^{-1} \notin R_p$. If $p$ held, we would have $x^{-1} \in R_p$. So we know $\neg p$ holds. But this is a contradiction. Therefore, $x$ must be zero (using decidable equality).
Conversely, suppose $R$ is a residue field. Then $2 \neq 0$, so 2 does not fail to have an inverse. That is, $2^{-1}$ is not not in $R_p$. Then $\neg \neg p$.
I claim that $R_p$ is a Heyting field iff $p$ iff $R_p$ is a discrete field. For suppose $R$ is a Heyting field. Then either 2 or 3 has a multiplicative inverse, so either $2^{-1}$ or $3^{-1} \in R_p$. In either case, we see that $p$ holds. If $p$ holds, then $R_p = \mathbb{Q}$, which is a discrete field. And if $R_p$ is a discrete field, it is clearly a Heyting field.
With these facts in hand, we see that if every residue field with decidable equality is a Heyting field, then $p \iff \neg \neg p$ holds for all $p$. So we have full excluded middle.
Of course, assuming excluded middle, it is clear that all residue fields with decidable equality are discrete fields. $\square$
I have not yet determined whether all Heyting fields with decidable equality are discrete, but it seems very likely that this also cannot be proven.
If no one objects, I will change the page to say that a residue field is discrete if and only if unithood is decidable.
1 to 11 of 11