```
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 (_==_)
```

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:

- A set $ 𝔽 $
- Two binary operations: + and −

where:

- $ 𝔽 $ is an abelian group under addition, which implies the operation +:
- is associative
- is commutative
- has an inverse (−)
- has an identity

- $ 𝔽 $ is an abelian group under multiplication, which implies the operation ★:
- is associative
- is commutative
- has an inverse (−)
- has an identity

- Multiplication is distributive over addition
- 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 + 0# -_
+-isAbelianGroup : IsAbelianGroup * 1# ÷_
*-isAbelianGroup : * DistributesOver +
distrib : Zero 0# *
zero
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 + * -_ 0# 1#
isRing = record
isRing { +-isAbelianGroup = +-isAbelianGroup
; *-isMonoid = *-isMonoid
; distrib = distrib
; zero = zero
}
```

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 + 0# -_
+-isAbelianGroup : IsAbelianGroup * 1# ÷_
*-isAbelianGroup : * DistributesOver +
distrib : Zero 0# *
zero : 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 + * -_ 0# 1#
isRing = record
isRing { +-isAbelianGroup = +-isAbelianGroup
; *-isMonoid = *-isMonoid
; distrib = distrib
; zero = zero
}
```

The real and rational numbers form ordered fields.