Commutative rings

module commutative-algebra.commutative-rings where
Imports
open import commutative-algebra.commutative-semirings

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

open import foundation.binary-embeddings
open import foundation.binary-equivalences
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.interchange-law
open import foundation.involutions
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.abelian-groups
open import group-theory.commutative-monoids
open import group-theory.groups
open import group-theory.monoids
open import group-theory.semigroups

open import lists.concatenation-lists
open import lists.lists

open import ring-theory.rings
open import ring-theory.semirings

Idea

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

Definition

Commutative rings

is-commutative-Ring :
  { l : Level}  Ring l  UU l
is-commutative-Ring A =
  (x y : type-Ring A)  mul-Ring A x y  mul-Ring A y x

is-prop-is-commutative-Ring :
  { l : Level} (A : Ring l)  is-prop (is-commutative-Ring A)
is-prop-is-commutative-Ring A =
  is-prop-Π
    ( λ x 
      is-prop-Π
      ( λ y 
        is-set-type-Ring A (mul-Ring A x y) (mul-Ring A y x)))

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

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

  ring-Commutative-Ring : Ring l
  ring-Commutative-Ring = pr1 A

  ab-Commutative-Ring : Ab l
  ab-Commutative-Ring = ab-Ring ring-Commutative-Ring

  set-Commutative-Ring : Set l
  set-Commutative-Ring = set-Ring ring-Commutative-Ring

  type-Commutative-Ring : UU l
  type-Commutative-Ring = type-Ring ring-Commutative-Ring

  is-set-type-Commutative-Ring : is-set type-Commutative-Ring
  is-set-type-Commutative-Ring = is-set-type-Ring ring-Commutative-Ring

Addition in a commutative ring

  has-associative-add-Commutative-Ring :
    has-associative-mul-Set set-Commutative-Ring
  has-associative-add-Commutative-Ring =
    has-associative-add-Ring ring-Commutative-Ring

  add-Commutative-Ring :
    type-Commutative-Ring  type-Commutative-Ring  type-Commutative-Ring
  add-Commutative-Ring = add-Ring ring-Commutative-Ring

  add-Commutative-Ring' :
    type-Commutative-Ring  type-Commutative-Ring  type-Commutative-Ring
  add-Commutative-Ring' = add-Ring' ring-Commutative-Ring

  ap-add-Commutative-Ring :
    {x x' y y' : type-Commutative-Ring} 
    (x  x')  (y  y') 
    add-Commutative-Ring x y  add-Commutative-Ring x' y'
  ap-add-Commutative-Ring = ap-add-Ring ring-Commutative-Ring

  associative-add-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    ( add-Commutative-Ring (add-Commutative-Ring x y) z) 
    ( add-Commutative-Ring x (add-Commutative-Ring y z))
  associative-add-Commutative-Ring =
    associative-add-Ring ring-Commutative-Ring

  additive-semigroup-Commutative-Ring : Semigroup l
  additive-semigroup-Commutative-Ring = semigroup-Ab ab-Commutative-Ring

  is-group-additive-semigroup-Commutative-Ring :
    is-group additive-semigroup-Commutative-Ring
  is-group-additive-semigroup-Commutative-Ring =
    is-group-Ab ab-Commutative-Ring

  commutative-add-Commutative-Ring :
    (x y : type-Commutative-Ring) 
    Id (add-Commutative-Ring x y) (add-Commutative-Ring y x)
  commutative-add-Commutative-Ring = commutative-add-Ab ab-Commutative-Ring

  interchange-add-add-Commutative-Ring :
    (x y x' y' : type-Commutative-Ring) 
    ( add-Commutative-Ring
      ( add-Commutative-Ring x y)
      ( add-Commutative-Ring x' y')) 
    ( add-Commutative-Ring
      ( add-Commutative-Ring x x')
      ( add-Commutative-Ring y y'))
  interchange-add-add-Commutative-Ring =
    interchange-add-add-Ring ring-Commutative-Ring

  right-swap-add-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    ( add-Commutative-Ring (add-Commutative-Ring x y) z) 
    ( add-Commutative-Ring (add-Commutative-Ring x z) y)
  right-swap-add-Commutative-Ring =
    right-swap-add-Ring ring-Commutative-Ring

  left-swap-add-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    ( add-Commutative-Ring x (add-Commutative-Ring y z)) 
    ( add-Commutative-Ring y (add-Commutative-Ring x z))
  left-swap-add-Commutative-Ring =
    left-swap-add-Ring ring-Commutative-Ring

  is-equiv-add-Commutative-Ring :
    (x : type-Commutative-Ring)  is-equiv (add-Commutative-Ring x)
  is-equiv-add-Commutative-Ring = is-equiv-add-Ab ab-Commutative-Ring

  is-equiv-add-Commutative-Ring' :
    (x : type-Commutative-Ring)  is-equiv (add-Commutative-Ring' x)
  is-equiv-add-Commutative-Ring' = is-equiv-add-Ab' ab-Commutative-Ring

  is-binary-equiv-add-Commutative-Ring : is-binary-equiv add-Commutative-Ring
  pr1 is-binary-equiv-add-Commutative-Ring = is-equiv-add-Commutative-Ring'
  pr2 is-binary-equiv-add-Commutative-Ring = is-equiv-add-Commutative-Ring

  is-binary-emb-add-Commutative-Ring : is-binary-emb add-Commutative-Ring
  is-binary-emb-add-Commutative-Ring = is-binary-emb-add-Ab ab-Commutative-Ring

  is-emb-add-Commutative-Ring :
    (x : type-Commutative-Ring)  is-emb (add-Commutative-Ring x)
  is-emb-add-Commutative-Ring = is-emb-add-Ab ab-Commutative-Ring

  is-emb-add-Commutative-Ring' :
    (x : type-Commutative-Ring)  is-emb (add-Commutative-Ring' x)
  is-emb-add-Commutative-Ring' = is-emb-add-Ab' ab-Commutative-Ring

  is-injective-add-Commutative-Ring :
    (x : type-Commutative-Ring)  is-injective (add-Commutative-Ring x)
  is-injective-add-Commutative-Ring = is-injective-add-Ab ab-Commutative-Ring

  is-injective-add-Commutative-Ring' :
    (x : type-Commutative-Ring)  is-injective (add-Commutative-Ring' x)
  is-injective-add-Commutative-Ring' = is-injective-add-Ab' ab-Commutative-Ring

The zero element of a commutative ring

  has-zero-Commutative-Ring : is-unital add-Commutative-Ring
  has-zero-Commutative-Ring = has-zero-Ring ring-Commutative-Ring

  zero-Commutative-Ring : type-Commutative-Ring
  zero-Commutative-Ring = zero-Ring ring-Commutative-Ring

  is-zero-Commutative-Ring : type-Commutative-Ring  UU l
  is-zero-Commutative-Ring = is-zero-Ring ring-Commutative-Ring

  is-nonzero-Commutative-Ring : type-Commutative-Ring  UU l
  is-nonzero-Commutative-Ring = is-nonzero-Ring ring-Commutative-Ring

  is-zero-commutative-ring-Prop : type-Commutative-Ring  Prop l
  is-zero-commutative-ring-Prop x =
    Id-Prop set-Commutative-Ring x zero-Commutative-Ring

  is-nonzero-commutative-ring-Prop : type-Commutative-Ring  Prop l
  is-nonzero-commutative-ring-Prop x =
    neg-Prop (is-zero-commutative-ring-Prop x)

  left-unit-law-add-Commutative-Ring :
    (x : type-Commutative-Ring) 
    add-Commutative-Ring zero-Commutative-Ring x  x
  left-unit-law-add-Commutative-Ring =
    left-unit-law-add-Ring ring-Commutative-Ring

  right-unit-law-add-Commutative-Ring :
    (x : type-Commutative-Ring) 
    add-Commutative-Ring x zero-Commutative-Ring  x
  right-unit-law-add-Commutative-Ring =
    right-unit-law-add-Ring ring-Commutative-Ring

Additive inverses in a commutative ring

  has-negatives-Commutative-Ring :
    is-group' additive-semigroup-Commutative-Ring has-zero-Commutative-Ring
  has-negatives-Commutative-Ring = has-negatives-Ab ab-Commutative-Ring

  neg-Commutative-Ring : type-Commutative-Ring  type-Commutative-Ring
  neg-Commutative-Ring = neg-Ring ring-Commutative-Ring

  left-inverse-law-add-Commutative-Ring :
    (x : type-Commutative-Ring) 
    add-Commutative-Ring (neg-Commutative-Ring x) x  zero-Commutative-Ring
  left-inverse-law-add-Commutative-Ring =
    left-inverse-law-add-Ring ring-Commutative-Ring

  right-inverse-law-add-Commutative-Ring :
    (x : type-Commutative-Ring) 
    add-Commutative-Ring x (neg-Commutative-Ring x)  zero-Commutative-Ring
  right-inverse-law-add-Commutative-Ring =
    right-inverse-law-add-Ring ring-Commutative-Ring

  neg-neg-Commutative-Ring :
    (x : type-Commutative-Ring) 
    neg-Commutative-Ring (neg-Commutative-Ring x)  x
  neg-neg-Commutative-Ring = neg-neg-Ab ab-Commutative-Ring

  distributive-neg-add-Commutative-Ring :
    (x y : type-Commutative-Ring) 
    neg-Commutative-Ring (add-Commutative-Ring x y) 
    add-Commutative-Ring (neg-Commutative-Ring x) (neg-Commutative-Ring y)
  distributive-neg-add-Commutative-Ring =
    distributive-neg-add-Ab ab-Commutative-Ring

Multiplication in a commutative ring

  has-associative-mul-Commutative-Ring :
    has-associative-mul-Set set-Commutative-Ring
  has-associative-mul-Commutative-Ring =
    has-associative-mul-Ring ring-Commutative-Ring

  mul-Commutative-Ring : (x y : type-Commutative-Ring)  type-Commutative-Ring
  mul-Commutative-Ring = mul-Ring ring-Commutative-Ring

  mul-Commutative-Ring' : (x y : type-Commutative-Ring)  type-Commutative-Ring
  mul-Commutative-Ring' = mul-Ring' ring-Commutative-Ring

  ap-mul-Commutative-Ring :
    {x x' y y' : type-Commutative-Ring} (p : Id x x') (q : Id y y') 
    Id (mul-Commutative-Ring x y) (mul-Commutative-Ring x' y')
  ap-mul-Commutative-Ring p q = ap-binary mul-Commutative-Ring p q

  associative-mul-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    mul-Commutative-Ring (mul-Commutative-Ring x y) z 
    mul-Commutative-Ring x (mul-Commutative-Ring y z)
  associative-mul-Commutative-Ring =
    associative-mul-Ring ring-Commutative-Ring

  multiplicative-semigroup-Commutative-Ring : Semigroup l
  pr1 multiplicative-semigroup-Commutative-Ring = set-Commutative-Ring
  pr2 multiplicative-semigroup-Commutative-Ring =
    has-associative-mul-Commutative-Ring

  left-distributive-mul-add-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    ( mul-Commutative-Ring x (add-Commutative-Ring y z)) 
    ( add-Commutative-Ring
      ( mul-Commutative-Ring x y)
      ( mul-Commutative-Ring x z))
  left-distributive-mul-add-Commutative-Ring =
    left-distributive-mul-add-Ring ring-Commutative-Ring

  right-distributive-mul-add-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    ( mul-Commutative-Ring (add-Commutative-Ring x y) z) 
    ( add-Commutative-Ring
      ( mul-Commutative-Ring x z)
      ( mul-Commutative-Ring y z))
  right-distributive-mul-add-Commutative-Ring =
    right-distributive-mul-add-Ring ring-Commutative-Ring

  commutative-mul-Commutative-Ring :
    (x y : type-Commutative-Ring) 
    mul-Commutative-Ring x y  mul-Commutative-Ring y x
  commutative-mul-Commutative-Ring = pr2 A

Multiplicative units in a commutative ring

  is-unital-Commutative-Ring : is-unital mul-Commutative-Ring
  is-unital-Commutative-Ring = is-unital-Ring ring-Commutative-Ring

  multiplicative-monoid-Commutative-Ring : Monoid l
  multiplicative-monoid-Commutative-Ring =
    multiplicative-monoid-Ring ring-Commutative-Ring

  one-Commutative-Ring : type-Commutative-Ring
  one-Commutative-Ring = one-Ring ring-Commutative-Ring

  left-unit-law-mul-Commutative-Ring :
    (x : type-Commutative-Ring) 
    mul-Commutative-Ring one-Commutative-Ring x  x
  left-unit-law-mul-Commutative-Ring =
    left-unit-law-mul-Ring ring-Commutative-Ring

  right-unit-law-mul-Commutative-Ring :
    (x : type-Commutative-Ring) 
    mul-Commutative-Ring x one-Commutative-Ring  x
  right-unit-law-mul-Commutative-Ring =
    right-unit-law-mul-Ring ring-Commutative-Ring

  right-swap-mul-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    mul-Commutative-Ring (mul-Commutative-Ring x y) z 
    mul-Commutative-Ring (mul-Commutative-Ring x z) y
  right-swap-mul-Commutative-Ring x y z =
    ( associative-mul-Commutative-Ring x y z) 
    ( ( ap
        ( mul-Commutative-Ring x)
        ( commutative-mul-Commutative-Ring y z)) 
      ( inv (associative-mul-Commutative-Ring x z y)))

  left-swap-mul-Commutative-Ring :
    (x y z : type-Commutative-Ring) 
    mul-Commutative-Ring x (mul-Commutative-Ring y z) 
    mul-Commutative-Ring y (mul-Commutative-Ring x z)
  left-swap-mul-Commutative-Ring x y z =
    ( inv (associative-mul-Commutative-Ring x y z)) 
    ( ( ap
        ( mul-Commutative-Ring' z)
        ( commutative-mul-Commutative-Ring x y)) 
      ( associative-mul-Commutative-Ring y x z))

  interchange-mul-mul-Commutative-Ring :
    (x y z w : type-Commutative-Ring) 
    mul-Commutative-Ring
      ( mul-Commutative-Ring x y)
      ( mul-Commutative-Ring z w) 
    mul-Commutative-Ring
      ( mul-Commutative-Ring x z)
      ( mul-Commutative-Ring y w)
  interchange-mul-mul-Commutative-Ring =
    interchange-law-commutative-and-associative
      mul-Commutative-Ring
      commutative-mul-Commutative-Ring
      associative-mul-Commutative-Ring

The zero laws for multiplication of a commutative ring

  left-zero-law-mul-Commutative-Ring :
    (x : type-Commutative-Ring) 
    mul-Commutative-Ring zero-Commutative-Ring x 
    zero-Commutative-Ring
  left-zero-law-mul-Commutative-Ring =
    left-zero-law-mul-Ring ring-Commutative-Ring

  right-zero-law-mul-Commutative-Ring :
    (x : type-Commutative-Ring) 
    mul-Commutative-Ring x zero-Commutative-Ring 
    zero-Commutative-Ring
  right-zero-law-mul-Commutative-Ring =
    right-zero-law-mul-Ring ring-Commutative-Ring

Commutative rings are commutative semirings

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

  semiring-Commutative-Ring : Semiring l
  semiring-Commutative-Ring = semiring-Ring ring-Commutative-Ring

  commutative-semiring-Commutative-Ring : Commutative-Semiring l
  pr1 commutative-semiring-Commutative-Ring = semiring-Commutative-Ring
  pr2 commutative-semiring-Commutative-Ring = commutative-mul-Commutative-Ring

Computing multiplication with minus one in a ring

  neg-one-Commutative-Ring : type-Commutative-Ring
  neg-one-Commutative-Ring = neg-one-Ring ring-Commutative-Ring

  mul-neg-one-Commutative-Ring :
    (x : type-Commutative-Ring) 
    mul-Commutative-Ring neg-one-Commutative-Ring x 
    neg-Commutative-Ring x
  mul-neg-one-Commutative-Ring = mul-neg-one-Ring ring-Commutative-Ring

  mul-neg-one-Commutative-Ring' :
    (x : type-Commutative-Ring) 
    mul-Commutative-Ring x neg-one-Commutative-Ring 
    neg-Commutative-Ring x
  mul-neg-one-Commutative-Ring' = mul-neg-one-Ring' ring-Commutative-Ring

  is-involution-mul-neg-one-Commutative-Ring :
    is-involution (mul-Commutative-Ring neg-one-Commutative-Ring)
  is-involution-mul-neg-one-Commutative-Ring =
    is-involution-mul-neg-one-Ring ring-Commutative-Ring

  is-involution-mul-neg-one-Commutative-Ring' :
    is-involution (mul-Commutative-Ring' neg-one-Commutative-Ring)
  is-involution-mul-neg-one-Commutative-Ring' =
    is-involution-mul-neg-one-Ring' ring-Commutative-Ring

Left and right negative laws for multiplication

  left-negative-law-mul-Commutative-Ring :
    (x y : type-Commutative-Ring) 
    mul-Commutative-Ring (neg-Commutative-Ring x) y 
    neg-Commutative-Ring (mul-Commutative-Ring x y)
  left-negative-law-mul-Commutative-Ring =
    left-negative-law-mul-Ring ring-Commutative-Ring

  right-negative-law-mul-Commutative-Ring :
    (x y : type-Commutative-Ring) 
    mul-Commutative-Ring x (neg-Commutative-Ring y) 
    neg-Commutative-Ring (mul-Commutative-Ring x y)
  right-negative-law-mul-Commutative-Ring =
    right-negative-law-mul-Ring ring-Commutative-Ring

  mul-neg-Commutative-Ring :
    (x y : type-Commutative-Ring) 
    mul-Commutative-Ring (neg-Commutative-Ring x) (neg-Commutative-Ring y) 
    mul-Commutative-Ring x y
  mul-neg-Commutative-Ring = mul-neg-Ring ring-Commutative-Ring

Scalar multiplication of elements of a commutative ring by natural numbers

  mul-nat-scalar-Commutative-Ring :
      type-Commutative-Ring  type-Commutative-Ring
  mul-nat-scalar-Commutative-Ring =
    mul-nat-scalar-Ring ring-Commutative-Ring

  ap-mul-nat-scalar-Commutative-Ring :
    {m n : } {x y : type-Commutative-Ring} 
    (m  n)  (x  y) 
    mul-nat-scalar-Commutative-Ring m x 
    mul-nat-scalar-Commutative-Ring n y
  ap-mul-nat-scalar-Commutative-Ring =
    ap-mul-nat-scalar-Ring ring-Commutative-Ring

  left-zero-law-mul-nat-scalar-Commutative-Ring :
    (x : type-Commutative-Ring) 
    mul-nat-scalar-Commutative-Ring 0 x  zero-Commutative-Ring
  left-zero-law-mul-nat-scalar-Commutative-Ring =
    left-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring

  right-zero-law-mul-nat-scalar-Commutative-Ring :
    (n : ) 
    mul-nat-scalar-Commutative-Ring n zero-Commutative-Ring 
    zero-Commutative-Ring
  right-zero-law-mul-nat-scalar-Commutative-Ring =
    right-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring

  left-unit-law-mul-nat-scalar-Commutative-Ring :
    (x : type-Commutative-Ring) 
    mul-nat-scalar-Commutative-Ring 1 x  x
  left-unit-law-mul-nat-scalar-Commutative-Ring =
    left-unit-law-mul-nat-scalar-Ring ring-Commutative-Ring

  left-nat-scalar-law-mul-Commutative-Ring :
    (n : ) (x y : type-Commutative-Ring) 
    mul-Commutative-Ring (mul-nat-scalar-Commutative-Ring n x) y 
    mul-nat-scalar-Commutative-Ring n (mul-Commutative-Ring x y)
  left-nat-scalar-law-mul-Commutative-Ring =
    left-nat-scalar-law-mul-Ring ring-Commutative-Ring

  right-nat-scalar-law-mul-Commutative-Ring :
    (n : ) (x y : type-Commutative-Ring) 
    mul-Commutative-Ring x (mul-nat-scalar-Commutative-Ring n y) 
    mul-nat-scalar-Commutative-Ring n (mul-Commutative-Ring x y)
  right-nat-scalar-law-mul-Commutative-Ring =
    right-nat-scalar-law-mul-Ring ring-Commutative-Ring

  left-distributive-mul-nat-scalar-add-Commutative-Ring :
    (n : ) (x y : type-Commutative-Ring) 
    mul-nat-scalar-Commutative-Ring n (add-Commutative-Ring x y) 
    add-Commutative-Ring
      ( mul-nat-scalar-Commutative-Ring n x)
      ( mul-nat-scalar-Commutative-Ring n y)
  left-distributive-mul-nat-scalar-add-Commutative-Ring =
    left-distributive-mul-nat-scalar-add-Ring ring-Commutative-Ring

  right-distributive-mul-nat-scalar-add-Commutative-Ring :
    (m n : ) (x : type-Commutative-Ring) 
    mul-nat-scalar-Commutative-Ring (m +ℕ n) x 
    add-Commutative-Ring
      ( mul-nat-scalar-Commutative-Ring m x)
      ( mul-nat-scalar-Commutative-Ring n x)
  right-distributive-mul-nat-scalar-add-Commutative-Ring =
    right-distributive-mul-nat-scalar-add-Ring ring-Commutative-Ring

Addition of a list of elements in a commutative ring

  add-list-Commutative-Ring : list type-Commutative-Ring  type-Commutative-Ring
  add-list-Commutative-Ring = add-list-Ring ring-Commutative-Ring

  preserves-concat-add-list-Commutative-Ring :
    (l1 l2 : list type-Commutative-Ring) 
    Id ( add-list-Commutative-Ring (concat-list l1 l2))
       ( add-Commutative-Ring
         ( add-list-Commutative-Ring l1)
         ( add-list-Commutative-Ring l2))
  preserves-concat-add-list-Commutative-Ring =
    preserves-concat-add-list-Ring ring-Commutative-Ring