Heyting fields

Content created by Louis Wasserman.

Created on 2025-11-21.
Last modified on 2025-11-21.

module commutative-algebra.heyting-fields where
Imports 
open import commutative-algebra.commutative-rings
open import commutative-algebra.invertible-elements-commutative-rings
open import commutative-algebra.local-commutative-rings
open import commutative-algebra.trivial-commutative-rings

open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.negation
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import ring-theory.rings

Idea

A Heyting field is a local commutative ring with the properties:

Note that this is distinct from the classical notion of a field, called discrete field in constructive contexts, which asserts that every element is either invertible or equal to zero. A Heyting field is a discrete field if and only if its equality relation is decidable, which would not include e.g. the real numbers.

Definition

is-heyting-field-prop-Local-Commutative-Ring :
  {l : Level} → Local-Commutative-Ring l → Prop l
is-heyting-field-prop-Local-Commutative-Ring R =
  ( is-nontrivial-commutative-ring-Prop
    ( commutative-ring-Local-Commutative-Ring R)) ∧
  ( Π-Prop
    ( type-Local-Commutative-Ring R)
    ( λ x →
      hom-Prop
        ( ¬'
          ( is-invertible-element-prop-Commutative-Ring
            ( commutative-ring-Local-Commutative-Ring R)
            ( x)))
        ( is-zero-prop-Local-Commutative-Ring R x)))

is-heyting-field-Local-Commutative-Ring :
  {l : Level} → Local-Commutative-Ring l → UU l
is-heyting-field-Local-Commutative-Ring R =
  type-Prop (is-heyting-field-prop-Local-Commutative-Ring R)

Heyting-Field : (l : Level) → UU (lsuc l)
Heyting-Field l =
  type-subtype (is-heyting-field-prop-Local-Commutative-Ring {l})

Properties

module _
  {l : Level}
  (F : Heyting-Field l)
  where

  local-commutative-ring-Heyting-Field : Local-Commutative-Ring l
  local-commutative-ring-Heyting-Field = pr1 F

  commutative-ring-Heyting-Field : Commutative-Ring l
  commutative-ring-Heyting-Field =
    commutative-ring-Local-Commutative-Ring local-commutative-ring-Heyting-Field

  ring-Heyting-Field : Ring l
  ring-Heyting-Field = ring-Commutative-Ring commutative-ring-Heyting-Field

  type-Heyting-Field : UU l
  type-Heyting-Field = type-Ring ring-Heyting-Field

  set-Heyting-Field : Set l
  set-Heyting-Field = set-Ring ring-Heyting-Field

  zero-Heyting-Field : type-Heyting-Field
  zero-Heyting-Field = zero-Ring ring-Heyting-Field

  one-Heyting-Field : type-Heyting-Field
  one-Heyting-Field = one-Ring ring-Heyting-Field

  add-Heyting-Field :
    type-Heyting-Field → type-Heyting-Field → type-Heyting-Field
  add-Heyting-Field = add-Ring ring-Heyting-Field

  mul-Heyting-Field :
    type-Heyting-Field → type-Heyting-Field → type-Heyting-Field
  mul-Heyting-Field = mul-Ring ring-Heyting-Field

  neg-Heyting-Field : type-Heyting-Field → type-Heyting-Field
  neg-Heyting-Field = neg-Ring ring-Heyting-Field

Recent changes