Jump to content

Heyting field

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by 2601:581:c100:7810:f9bd:7235:a052:5d04 (talk) at 15:12, 14 February 2019. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

A Heyting field is one of the inequivalent ways in constructive mathematics to capture the classical notion of a field. It is essentially a field with an apartness relation. A commutative ring is a Heyting field if ¬, either or is invertible for every , and each noninvertible element is zero. The first two conditions say that the ring is local; the first and third conditions say that it is a field in the classical sense.

The apartness relation is defined by writing # if is invertible. This relation is often now written as with the warning that it is not equivalent to ¬. For example, the assumption ¬ is not generally sufficient to construct the inverse of , but is.

The prototypical Heyting field is the real numbers.

References

  • Mines, Richman, Ruitenberg. A Course in Constructive Algebra. Springer, 1987.