symmetric monoidal (∞,1)-category of spectra
A Heyting field is a local ring where every non-invertible element is equal to zero. More specifically, it is a commutative ring such that
is non-trivial ();
given elements and , if is invertible, then either is invertible or is invertible;
given an element , if is non-invertible, then .
Equivalently, a Heyting field is:
a local ring whose quotient ring by the ideal of non-invertible elements is isomorphic to ;
a local ring such that the canonical apartness relation — defined as if and only if is invertible — is a tight apartness relation.
a local ring which is both reduced and Artinian.
a local ring which is a semiprimitive ring.
In Lombardi & Quitté (2010), the authors’ definition of Heyting field do not include the non-equational axiom . Instead, they define non-invertible to mean that if the element is invertible, then . With such a definition, the trivial ring counts as a Heyting field and constitutes the terminal object in the categories of Heyting fields.
Every Heyting field has stable equality, because it has a tight apartness relation defined as if and only if is invertible. For all elements and , , and because , , and thus has stable equality.
A Heyting field with decidable equality is a discrete field.
Johnstone (1977) defined a residue field to be a commutative ring which only satisfy axioms 1 and 3 in Def. ; we shall call these Johnstone residue fields in this article to not confuse them with the notion of residue field in algebraic geometry.
If every Johnstone residue field with decidable equality is a Heyting field, then excluded middle follows. The following proof is due to Mark Saving:
Let be a proposition. We define the set to be the union of and
is a subring of the rational numbers .
Since is a subset of and has decidable equality, also has decidable equality. And of course in .
is a Johnstone residue field iff .
Given a proposition , suppose its double negation , and consider some . Suppose does not have a multiplicative inverse. Now suppose . Then we see that is not in . If held, we would have . So we know holds. But this is a contradiction. Therefore, must be zero (using decidable equality).
Conversely, suppose is a Johnstone residue field. If held, we would have , which clearly is not a Johnstone residue field since is neither invertible nor zero. So we must have .
is a Heyting field iff it is the case that iff is a discrete field.
Suppose is a Heyting field. Then either or has a multiplicative inverse, so either or . In either case, we see that holds. If holds, then , which is a discrete field. And if is a discrete field, it is clearly a Heyting field.
If every Johnstone residue field with discrete equality is Heyting, then excluded middle is valid.
From the lemmas above, if every Johnstone residue field with decidable equality is a Heyting field, then holds for all propositions . So we have full excluded middle.
Peter Johnstone, Rings, Fields, and Spectra, Journal of Algebra 49 (1977) 238-260 [doi:10.1016/0021-8693(77)90284-8]
Henri Lombardi, Claude Quitté (2010): Commutative algebra: Constructive methods (Finite projective modules) Translated by Tania K. Roblo, Springer (2015) [doi:10.1007/978-94-017-9944-7, pdf]
Last revised on January 12, 2023 at 18:20:49. See the history of this page for a list of all contributions to it.