A definition of field in constructive mathematics which uses denial inequality. It is primarily used in synthetic differential geometry.
A field in the sense of Kock, or Kock field for short, is a commutative ring $R$ such that Anders Kock‘s Postulate K is satisfied:
$R$ is nontrivial ($0 \neq 1$)
For all natural numbers $n \in \mathrm{N}$ and functions $x \colon \mathrm{Fin}(n) \to R$, if $x(i) \neq 0$ for all elements $i \in \mathrm{Fin}(n)$, then there exists an element $j \in \mathrm{Fin}(n)$ such that $x(j)$ is invertible.
(Here $Fin(n) \simeq \{1, \cdots, n\}$ denotes any finite set with $n$ elements.)
Every Kock field is a local ring where the denial inequality $\neq$ is the apartness relation defined by $a \neq b$ if and only if $b - a$ is invertible. Thus, it is a weak local ring with an equivalence relation $a \approx b$ defined by the double negation of equality.
However, unlike a Heyting field, a Kock field cannot in general be proven to have stable equality, since its apartness relation is not tight.
Every Kock field with decidable equality is a discrete field.
These are just called fields in
Last revised on August 19, 2024 at 14:52:05. See the history of this page for a list of all contributions to it.