Contents Previous Next

Fields and Family

open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)

open import Types.product
open import Types.relations
open import Types.equality

module Algebra.fields {a ℓ} {A : Set a} (_==_ : Rel A ℓ) where
  open import Types.operations (_==_)

  open import Algebra.order (_==_)
  open import Algebra.groups (_==_)
  open import Algebra.rings (_==_)

Fields

In abstract algebra, a field has a very specific definition, which is different from the physics conception of a “thing spread across space”. A field is, like real numbers, a bunch of objects (a set) for which addition, subtraction, multiplication and division operations are defined. Rational numbers, complex numbers as well as the set of binary values - 0 & 1, like real numbers, fall into this category. Another way to define fields is to define addition, multiplication and their inverses, i.e. subtraction and division, except at “0” - the identity element for multiplication. The formal definition of fields tries to capture all aspects of these operations.

A field is defined as a set with two operations - addition and multiplication. Thus, an operation on a field would be a function type with the signature F : 𝔽 → 𝔽 → 𝔽 where 𝔽 is the set of objects in the field.

A field is a structure containing:

where:

  1. $ 𝔽 $ is an abelian group under addition, which implies the operation +:
  2. $ 𝔽 $ is an abelian group under multiplication, which implies the operation ★:
  3. Multiplication is distributive over addition
  4. There must be an annihilating element 𝕖 such that $ ∀ x : 𝕖 ★ x = 𝕖 $

A field is thus a more restricted version of a Ring, where there are additional requirements of commutativity and inverse of multiplication.

  record IsField (+ * : ★ A) (-_ ÷_ : ♠ A) (0# 1# : A) : Set (a ⊔ ℓ) where
    field
      +-isAbelianGroup : IsAbelianGroup + 0# -_
      *-isAbelianGroup : IsAbelianGroup * 1# ÷_
      distrib          : * DistributesOver +
      zero             : Zero 0# *

    open IsAbelianGroup +-isAbelianGroup public
      renaming
      ( assoc               to +-assoc
      ; ∙-cong              to +-cong
      ; ∙-congˡ             to +-congˡ
      ; ∙-congʳ             to +-congʳ
      ; identity            to +-identity
      ; identityˡ           to +-identityˡ
      ; identityʳ           to +-identityʳ
      ; inverse             to -‿inverse
      ; inverseˡ            to -‿inverseˡ
      ; inverseʳ            to -‿inverseʳ
      ; ⁻¹-cong             to -‿cong
      ; comm                to +-comm
      ; isMagma             to +-isMagma
      ; isSemigroup         to +-isSemigroup
      ; isMonoid            to +-isMonoid
      ; isCommutativeMonoid to +-isCommutativeMonoid
      ; isGroup             to +-isGroup
      )

    open IsAbelianGroup *-isAbelianGroup public
      using ()
      renaming
      ( assoc               to *-assoc
      ; ∙-cong              to *-cong
      ; ∙-congˡ             to *-congˡ
      ; ∙-congʳ             to *-congʳ
      ; identity            to *-identity
      ; identityˡ           to *-identityˡ
      ; identityʳ           to *-identityʳ
      ; inverse             to ÷‿inverse
      ; inverseˡ            to ÷‿inverseˡ
      ; inverseʳ            to ÷‿inverseʳ
      ; ⁻¹-cong             to ÷‿cong
      ; comm                to *-comm
      ; isMagma             to *-isMagma
      ; isSemigroup         to *-isSemigroup
      ; isMonoid            to *-isMonoid
      ; isCommutativeMonoid to *-isCommutativeMonoid
      ; isGroup             to *-isGroup
      )

    isRing : IsRing + * -_ 0# 1#
    isRing = record
      { +-isAbelianGroup = +-isAbelianGroup
      ; *-isMonoid       = *-isMonoid
      ; distrib          = distrib
      ; zero             = zero
      }

Ordered Fields

Ordered fields impose an additional restriction on fields: there has to be an order ≤ between members of 𝔽. This order is required to be a total order.

  record IsOrderedField (+ * : ★ A) (-_ ÷_ : ♠ A) (_≤_ : Rel A ℓ) (0# 1# : A) : Set (a ⊔ ℓ) where
    field
      +-isAbelianGroup : IsAbelianGroup + 0# -_
      *-isAbelianGroup : IsAbelianGroup * 1# ÷_
      distrib          : * DistributesOver +
      zero             : Zero 0# *
      isTotalOrder     : IsTotalOrder _≤_

    open IsAbelianGroup +-isAbelianGroup public
      renaming
      ( assoc               to +-assoc
      ; ∙-cong              to +-cong
      ; ∙-congˡ             to +-congˡ
      ; ∙-congʳ             to +-congʳ
      ; identity            to +-identity
      ; identityˡ           to +-identityˡ
      ; identityʳ           to +-identityʳ
      ; inverse             to -‿inverse
      ; inverseˡ            to -‿inverseˡ
      ; inverseʳ            to -‿inverseʳ
      ; ⁻¹-cong             to -‿cong
      ; comm                to +-comm
      ; isMagma             to +-isMagma
      ; isSemigroup         to +-isSemigroup
      ; isMonoid            to +-isMonoid
      ; isCommutativeMonoid to +-isCommutativeMonoid
      ; isGroup             to +-isGroup
      )

    open IsAbelianGroup *-isAbelianGroup public
      using ()
      renaming
      ( assoc               to *-assoc
      ; ∙-cong              to *-cong
      ; ∙-congˡ             to *-congˡ
      ; ∙-congʳ             to *-congʳ
      ; identity            to *-identity
      ; identityˡ           to *-identityˡ
      ; identityʳ           to *-identityʳ
      ; inverse             to ÷‿inverse
      ; inverseˡ            to ÷‿inverseˡ
      ; inverseʳ            to ÷‿inverseʳ
      ; ⁻¹-cong             to ÷‿cong
      ; comm                to *-comm
      ; isMagma             to *-isMagma
      ; isSemigroup         to *-isSemigroup
      ; isMonoid            to *-isMonoid
      ; isCommutativeMonoid to *-isCommutativeMonoid
      ; isGroup             to *-isGroup
      )

    isRing : IsRing + * -_ 0# 1#
    isRing = record
      { +-isAbelianGroup = +-isAbelianGroup
      ; *-isMonoid       = *-isMonoid
      ; distrib          = distrib
      ; zero             = zero
      }

The real and rational numbers form ordered fields.

Fields and family 2