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.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
```

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
)
```

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.

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
}
```

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 )
```