Contents Previous Next


Rings

A ring is a structure containing:

where the structure defined on the operations are:

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

Examples of rings would be natural, real, complex and rational numbers. Any algebra over a ring is also a ring. Hence, any set of n × n matrices of real numbers also forms a ring. A set of real upper or lower triangular matrices would also form a ring. The family of rings starts from semirings and goes on with commutative semirings, rings and commutative rings.

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

open import Types.product
open import Types.equality

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

In order to derive the family of Rings, we start with the idea of an indempotent function. An Idempotent function is one which, when applied multiple times on an initial input produces the same result. That is, if 𝔽 is a function $ 𝔽 : ϕ → ϕ $ then it’s repeated application $ 𝔽(𝔽(𝔽(…𝔽(x)…))) == 𝔽(x) $.

  _IdempotentOn_ : ★ A  A  Set _
  __ IdempotentOn x = (x ∙ x) == x

  Idempotent : ★ A  Set _
  Idempotent ∙ =  x  ∙ IdempotentOn x

  IdempotentFunction : ♠ A  Set _
  IdempotentFunction f =  x  f (f x) == f x

Near-Semiring

We define a Near-Semiring as the most abstract structure in the family of rings. It is a structure containing:

where the structure defined on the operations are:

  1. $ 𝕊 $ is an monoid under addition, which implies the operation +:
  2. $ 𝕊 $ is a semigroup under multiplication, which implies the operation *:
  3. Multiplication is distributive over addition
  4. There must be an annihilating element 𝕖 such that $ ∀ x : 𝕖 * x = 𝕖 $
  record IsNearSemiring (+ * : ★ A) (0# : A) : Set (a ⊔ ℓ) where
    field
      +-isMonoid    : IsMonoid + 0#
      *-isSemigroup : IsSemigroup *
      distribʳ      : * DistributesOverʳ +
      zeroˡ         : LeftZero 0# *

    open IsMonoid +-isMonoid public
      renaming
      ( assoc       to +-assoc
      ; ∙-cong      to +-cong
      ; ∙-congˡ     to +-congˡ
      ; ∙-congʳ     to +-congʳ
      ; identity    to +-identity
      ; identityˡ   to +-identityˡ
      ; identityʳ   to +-identityʳ
      ; isMagma     to +-isMagma
      ; isSemigroup to +-isSemigroup
      )

    open IsSemigroup *-isSemigroup public
      using ()
      renaming
      ( assoc    to *-assoc
      ; ∙-cong   to *-cong
      ; ∙-congˡ  to *-congˡ
      ; ∙-congʳ  to *-congʳ
      ; isMagma  to *-isMagma
      )

Semiring

A Semiring is a structure containing:

where the structure defined on the operations are:

  1. $ 𝕊 $ is an commutative monoid under addition, which implies the operation +:
  2. $ 𝕊 $ is a monoid under multiplication, which implies the operation *:
  3. Multiplication is distributive over addition
  4. There must be an annihilating element 𝕖 such that $ ∀ x : 𝕖 * x = 𝕖 $

These laws are the same as that of a ring, except for the requirement of addition to have an inverse operation. It is easier to first describe the semiring with the annihilation element:

  record IsSemiringWithoutOne (+ * : ★ A) (0# : A) : Set (a ⊔ ℓ) where
    field
      +-isCommutativeMonoid : IsCommutativeMonoid + 0#
      *-isSemigroup         : IsSemigroup *
      distrib               : * DistributesOver +
      zero                  : Zero 0# *

    open IsCommutativeMonoid +-isCommutativeMonoid public
      using ()
      renaming
      ( isMonoid    to +-isMonoid
      ; comm        to +-comm
      )

    zeroˡ : LeftZero 0# *
    zeroˡ = fst zero

    zeroʳ : RightZero 0# *
    zeroʳ = snd zero

    isNearSemiring : IsNearSemiring + * 0#
    isNearSemiring = record
      { +-isMonoid    = +-isMonoid
      ; *-isSemigroup = *-isSemigroup
      ; distribʳ      = snd distrib
      ; zeroˡ         = zeroˡ
      }

    open IsNearSemiring isNearSemiring public
      hiding (+-isMonoid; zeroˡ)


  record IsSemiringWithoutAnnihilatingZero
    (+ * : ★ A) (0# 1# : A) : Set (a ⊔ ℓ) where

    field
      -- 0# is the identity element of *
      -- 1# is the identity element of +
      +-isCommutativeMonoid : IsCommutativeMonoid + 0#
      *-isMonoid            : IsMonoid * 1#
      distrib               : * DistributesOver +

    open IsCommutativeMonoid +-isCommutativeMonoid public
      renaming
      ( assoc       to +-assoc
      ; ∙-cong      to +-cong
      ; ∙-congˡ     to +-congˡ
      ; ∙-congʳ     to +-congʳ
      ; identity    to +-identity
      ; identityˡ   to +-identityˡ
      ; identityʳ   to +-identityʳ
      ; comm        to +-comm
      ; isMagma     to +-isMagma
      ; isSemigroup to +-isSemigroup
      ; isMonoid    to +-isMonoid
      )

    open IsMonoid *-isMonoid public
      using ()
      renaming
      ( assoc       to *-assoc
      ; ∙-cong      to *-cong
      ; ∙-congˡ     to *-congˡ
      ; ∙-congʳ     to *-congʳ
      ; identity    to *-identity
      ; identityˡ   to *-identityˡ
      ; identityʳ   to *-identityʳ
      ; isMagma     to *-isMagma
      ; isSemigroup to *-isSemigroup
      )

And now the complete definition:

  record IsSemiring (+ * : ★ A) (0# 1# : A) : Set (a ⊔ ℓ) where
    field
      isSemiringWithoutAnnihilatingZero :
        IsSemiringWithoutAnnihilatingZero + * 0# 1#
      zero : Zero 0# *

    open IsSemiringWithoutAnnihilatingZero
           isSemiringWithoutAnnihilatingZero public

    isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
    isSemiringWithoutOne = record
      { +-isCommutativeMonoid = +-isCommutativeMonoid
      ; *-isSemigroup         = *-isSemigroup
      ; distrib               = distrib
      ; zero                  = zero
      }

    open IsSemiringWithoutOne isSemiringWithoutOne public
      using
      ( isNearSemiring
      ; zeroˡ
      ; zeroʳ
      )

We can add commutativity of multiplication to the above structures to obtain their commutative versions.

Commutative Semiring

A Commutative Semiring is a structure containing:

where the structure defined on the operations are:

  1. $ 𝕊 $ is an commutative monoid under addition, which implies the operation +:
  2. $ 𝕊 $ is a commutative monoid under multiplication, which implies the operation *:
  3. Multiplication is distributive over addition
  4. There must be an annihilating element 𝕖 such that $ ∀ x : 𝕖 * x = 𝕖 $
  record IsCommutativeSemiringWithoutOne
           (+ * : ★ A) (0# : A) : Set (a ⊔ ℓ) where
    field
      isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
      *-comm               : Commutative *

    open IsSemiringWithoutOne isSemiringWithoutOne public

  record IsCommutativeSemiring (+ * : ★ A) (0# 1# : A) : Set (a ⊔ ℓ) where
    field
      +-isCommutativeMonoid : IsCommutativeMonoid + 0#
      *-isCommutativeMonoid : IsCommutativeMonoid * 1#
      distrib               : * DistributesOver +
      zero                  : Zero 0# *

    private
      module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
      open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
             using () renaming (comm to *-comm)

    distribˡ : * DistributesOverˡ +
    distribˡ = fst distrib

    distribʳ : * DistributesOverʳ +
    distribʳ = snd distrib

    zeroʳ : RightZero 0# *
    zeroʳ = snd zero

    zeroˡ : RightZero 0# *
    zeroˡ = snd zero

    isSemiring : IsSemiring + * 0# 1#
    isSemiring = record
      { isSemiringWithoutAnnihilatingZero = record
        { +-isCommutativeMonoid = +-isCommutativeMonoid
        ; *-isMonoid            = *-CM.isMonoid
        ; distrib               = distrib
        }
      ; zero                    = zero
      }

    open IsSemiring isSemiring public
      hiding
      ( distrib; zero; zeroˡ; zeroʳ
      ; +-isCommutativeMonoid
      )

    isCommutativeSemiringWithoutOne :
      IsCommutativeSemiringWithoutOne + * 0#
    isCommutativeSemiringWithoutOne = record
      { isSemiringWithoutOne = isSemiringWithoutOne
      ; *-comm               = *-CM.comm
      }

Ring

We now define a ring in Agda:

  record IsRing (+ * : ★ A) (-_ : ♠ A) (0# 1# : A) : Set (a ⊔ ℓ) where
    field
      +-isAbelianGroup : IsAbelianGroup + 0# -_
      *-isMonoid       : IsMonoid * 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 IsMonoid *-isMonoid public
      using ()
      renaming
      ( assoc       to *-assoc
      ; ∙-cong      to *-cong
      ; ∙-congˡ     to *-congˡ
      ; ∙-congʳ     to *-congʳ
      ; identity    to *-identity
      ; identityˡ   to *-identityˡ
      ; identityʳ   to *-identityʳ
      ; isMagma     to *-isMagma
      ; isSemigroup to *-isSemigroup
      )

    distribˡ : * DistributesOverˡ +
    distribˡ = fst distrib

    distribʳ : * DistributesOverʳ +
    distribʳ = snd distrib

    isSemiringWithoutAnnihilatingZero
      : IsSemiringWithoutAnnihilatingZero + * 0# 1#
    isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = +-isCommutativeMonoid
      ; *-isMonoid            = *-isMonoid
      ; distrib               = distrib
      }

    isSemiring : IsSemiring + * 0# 1#
    isSemiring = record
      { isSemiringWithoutAnnihilatingZero =
          isSemiringWithoutAnnihilatingZero
      ; zero = zero
      }

    open IsSemiring isSemiring public
      using (distrib; isNearSemiring; isSemiringWithoutOne)

and finally, the commutative ring:

  record IsCommutativeRing
           (+ * : ★ A) (- : ♠ A) (0# 1# : A) : Set (a ⊔ ℓ) where
    field
      isRing : IsRing + * - 0# 1#
      *-comm : Commutative *

    open IsRing isRing public

    *-isCommutativeMonoid : IsCommutativeMonoid * 1#
    *-isCommutativeMonoid =  record
      { isSemigroup = *-isSemigroup
      ; identityˡ   = *-identityˡ
      ; identityʳ   = *-identityʳ
      ; comm        = *-comm
      }

    isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
    isCommutativeSemiring = record
      { +-isCommutativeMonoid = +-isCommutativeMonoid
      ; *-isCommutativeMonoid = *-isCommutativeMonoid
      ; distrib               = (distribˡ , distribʳ)
      ; zero                  = zero
      }

    open IsCommutativeSemiring isCommutativeSemiring public
      using ( isCommutativeSemiringWithoutOne )

Rings and family 2