Rings

Rings

A ring is a structure containing:

A set \(𝕊\)
Two binary operations: + and −

where the structure defined on the operations are:

\(𝕊\) is an abelian group under addition, which implies the operation +:
- is associative
- is commutative
- has an inverse (−)
- has an identity
\(𝕊\) is a monoid under multiplication, which implies the operation ★:
- is associative
- has an identity
Multiplication is distributive over addition
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.relations
open import Types.equality

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

The family of rings consist of a set and two binary operations. Each binary operation behaves in a certain way with the set, taking upon roles from the group family, e.g. one operation can behave like a monoid with respect to the set while the other one can behave like a group.

Object ↓ Operation →	`+` behaves as	`*` behaves as
Near-Semiring	Monoid	Semigroup
Semiring	Commutative Monoid	Monoid
Commutative Semiring	Commutative Monoid	Commutative Monoid
Ring	Abelian Group	Monoid

The * operation interacts with the + operation by folowing the law of distributivity.

Near-Semiring

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

A set \(𝕊\)
Two binary operations: + and *

where the structure defined on the operations are:

\(𝕊\) is an monoid under addition, which implies the operation +:
- is associative
- has an identity
\(𝕊\) is a semigroup under multiplication, which implies the operation *:
- is associative
Multiplication is distributive over addition
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:

A set \(𝕊\)
Two binary operations: + and *

where the structure defined on the operations are:

\(𝕊\) is an commutative monoid under addition, which implies the operation +:
- is associative
- is commutative
- has an identity
\(𝕊\) is a monoid under multiplication, which implies the operation *:
- is associative
- has an identity
Multiplication is distributive over addition
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:

A set \(𝕊\)
Two binary operations: + and *

where the structure defined on the operations are:

\(𝕊\) is an commutative monoid under addition, which implies the operation +:
- is associative
- is commutative
- has an identity
\(𝕊\) is a commutative monoid under multiplication, which implies the operation *:
- is associative
- is commutative
- has an identity
Multiplication is distributive over addition
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

A Ring is a structure containing:

A set \(𝕊\)
Two binary operations: + and *

where the structure defined on the operations are:

\(𝕊\) is an abelian group under addition, which implies the operation +:
- is associative
- is commutative
- has an identity
- has an inverse (-)
\(𝕊\) is a monoid under multiplication, which implies the operation *:
- is associative
- has an identity
Multiplication is distributive over addition
There must be an annihilating element 𝕖 such that \(∀ x : 𝕖 * x = 𝕖\)

  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
      { isMonoid    = *-isMonoid
      ; 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