nLab Heyting field

 Definition

In constructive mathematics:

Definition

A Heyting field is a local ring where every non-invertible element is equal to zero. More specifically, it is a commutative ring $R$ such that

1. $R$ is non-trivial ($0 \neq 1$);

2. given elements $a \in R$ and $b \in R$, if $a + b$ is invertible, then either $a$ is invertible or $b$ is invertible;

3. given an element $a \in R$, if $a$ is non-invertible, then $a = 0$.

Equivalently, a Heyting field is:

• a local ring $R$ whose quotient ring by the ideal of non-invertible elements is isomorphic to $R$;

• a local ring $R$ such that the canonical apartness relation $\#$ — defined as $a \# b$ if and only if $a - b$ is invertible — is a tight apartness relation.

• a local ring which is both reduced and Artinian.

• a local ring which is a semiprimitive ring.

Remark

In Lombardi & Quitté (2010), the authors’ definition of Heyting field do not include the non-equational axiom $1 \neq 0$. Instead, they define non-invertible to mean that if the element is invertible, then $1 = 0$. With such a definition, the trivial ring counts as a Heyting field and constitutes the terminal object in the categories of Heyting fields.

 Properties

Stable equality.

Every Heyting field $R$ has stable equality, because it has a tight apartness relation defined as $a \# b$ if and only if $a - b$ is invertible. For all elements $a \in R$ and $b \in R$, $\neg \neg \neg (a \# b) \iff \neg (a \# b)$, and because $\neg (a \# b) \iff a = b$, $\neg \neg (a = b) \iff a = b$, and thus $R$ has stable equality.

Decidable tight apartness

A Heyting field with decidable tight apartness is a discrete field.

Weak Heyting fields

A weak Heyting field (cf. Richman (2020)) or Johnstone residue field is a commutative ring which only satisfy axioms 1 and 3 in Def. . Johnstone (1977) referred these as a residue field; however, this is not to be confused with the already existing notion of a residue field in algebraic geometry as the quotient field of a local ring.

If every weak Heyting field with decidable equality is a Heyting field, then excluded middle follows. The following proof is due to Mark Saving:

Definition

Let $p$ be a proposition. We define the set $R_p$ to be the union of $\mathbb{Z}$ and $\{x \in \mathbb{Q} \vert p\}$

$R_p$ is a subring of the rational numbers $\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$.

Theorem

$R_p$ is a weak Heyting field iff $\neg \neg p$.

Proof

Given a proposition $p$, suppose its double negation $\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}$ is not in $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_p$ is a weak Heyting field. If $\neg p$ held, we would have $R_p = \mathbb{Z}$, which clearly is not a Johnstone residue field since $2$ is neither invertible nor zero. So we must have $\neg \neg p$.

Theorem

$R_p$ is a Heyting field iff it is the case that $p$ iff $R_p$ is a discrete field.

Proof

Suppose $R_p$ is a Heyting field. Then either $2$ or $3$ has a multiplicative inverse, so either $2^{-1} \in R_p$ 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.

Theorem

If every weak Heyting field with discrete equality is Heyting, then excluded middle is valid.

Proof

From the lemmas above, if every weak Heyting field with decidable equality is a Heyting field, then $p \iff \neg \neg p$ holds for all propositions $p$. So we have full excluded middle.

See also

• field

• local ring

• reduced local ring

• Artinian local ring

• ordered field

• tight apartness ring

 References

• 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]

• Fred Richman, Laurent series over $\mathbb{R}$. Communications in Algebra, Volume 48, Issue 5, 11 Jan 2020 Pages 1982-1984 [doi:10.1080/00927872.2019.1710166]