# Commutative rings

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

Created on 2022-04-22.

module commutative-algebra.commutative-rings where

Imports
open import commutative-algebra.commutative-semirings

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
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.function-types
open import foundation.homotopies
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

### The predicate on rings of being commutative

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

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

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

is-commutative-prop-Ring : Prop l
is-commutative-prop-Ring = is-commutative-Ring , is-prop-is-commutative-Ring


### Commutative rings

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

type-Commutative-Ring → type-Commutative-Ring → type-Commutative-Ring

type-Commutative-Ring → type-Commutative-Ring → type-Commutative-Ring

{x x' y y' : type-Commutative-Ring} →
(x ＝ x') → (y ＝ y') →

(x y z : type-Commutative-Ring) →

is-group-Ab ab-Commutative-Ring

(x y : type-Commutative-Ring) →

(x y x' y' : type-Commutative-Ring) →

(x y z : type-Commutative-Ring) →

(x y z : type-Commutative-Ring) →

left-subtraction-Commutative-Ring :
type-Commutative-Ring → type-Commutative-Ring → type-Commutative-Ring
left-subtraction-Commutative-Ring =
left-subtraction-Ring ring-Commutative-Ring

is-section-left-subtraction-Commutative-Ring :
(x : type-Commutative-Ring) →
(add-Commutative-Ring x ∘ left-subtraction-Commutative-Ring x) ~ id
is-section-left-subtraction-Commutative-Ring =
is-section-left-subtraction-Ring ring-Commutative-Ring

is-retraction-left-subtraction-Commutative-Ring :
(x : type-Commutative-Ring) →
(left-subtraction-Commutative-Ring x ∘ add-Commutative-Ring x) ~ id
is-retraction-left-subtraction-Commutative-Ring =
is-retraction-left-subtraction-Ring ring-Commutative-Ring

(x : type-Commutative-Ring) → is-equiv (add-Commutative-Ring x)

type-Commutative-Ring → (type-Commutative-Ring ≃ type-Commutative-Ring)

right-subtraction-Commutative-Ring :
type-Commutative-Ring → type-Commutative-Ring → type-Commutative-Ring
right-subtraction-Commutative-Ring =
right-subtraction-Ring ring-Commutative-Ring

is-section-right-subtraction-Commutative-Ring :
(x : type-Commutative-Ring) →
(λ y → right-subtraction-Commutative-Ring y x)) ~ id
is-section-right-subtraction-Commutative-Ring =
is-section-right-subtraction-Ring ring-Commutative-Ring

is-retraction-right-subtraction-Commutative-Ring :
(x : type-Commutative-Ring) →
( ( λ y → right-subtraction-Commutative-Ring y x) ∘
is-retraction-right-subtraction-Commutative-Ring =
is-retraction-right-subtraction-Ring ring-Commutative-Ring

(x : type-Commutative-Ring) → is-equiv (add-Commutative-Ring' x)

type-Commutative-Ring → (type-Commutative-Ring ≃ type-Commutative-Ring)

(x : type-Commutative-Ring) → is-emb (add-Commutative-Ring x)

(x : type-Commutative-Ring) → is-emb (add-Commutative-Ring' x)

(x : type-Commutative-Ring) → is-injective (add-Commutative-Ring x)

(x : type-Commutative-Ring) → is-injective (add-Commutative-Ring' x)


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

(x : type-Commutative-Ring) →

(x : type-Commutative-Ring) →


### Additive inverses in a commutative ring

  has-negatives-Commutative-Ring :
is-group-is-unital-Semigroup
( 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

(x : type-Commutative-Ring) →
add-Commutative-Ring (neg-Commutative-Ring x) x ＝ zero-Commutative-Ring

(x : type-Commutative-Ring) →
add-Commutative-Ring x (neg-Commutative-Ring x) ＝ zero-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

(x y : type-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

(x y z : type-Commutative-Ring) →
( mul-Commutative-Ring x (add-Commutative-Ring y z)) ＝
( mul-Commutative-Ring x y)
( mul-Commutative-Ring x z))

(x y z : type-Commutative-Ring) →
( mul-Commutative-Ring (add-Commutative-Ring x y) z) ＝
( mul-Commutative-Ring x z)
( mul-Commutative-Ring y z))

(u v x y : type-Commutative-Ring) →
mul-Commutative-Ring
( mul-Commutative-Ring u x)
( mul-Commutative-Ring u y))
( mul-Commutative-Ring v x)
( mul-Commutative-Ring v y))

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


### Distributivity of multiplication over subtraction

  left-distributive-mul-left-subtraction-Commutative-Ring :
(x y z : type-Commutative-Ring) →
mul-Commutative-Ring x (left-subtraction-Commutative-Ring y z) ＝
left-subtraction-Commutative-Ring
( mul-Commutative-Ring x y)
( mul-Commutative-Ring x z)
left-distributive-mul-left-subtraction-Commutative-Ring =
left-distributive-mul-left-subtraction-Ring ring-Commutative-Ring

right-distributive-mul-left-subtraction-Commutative-Ring :
(x y z : type-Commutative-Ring) →
mul-Commutative-Ring (left-subtraction-Commutative-Ring x y) z ＝
left-subtraction-Commutative-Ring
( mul-Commutative-Ring x z)
( mul-Commutative-Ring y z)
right-distributive-mul-left-subtraction-Commutative-Ring =
right-distributive-mul-left-subtraction-Ring ring-Commutative-Ring

left-distributive-mul-right-subtraction-Commutative-Ring :
(x y z : type-Commutative-Ring) →
mul-Commutative-Ring x (right-subtraction-Commutative-Ring y z) ＝
right-subtraction-Commutative-Ring
( mul-Commutative-Ring x y)
( mul-Commutative-Ring x z)
left-distributive-mul-right-subtraction-Commutative-Ring =
left-distributive-mul-right-subtraction-Ring ring-Commutative-Ring

right-distributive-mul-right-subtraction-Commutative-Ring :
(x y z : type-Commutative-Ring) →
mul-Commutative-Ring (right-subtraction-Commutative-Ring x y) z ＝
right-subtraction-Commutative-Ring
( mul-Commutative-Ring x z)
( mul-Commutative-Ring y z)
right-distributive-mul-right-subtraction-Commutative-Ring =
right-distributive-mul-right-subtraction-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

(n : ℕ) (x y : type-Commutative-Ring) →
mul-nat-scalar-Commutative-Ring n (add-Commutative-Ring x y) ＝
( mul-nat-scalar-Commutative-Ring n x)
( mul-nat-scalar-Commutative-Ring n y)

(m n : ℕ) (x : type-Commutative-Ring) →
mul-nat-scalar-Commutative-Ring (m +ℕ n) x ＝
( mul-nat-scalar-Commutative-Ring m x)
( mul-nat-scalar-Commutative-Ring n x)


### Addition of a list of elements in a commutative ring

  add-list-Commutative-Ring : list type-Commutative-Ring → type-Commutative-Ring