nLab Kock field



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 RR such that Anders Kock‘s Postulate K is satisfied:

  1. RR is nontrivial (010 \neq 1)

  2. For all natural numbers nNn \in \mathrm{N} and functions x:Fin(n)Rx \colon \mathrm{Fin}(n) \to R, if x(i)0x(i) \neq 0 for all elements iFin(n)i \in \mathrm{Fin}(n), then there exists an element jFin(n)j \in \mathrm{Fin}(n) such that x(j)x(j) is invertible.

(Here Fin(n){1,,n}Fin(n) \simeq \{1, \cdots, n\} denotes any finite set with nn elements.)


Every Kock field is a local ring where the denial inequality \neq is the apartness relation defined by aba \neq b if and only if bab - a is invertible. Thus, it is a weak local ring with an equivalence relation aba \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.

 See also


Last revised on December 7, 2022 at 17:42:04. See the history of this page for a list of all contributions to it.