nLab Kock field

Contents

Idea

A definition of field in constructive mathematics which uses denial inequality. It is primarily used in synthetic differential geometry.

Definition

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.)

Properties

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

References

These are just called fields in

  • Mike Shulman, Chicago Pizza-Seminar: Synthetic Differential Geometry (pdf)

Last revised on August 19, 2024 at 14:52:05. See the history of this page for a list of all contributions to it.