Semirings

module ring-theory.semirings where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.sets
open import foundation.unital-binary-operations
open import foundation.universe-levels

open import group-theory.commutative-monoids
open import group-theory.monoids
open import group-theory.semigroups

Idea

The concept of semiring vastly generalizes the arithmetical structure on the natural numbers. A semiring consists of a set equipped with addition and multiplication, where the addition operation gives the ring the structure of a commutative monoid, and the multiplication is associative, unital, and distributive over addition.

Definitions

Semirings

has-mul-Commutative-Monoid :
  {l : Level} → Commutative-Monoid l → UU l
has-mul-Commutative-Monoid M =
  Σ ( has-associative-mul-Set (set-Commutative-Monoid M))
    ( λ μ →
      ( is-unital (pr1 μ)) ×
      ( ( (a b c : type-Commutative-Monoid M) →
          pr1 μ a (mul-Commutative-Monoid M b c) ＝
          mul-Commutative-Monoid M (pr1 μ a b) (pr1 μ a c)) ×
        ( (a b c : type-Commutative-Monoid M) →
          pr1 μ (mul-Commutative-Monoid M a b) c ＝
          mul-Commutative-Monoid M (pr1 μ a c) (pr1 μ b c))))

zero-laws-Commutative-Monoid :
  {l : Level} (M : Commutative-Monoid l) → has-mul-Commutative-Monoid M → UU l
zero-laws-Commutative-Monoid M ((μ , α) , laws) =
  ( (x : type-Commutative-Monoid M) →
    μ (unit-Commutative-Monoid M) x ＝ unit-Commutative-Monoid M) ×
  ((x : type-Commutative-Monoid M) →
    μ x (unit-Commutative-Monoid M) ＝ unit-Commutative-Monoid M)

Semiring : (l : Level) → UU (lsuc l)
Semiring l1 =
  Σ ( Commutative-Monoid l1)
    ( λ M →
      Σ (has-mul-Commutative-Monoid M) (zero-laws-Commutative-Monoid M))

module _
  {l : Level} (R : Semiring l)
  where

  additive-commutative-monoid-Semiring : Commutative-Monoid l
  additive-commutative-monoid-Semiring = pr1 R

  additive-monoid-Semiring : Monoid l
  additive-monoid-Semiring =
    monoid-Commutative-Monoid additive-commutative-monoid-Semiring

  additive-semigroup-Semiring : Semigroup l
  additive-semigroup-Semiring =
    semigroup-Commutative-Monoid additive-commutative-monoid-Semiring

  set-Semiring : Set l
  set-Semiring =
    set-Commutative-Monoid additive-commutative-monoid-Semiring

  type-Semiring : UU l
  type-Semiring =
    type-Commutative-Monoid additive-commutative-monoid-Semiring

  is-set-type-Semiring : is-set type-Semiring
  is-set-type-Semiring =
    is-set-type-Commutative-Monoid
      ( additive-commutative-monoid-Semiring)

Addition in a semiring

module _
  {l : Level} (R : Semiring l)
  where

  has-associative-add-Semiring : has-associative-mul-Set (set-Semiring R)
  has-associative-add-Semiring =
    has-associative-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

  add-Semiring : type-Semiring R → type-Semiring R → type-Semiring R
  add-Semiring =
    mul-Commutative-Monoid (additive-commutative-monoid-Semiring R)

  add-Semiring' : type-Semiring R → type-Semiring R → type-Semiring R
  add-Semiring' =
    mul-Commutative-Monoid' (additive-commutative-monoid-Semiring R)

  ap-add-Semiring :
    {x y x' y' : type-Semiring R} →
    x ＝ x' → y ＝ y' → add-Semiring x y ＝ add-Semiring x' y'
  ap-add-Semiring =
    ap-mul-Commutative-Monoid (additive-commutative-monoid-Semiring R)

  associative-add-Semiring :
    (x y z : type-Semiring R) →
    add-Semiring (add-Semiring x y) z ＝ add-Semiring x (add-Semiring y z)
  associative-add-Semiring =
    associative-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

  commutative-add-Semiring :
    (x y : type-Semiring R) → add-Semiring x y ＝ add-Semiring y x
  commutative-add-Semiring =
    commutative-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

  interchange-add-add-Semiring :
    (x y x' y' : type-Semiring R) →
    ( add-Semiring (add-Semiring x y) (add-Semiring x' y')) ＝
    ( add-Semiring (add-Semiring x x') (add-Semiring y y'))
  interchange-add-add-Semiring =
    interchange-mul-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

  right-swap-add-Semiring :
    (x y z : type-Semiring R) →
    add-Semiring (add-Semiring x y) z ＝ add-Semiring (add-Semiring x z) y
  right-swap-add-Semiring =
    right-swap-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

  left-swap-add-Semiring :
    (x y z : type-Semiring R) →
    add-Semiring x (add-Semiring y z) ＝ add-Semiring y (add-Semiring x z)
  left-swap-add-Semiring =
    left-swap-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

The zero element of a semiring

module _
  {l : Level} (R : Semiring l)
  where

  has-zero-Semiring : is-unital (add-Semiring R)
  has-zero-Semiring =
    has-unit-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

  zero-Semiring : type-Semiring R
  zero-Semiring =
    unit-Commutative-Monoid (additive-commutative-monoid-Semiring R)

  is-zero-Semiring : type-Semiring R → UU l
  is-zero-Semiring x = Id x zero-Semiring

  is-nonzero-Semiring : type-Semiring R → UU l
  is-nonzero-Semiring x = ¬ (is-zero-Semiring x)

  is-zero-semiring-Prop : type-Semiring R → Prop l
  is-zero-semiring-Prop x = Id-Prop (set-Semiring R) x zero-Semiring

  left-unit-law-add-Semiring :
    (x : type-Semiring R) → Id (add-Semiring R zero-Semiring x) x
  left-unit-law-add-Semiring =
    left-unit-law-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

  right-unit-law-add-Semiring :
    (x : type-Semiring R) → Id (add-Semiring R x zero-Semiring) x
  right-unit-law-add-Semiring =
    right-unit-law-mul-Commutative-Monoid
      ( additive-commutative-monoid-Semiring R)

Multiplication in a semiring

module _
  {l : Level} (R : Semiring l)
  where

  has-associative-mul-Semiring : has-associative-mul-Set (set-Semiring R)
  has-associative-mul-Semiring = pr1 (pr1 (pr2 R))

  mul-Semiring : type-Semiring R → type-Semiring R → type-Semiring R
  mul-Semiring = pr1 has-associative-mul-Semiring

  mul-Semiring' : type-Semiring R → type-Semiring R → type-Semiring R
  mul-Semiring' x y = mul-Semiring y x

  ap-mul-Semiring :
    {x x' y y' : type-Semiring R} (p : Id x x') (q : Id y y') →
    Id (mul-Semiring x y) (mul-Semiring x' y')
  ap-mul-Semiring p q = ap-binary mul-Semiring p q

  associative-mul-Semiring :
    (x y z : type-Semiring R) →
    Id (mul-Semiring (mul-Semiring x y) z) (mul-Semiring x (mul-Semiring y z))
  associative-mul-Semiring = pr2 has-associative-mul-Semiring

  multiplicative-semigroup-Semiring : Semigroup l
  pr1 multiplicative-semigroup-Semiring = set-Semiring R
  pr2 multiplicative-semigroup-Semiring = has-associative-mul-Semiring

  left-distributive-mul-add-Semiring :
    (x y z : type-Semiring R) →
    mul-Semiring x (add-Semiring R y z) ＝
    add-Semiring R (mul-Semiring x y) (mul-Semiring x z)
  left-distributive-mul-add-Semiring =
    pr1 (pr2 (pr2 (pr1 (pr2 R))))

  right-distributive-mul-add-Semiring :
    (x y z : type-Semiring R) →
    Id ( mul-Semiring (add-Semiring R x y) z)
      ( add-Semiring R (mul-Semiring x z) (mul-Semiring y z))
  right-distributive-mul-add-Semiring =
    pr2 (pr2 (pr2 (pr1 (pr2 R))))

  left-zero-law-mul-Semiring :
    (x : type-Semiring R) → mul-Semiring (zero-Semiring R) x ＝ zero-Semiring R
  left-zero-law-mul-Semiring = pr1 (pr2 (pr2 R))

  right-zero-law-mul-Semiring :
    (x : type-Semiring R) → mul-Semiring x (zero-Semiring R) ＝ zero-Semiring R
  right-zero-law-mul-Semiring = pr2 (pr2 (pr2 R))

Multiplicative units in a semiring

module _
  {l : Level} (R : Semiring l)
  where

  is-unital-Semiring : is-unital (mul-Semiring R)
  is-unital-Semiring = pr1 (pr2 (pr1 (pr2 R)))

  multiplicative-monoid-Semiring : Monoid l
  pr1 multiplicative-monoid-Semiring = multiplicative-semigroup-Semiring R
  pr2 multiplicative-monoid-Semiring = is-unital-Semiring

  one-Semiring : type-Semiring R
  one-Semiring = unit-Monoid multiplicative-monoid-Semiring

  left-unit-law-mul-Semiring :
    (x : type-Semiring R) → Id (mul-Semiring R one-Semiring x) x
  left-unit-law-mul-Semiring =
    left-unit-law-mul-Monoid multiplicative-monoid-Semiring

  right-unit-law-mul-Semiring :
    (x : type-Semiring R) → Id (mul-Semiring R x one-Semiring) x
  right-unit-law-mul-Semiring =
    right-unit-law-mul-Monoid multiplicative-monoid-Semiring

Scalar multiplication of semiring elements by natural numbers

module _
  {l : Level} (R : Semiring l)
  where

  mul-nat-scalar-Semiring : ℕ → type-Semiring R → type-Semiring R
  mul-nat-scalar-Semiring zero-ℕ x = zero-Semiring R
  mul-nat-scalar-Semiring (succ-ℕ n) x =
    add-Semiring R (mul-nat-scalar-Semiring n x) x

  ap-mul-nat-scalar-Semiring :
    {m n : ℕ} {x y : type-Semiring R} →
    (m ＝ n) → (x ＝ y) →
    mul-nat-scalar-Semiring m x ＝ mul-nat-scalar-Semiring n y
  ap-mul-nat-scalar-Semiring p q = ap-binary mul-nat-scalar-Semiring p q

  left-zero-law-mul-nat-scalar-Semiring :
    (x : type-Semiring R) → mul-nat-scalar-Semiring 0 x ＝ zero-Semiring R
  left-zero-law-mul-nat-scalar-Semiring x = refl

  right-zero-law-mul-nat-scalar-Semiring :
    (n : ℕ) → mul-nat-scalar-Semiring n (zero-Semiring R) ＝ zero-Semiring R
  right-zero-law-mul-nat-scalar-Semiring zero-ℕ = refl
  right-zero-law-mul-nat-scalar-Semiring (succ-ℕ n) =
    ( right-unit-law-add-Semiring R _) ∙
    ( right-zero-law-mul-nat-scalar-Semiring n)

  left-unit-law-mul-nat-scalar-Semiring :
    (x : type-Semiring R) → mul-nat-scalar-Semiring 1 x ＝ x
  left-unit-law-mul-nat-scalar-Semiring x = left-unit-law-add-Semiring R x

  left-nat-scalar-law-mul-Semiring :
    (n : ℕ) (x y : type-Semiring R) →
    mul-Semiring R (mul-nat-scalar-Semiring n x) y ＝
    mul-nat-scalar-Semiring n (mul-Semiring R x y)
  left-nat-scalar-law-mul-Semiring zero-ℕ x y =
    left-zero-law-mul-Semiring R y
  left-nat-scalar-law-mul-Semiring (succ-ℕ n) x y =
    ( right-distributive-mul-add-Semiring R
      ( mul-nat-scalar-Semiring n x)
      ( x)
      ( y)) ∙
    ( ap
      ( add-Semiring' R (mul-Semiring R x y))
      ( left-nat-scalar-law-mul-Semiring n x y))

  right-nat-scalar-law-mul-Semiring :
    (n : ℕ) (x y : type-Semiring R) →
    mul-Semiring R x (mul-nat-scalar-Semiring n y) ＝
    mul-nat-scalar-Semiring n (mul-Semiring R x y)
  right-nat-scalar-law-mul-Semiring zero-ℕ x y =
    right-zero-law-mul-Semiring R x
  right-nat-scalar-law-mul-Semiring (succ-ℕ n) x y =
    ( left-distributive-mul-add-Semiring R x
      ( mul-nat-scalar-Semiring n y)
      ( y)) ∙
    ( ap
      ( add-Semiring' R (mul-Semiring R x y))
      ( right-nat-scalar-law-mul-Semiring n x y))

  left-distributive-mul-nat-scalar-add-Semiring :
    (n : ℕ) (x y : type-Semiring R) →
    mul-nat-scalar-Semiring n (add-Semiring R x y) ＝
    add-Semiring R (mul-nat-scalar-Semiring n x) (mul-nat-scalar-Semiring n y)
  left-distributive-mul-nat-scalar-add-Semiring zero-ℕ x y =
    inv (left-unit-law-add-Semiring R (zero-Semiring R))
  left-distributive-mul-nat-scalar-add-Semiring (succ-ℕ n) x y =
    ( ap
      ( add-Semiring' R (add-Semiring R x y))
      ( left-distributive-mul-nat-scalar-add-Semiring n x y)) ∙
    ( interchange-add-add-Semiring R
      ( mul-nat-scalar-Semiring n x)
      ( mul-nat-scalar-Semiring n y)
      ( x)
      ( y))

  right-distributive-mul-nat-scalar-add-Semiring :
    (m n : ℕ) (x : type-Semiring R) →
    mul-nat-scalar-Semiring (m +ℕ n) x ＝
    add-Semiring R (mul-nat-scalar-Semiring m x) (mul-nat-scalar-Semiring n x)
  right-distributive-mul-nat-scalar-add-Semiring m zero-ℕ x =
    inv (right-unit-law-add-Semiring R (mul-nat-scalar-Semiring m x))
  right-distributive-mul-nat-scalar-add-Semiring m (succ-ℕ n) x =
    ( ap
      ( add-Semiring' R x)
      ( right-distributive-mul-nat-scalar-add-Semiring m n x)) ∙
    ( associative-add-Semiring R
      ( mul-nat-scalar-Semiring m x)
      ( mul-nat-scalar-Semiring n x) x)