We now define objects of the field family, as we did for groups and rings before.
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Types.product
open import Types.relations
open import Types.equality
open import Algebra.order
open import Algebra.groups
open import Algebra.groups2
open import Algebra.rings
open import Algebra.rings2
open import Algebra.fields
module Algebra.fields2 where
record Field c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix 9 ÷_
infix 8 -_
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
: Set c
Data _≈_ : Rel Data ℓ
_+_ : ★ Data
_*_ : ★ Data
_ : ♠ Data
-_ : ♠ Data
÷: Data
0# : Data
1# : IsField _≈_ _+_ _*_ -_ ÷_ 0# 1#
isField
open IsField isField public
: Ring _ _
ring = record { isRing = isRing }
ring
open Ring ring public
using
( +-magma; +-semigroup; +-abelianGroup
; *-magma; *-semigroup
; +-monoid ; +-commutativeMonoid
; *-monoid
; nearSemiring; semiringWithoutOne; semiring
; semiringWithoutAnnihilatingZero
)
record OrderedField c ℓ : Set (lsuc (c ⊔ ℓ)) where
infix 9 ÷_
infix 8 -_
infixl 7 _*_
infixl 6 _+_
infix 4 _≈_
field
: Set c
Data _≈_ : Rel Data ℓ
_≤_ : Rel Data ℓ
_+_ : ★ Data
_*_ : ★ Data
_ : ♠ Data
-_ : ♠ Data
÷: Data
0# : Data
1# : IsOrderedField _≈_ _+_ _*_ -_ ÷_ _≤_ 0# 1#
isOrderedField
open IsOrderedField isOrderedField public
: Ring _ _
ring = record { isRing = isRing }
ring
open Ring ring public
using
( +-magma; +-semigroup; +-abelianGroup
; *-magma; *-semigroup
; +-monoid ; +-commutativeMonoid
; *-monoid
; nearSemiring; semiringWithoutOne; semiring
; semiringWithoutAnnihilatingZero
)