Commutative semirings

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Maša Žaucer.

Created on 2023-02-20.
Last modified on 2024-03-11.

module commutative-algebra.commutative-semirings where

Imports

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

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

open import ring-theory.semirings

Idea

A semiring A is said to be commutative^¶ if its multiplicative operation is commutative, i.e., if xy = yx for all x, y ∈ A.

Definitions

The predicate on semirings of being commutative

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

  is-commutative-Semiring : UU l
  is-commutative-Semiring =
    (x y : type-Semiring A) → mul-Semiring A x y ＝ mul-Semiring A y x

  is-prop-is-commutative-Semiring : is-prop is-commutative-Semiring
  is-prop-is-commutative-Semiring =
    is-prop-iterated-Π 2
      ( λ x y →
        is-set-type-Semiring A (mul-Semiring A x y) (mul-Semiring A y x))

  is-commutative-prop-Semiring : Prop l
  is-commutative-prop-Semiring =
    ( is-commutative-Semiring , is-prop-is-commutative-Semiring)

The type of commutative semirings

Commutative-Semiring :
  ( l : Level) → UU (lsuc l)
Commutative-Semiring l = Σ (Semiring l) is-commutative-Semiring

Immediate infrastructure for commutative semirings

module _
  {l : Level} (A : Commutative-Semiring l)
  where

  semiring-Commutative-Semiring : Semiring l
  semiring-Commutative-Semiring = pr1 A

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

  multiplicative-monoid-Commutative-Semiring : Monoid l
  multiplicative-monoid-Commutative-Semiring =
    multiplicative-monoid-Semiring semiring-Commutative-Semiring

  set-Commutative-Semiring : Set l
  set-Commutative-Semiring = set-Semiring semiring-Commutative-Semiring

  type-Commutative-Semiring : UU l
  type-Commutative-Semiring = type-Semiring semiring-Commutative-Semiring

  is-set-type-Commutative-Semiring : is-set type-Commutative-Semiring
  is-set-type-Commutative-Semiring =
    is-set-type-Semiring semiring-Commutative-Semiring

  zero-Commutative-Semiring : type-Commutative-Semiring
  zero-Commutative-Semiring = zero-Semiring semiring-Commutative-Semiring

  is-zero-Commutative-Semiring : type-Commutative-Semiring → UU l
  is-zero-Commutative-Semiring = is-zero-Semiring semiring-Commutative-Semiring

  is-nonzero-Commutative-Semiring : type-Commutative-Semiring → UU l
  is-nonzero-Commutative-Semiring =
    is-nonzero-Semiring semiring-Commutative-Semiring

  add-Commutative-Semiring :
    type-Commutative-Semiring → type-Commutative-Semiring →
    type-Commutative-Semiring
  add-Commutative-Semiring = add-Semiring semiring-Commutative-Semiring

  add-Commutative-Semiring' :
    type-Commutative-Semiring → type-Commutative-Semiring →
    type-Commutative-Semiring
  add-Commutative-Semiring' = add-Semiring' semiring-Commutative-Semiring

  ap-add-Commutative-Semiring :
    {x x' y y' : type-Commutative-Semiring} →
    (x ＝ x') → (y ＝ y') →
    add-Commutative-Semiring x y ＝ add-Commutative-Semiring x' y'
  ap-add-Commutative-Semiring = ap-add-Semiring semiring-Commutative-Semiring

  associative-add-Commutative-Semiring :
    (x y z : type-Commutative-Semiring) →
    ( add-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
    ( add-Commutative-Semiring x (add-Commutative-Semiring y z))
  associative-add-Commutative-Semiring =
    associative-add-Semiring semiring-Commutative-Semiring

  left-unit-law-add-Commutative-Semiring :
    (x : type-Commutative-Semiring) →
    add-Commutative-Semiring zero-Commutative-Semiring x ＝ x
  left-unit-law-add-Commutative-Semiring =
    left-unit-law-add-Semiring semiring-Commutative-Semiring

  right-unit-law-add-Commutative-Semiring :
    (x : type-Commutative-Semiring) →
    add-Commutative-Semiring x zero-Commutative-Semiring ＝ x
  right-unit-law-add-Commutative-Semiring =
    right-unit-law-add-Semiring semiring-Commutative-Semiring

  commutative-add-Commutative-Semiring :
    (x y : type-Commutative-Semiring) →
    add-Commutative-Semiring x y ＝ add-Commutative-Semiring y x
  commutative-add-Commutative-Semiring =
    commutative-add-Semiring semiring-Commutative-Semiring

  interchange-add-add-Commutative-Semiring :
    (x y x' y' : type-Commutative-Semiring) →
    ( add-Commutative-Semiring
      ( add-Commutative-Semiring x y)
      ( add-Commutative-Semiring x' y')) ＝
    ( add-Commutative-Semiring
      ( add-Commutative-Semiring x x')
      ( add-Commutative-Semiring y y'))
  interchange-add-add-Commutative-Semiring =
    interchange-add-add-Semiring semiring-Commutative-Semiring

  right-swap-add-Commutative-Semiring :
    (x y z : type-Commutative-Semiring) →
    ( add-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
    ( add-Commutative-Semiring (add-Commutative-Semiring x z) y)
  right-swap-add-Commutative-Semiring =
    right-swap-add-Semiring semiring-Commutative-Semiring

  left-swap-add-Commutative-Semiring :
    (x y z : type-Commutative-Semiring) →
    ( add-Commutative-Semiring x (add-Commutative-Semiring y z)) ＝
    ( add-Commutative-Semiring y (add-Commutative-Semiring x z))
  left-swap-add-Commutative-Semiring =
    left-swap-add-Semiring semiring-Commutative-Semiring

  mul-Commutative-Semiring :
    (x y : type-Commutative-Semiring) → type-Commutative-Semiring
  mul-Commutative-Semiring = mul-Semiring semiring-Commutative-Semiring

  mul-Commutative-Semiring' :
    (x y : type-Commutative-Semiring) → type-Commutative-Semiring
  mul-Commutative-Semiring' = mul-Semiring' semiring-Commutative-Semiring

  one-Commutative-Semiring : type-Commutative-Semiring
  one-Commutative-Semiring = one-Semiring semiring-Commutative-Semiring

  left-unit-law-mul-Commutative-Semiring :
    (x : type-Commutative-Semiring) →
    mul-Commutative-Semiring one-Commutative-Semiring x ＝ x
  left-unit-law-mul-Commutative-Semiring =
    left-unit-law-mul-Semiring semiring-Commutative-Semiring

  right-unit-law-mul-Commutative-Semiring :
    (x : type-Commutative-Semiring) →
    mul-Commutative-Semiring x one-Commutative-Semiring ＝ x
  right-unit-law-mul-Commutative-Semiring =
    right-unit-law-mul-Semiring semiring-Commutative-Semiring

  associative-mul-Commutative-Semiring :
    (x y z : type-Commutative-Semiring) →
    mul-Commutative-Semiring (mul-Commutative-Semiring x y) z ＝
    mul-Commutative-Semiring x (mul-Commutative-Semiring y z)
  associative-mul-Commutative-Semiring =
    associative-mul-Semiring semiring-Commutative-Semiring

  left-distributive-mul-add-Commutative-Semiring :
    (x y z : type-Commutative-Semiring) →
    ( mul-Commutative-Semiring x (add-Commutative-Semiring y z)) ＝
    ( add-Commutative-Semiring
      ( mul-Commutative-Semiring x y)
      ( mul-Commutative-Semiring x z))
  left-distributive-mul-add-Commutative-Semiring =
    left-distributive-mul-add-Semiring semiring-Commutative-Semiring

  right-distributive-mul-add-Commutative-Semiring :
    (x y z : type-Commutative-Semiring) →
    ( mul-Commutative-Semiring (add-Commutative-Semiring x y) z) ＝
    ( add-Commutative-Semiring
      ( mul-Commutative-Semiring x z)
      ( mul-Commutative-Semiring y z))
  right-distributive-mul-add-Commutative-Semiring =
    right-distributive-mul-add-Semiring semiring-Commutative-Semiring

  commutative-mul-Commutative-Semiring :
    (x y : type-Commutative-Semiring) →
    mul-Commutative-Semiring x y ＝ mul-Commutative-Semiring y x
  commutative-mul-Commutative-Semiring = pr2 A

  multiplicative-commutative-monoid-Commutative-Semiring :
    Commutative-Monoid l
  pr1 multiplicative-commutative-monoid-Commutative-Semiring =
    multiplicative-monoid-Commutative-Semiring
  pr2 multiplicative-commutative-monoid-Commutative-Semiring =
    commutative-mul-Commutative-Semiring

  left-zero-law-mul-Commutative-Semiring :
    (x : type-Commutative-Semiring) →
    mul-Commutative-Semiring zero-Commutative-Semiring x ＝
    zero-Commutative-Semiring
  left-zero-law-mul-Commutative-Semiring =
    left-zero-law-mul-Semiring semiring-Commutative-Semiring

  right-zero-law-mul-Commutative-Semiring :
    (x : type-Commutative-Semiring) →
    mul-Commutative-Semiring x zero-Commutative-Semiring ＝
    zero-Commutative-Semiring
  right-zero-law-mul-Commutative-Semiring =
    right-zero-law-mul-Semiring semiring-Commutative-Semiring

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

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

Operations

Scalar multiplication of elements of a commutative ring by natural numbers

  mul-nat-scalar-Commutative-Semiring :
    ℕ → type-Commutative-Semiring → type-Commutative-Semiring
  mul-nat-scalar-Commutative-Semiring =
    mul-nat-scalar-Semiring semiring-Commutative-Semiring

  ap-mul-nat-scalar-Commutative-Semiring :
    {m n : ℕ} {x y : type-Commutative-Semiring} →
    (m ＝ n) → (x ＝ y) →
    mul-nat-scalar-Commutative-Semiring m x ＝
    mul-nat-scalar-Commutative-Semiring n y
  ap-mul-nat-scalar-Commutative-Semiring =
    ap-mul-nat-scalar-Semiring semiring-Commutative-Semiring

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

  right-zero-law-mul-nat-scalar-Commutative-Semiring :
    (n : ℕ) →
    mul-nat-scalar-Commutative-Semiring n zero-Commutative-Semiring ＝
    zero-Commutative-Semiring
  right-zero-law-mul-nat-scalar-Commutative-Semiring =
    right-zero-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring

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

  left-nat-scalar-law-mul-Commutative-Semiring :
    (n : ℕ) (x y : type-Commutative-Semiring) →
    mul-Commutative-Semiring (mul-nat-scalar-Commutative-Semiring n x) y ＝
    mul-nat-scalar-Commutative-Semiring n (mul-Commutative-Semiring x y)
  left-nat-scalar-law-mul-Commutative-Semiring =
    left-nat-scalar-law-mul-Semiring semiring-Commutative-Semiring

  right-nat-scalar-law-mul-Commutative-Semiring :
    (n : ℕ) (x y : type-Commutative-Semiring) →
    mul-Commutative-Semiring x (mul-nat-scalar-Commutative-Semiring n y) ＝
    mul-nat-scalar-Commutative-Semiring n (mul-Commutative-Semiring x y)
  right-nat-scalar-law-mul-Commutative-Semiring =
    right-nat-scalar-law-mul-Semiring semiring-Commutative-Semiring

  left-distributive-mul-nat-scalar-add-Commutative-Semiring :
    (n : ℕ) (x y : type-Commutative-Semiring) →
    mul-nat-scalar-Commutative-Semiring n (add-Commutative-Semiring x y) ＝
    add-Commutative-Semiring
      ( mul-nat-scalar-Commutative-Semiring n x)
      ( mul-nat-scalar-Commutative-Semiring n y)
  left-distributive-mul-nat-scalar-add-Commutative-Semiring =
    left-distributive-mul-nat-scalar-add-Semiring semiring-Commutative-Semiring

  right-distributive-mul-nat-scalar-add-Commutative-Semiring :
    (m n : ℕ) (x : type-Commutative-Semiring) →
    mul-nat-scalar-Commutative-Semiring (m +ℕ n) x ＝
    add-Commutative-Semiring
      ( mul-nat-scalar-Commutative-Semiring m x)
      ( mul-nat-scalar-Commutative-Semiring n x)
  right-distributive-mul-nat-scalar-add-Commutative-Semiring =
    right-distributive-mul-nat-scalar-add-Semiring semiring-Commutative-Semiring

Recent changes

2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
2023-05-04. Egbert Rijke. Cleaning up commutative algebra (#589).
2023-03-18. Egbert Rijke and Maša Žaucer. Central elements in semigroups, monoids, groups, semirings, and rings; ideals; nilpotent elements in semirings, rings, commutative semirings, and commutative rings; the nilradical of a commutative ring (#516).
2023-03-14. Fredrik Bakke. Remove all unused imports (#502).