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.

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 + 0#
+-isMonoid : IsSemigroup *
*-isSemigroup : * DistributesOverʳ +
distribʳ : LeftZero 0# *
zeroˡ
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
)
```

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 + 0#
+-isCommutativeMonoid : IsSemigroup *
*-isSemigroup : * DistributesOver +
distrib : Zero 0# *
zero
open IsCommutativeMonoid +-isCommutativeMonoid public
using ()
renaming
( isMonoid to +-isMonoid
; comm to +-comm
)
: LeftZero 0# *
zeroˡ = fst zero
zeroˡ
: RightZero 0# *
zeroʳ = snd zero
zeroʳ
: IsNearSemiring + * 0#
isNearSemiring = record
isNearSemiring { +-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 + 0#
+-isCommutativeMonoid : IsMonoid * 1#
*-isMonoid : * DistributesOver +
distrib
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 0# *
zero
open IsSemiringWithoutAnnihilatingZero
public
isSemiringWithoutAnnihilatingZero
: IsSemiringWithoutOne + * 0#
isSemiringWithoutOne = record
isSemiringWithoutOne { +-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.

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 + * 0#
isSemiringWithoutOne : Commutative *
*-comm
open IsSemiringWithoutOne isSemiringWithoutOne public
record IsCommutativeSemiring (+ * : ★ A) (0# 1# : A) : Set (a ⊔ ℓ) where
field
: IsCommutativeMonoid + 0#
+-isCommutativeMonoid : IsCommutativeMonoid * 1#
*-isCommutativeMonoid : * DistributesOver +
distrib : Zero 0# *
zero
private
module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
using () renaming (comm to *-comm)
: * DistributesOverˡ +
distribˡ = fst distrib
distribˡ
: * DistributesOverʳ +
distribʳ = snd distrib
distribʳ
: RightZero 0# *
zeroʳ = snd zero
zeroʳ
: RightZero 0# *
zeroˡ = snd zero
zeroˡ
: IsSemiring + * 0# 1#
isSemiring = record
isSemiring { isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-isCommutativeMonoid
; *-isMonoid = *-CM.isMonoid
; distrib = distrib
}
; zero = zero
}
open IsSemiring isSemiring public
hiding
( distrib; zero; zeroˡ; zeroʳ
; +-isCommutativeMonoid
)
:
isCommutativeSemiringWithoutOne
IsCommutativeSemiringWithoutOne + * 0#= record
isCommutativeSemiringWithoutOne { isSemiringWithoutOne = isSemiringWithoutOne
; *-comm = *-CM.comm
}
```

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 + 0# -_
+-isAbelianGroup : IsMonoid * 1#
*-isMonoid : * 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 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
)
: * DistributesOverˡ +
distribˡ = fst distrib
distribˡ
: * DistributesOverʳ +
distribʳ = snd distrib
distribʳ
isSemiringWithoutAnnihilatingZero: IsSemiringWithoutAnnihilatingZero + * 0# 1#
= record
isSemiringWithoutAnnihilatingZero { +-isCommutativeMonoid = +-isCommutativeMonoid
; *-isMonoid = *-isMonoid
; distrib = distrib
}
: IsSemiring + * 0# 1#
isSemiring = record
isSemiring { 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 + * - 0# 1#
isRing : Commutative *
*-comm
open IsRing isRing public
: IsCommutativeMonoid * 1#
*-isCommutativeMonoid = record
*-isCommutativeMonoid { isMonoid = *-isMonoid
; comm = *-comm
}
: IsCommutativeSemiring + * 0# 1#
isCommutativeSemiring = record
isCommutativeSemiring { +-isCommutativeMonoid = +-isCommutativeMonoid
; *-isCommutativeMonoid = *-isCommutativeMonoid
; distrib = (distribˡ , distribʳ)
; zero = zero
}
open IsCommutativeSemiring isCommutativeSemiring public
using ( isCommutativeSemiringWithoutOne )
```