# Integral domains

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Fernando Chu.

Created on 2022-05-23.

module commutative-algebra.integral-domains where

Imports
open import commutative-algebra.commutative-rings
open import commutative-algebra.commutative-semirings
open import commutative-algebra.trivial-commutative-rings

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.cartesian-product-types
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

An integral domain is a nonzero commutative ring R such that the product of any two nonzero elements in R is nonzero. Equivalently, a commutative ring R is an integral domain if and only if multiplication by any nonzero element a satisfies the cancellation property: ax = ay ⇒ x = y.

## Definition

### The cancellation property for a commutative ring

cancellation-property-Commutative-Ring :
{l : Level} (R : Commutative-Ring l) → UU l
cancellation-property-Commutative-Ring R =
(x : type-Commutative-Ring R) → is-nonzero-Commutative-Ring R x →
is-injective (mul-Commutative-Ring R x)


### Integral domains

Integral-Domain : (l : Level) → UU (lsuc l)
Integral-Domain l =
Σ ( Commutative-Ring l)
( λ R →
cancellation-property-Commutative-Ring R ×
is-nontrivial-Commutative-Ring R)

module _
{l : Level} (R : Integral-Domain l)
where

commutative-ring-Integral-Domain : Commutative-Ring l
commutative-ring-Integral-Domain = pr1 R

has-cancellation-property-Integral-Domain :
cancellation-property-Commutative-Ring commutative-ring-Integral-Domain
has-cancellation-property-Integral-Domain = pr1 (pr2 R)

is-nontrivial-Integral-Domain :
is-nontrivial-Commutative-Ring commutative-ring-Integral-Domain
is-nontrivial-Integral-Domain = pr2 (pr2 R)

ab-Integral-Domain : Ab l
ab-Integral-Domain = ab-Commutative-Ring commutative-ring-Integral-Domain

ring-Integral-Domain : Ring l
ring-Integral-Domain = ring-Commutative-Ring commutative-ring-Integral-Domain

set-Integral-Domain : Set l
set-Integral-Domain = set-Ring ring-Integral-Domain

type-Integral-Domain : UU l
type-Integral-Domain = type-Ring ring-Integral-Domain

is-set-type-Integral-Domain : is-set type-Integral-Domain
is-set-type-Integral-Domain = is-set-type-Ring ring-Integral-Domain


### Addition in an integral domain

  has-associative-add-Integral-Domain :
has-associative-mul-Set set-Integral-Domain

type-Integral-Domain → type-Integral-Domain → type-Integral-Domain

type-Integral-Domain → type-Integral-Domain → type-Integral-Domain

{x x' y y' : type-Integral-Domain} →
(x ＝ x') → (y ＝ y') →

(x y z : type-Integral-Domain) →

is-group-Ab ab-Integral-Domain

(x y : type-Integral-Domain) →

(x y x' y' : type-Integral-Domain) →

(x y z : type-Integral-Domain) →

(x y z : type-Integral-Domain) →

(x : type-Integral-Domain) → is-equiv (add-Integral-Domain x)

(x : type-Integral-Domain) → is-equiv (add-Integral-Domain' x)

(x : type-Integral-Domain) → is-emb (add-Integral-Domain x)

(x : type-Integral-Domain) → is-emb (add-Integral-Domain' x)

(x : type-Integral-Domain) → is-injective (add-Integral-Domain x)

(x : type-Integral-Domain) → is-injective (add-Integral-Domain' x)


### The zero element of an integral domain

  has-zero-Integral-Domain : is-unital add-Integral-Domain
has-zero-Integral-Domain =
has-zero-Commutative-Ring commutative-ring-Integral-Domain

zero-Integral-Domain : type-Integral-Domain
zero-Integral-Domain =
zero-Commutative-Ring commutative-ring-Integral-Domain

is-zero-Integral-Domain : type-Integral-Domain → UU l
is-zero-Integral-Domain =
is-zero-Commutative-Ring commutative-ring-Integral-Domain

is-nonzero-Integral-Domain : type-Integral-Domain → UU l
is-nonzero-Integral-Domain =
is-nonzero-Commutative-Ring commutative-ring-Integral-Domain

is-zero-integral-domain-Prop : type-Integral-Domain → Prop l
is-zero-integral-domain-Prop x =
Id-Prop set-Integral-Domain x zero-Integral-Domain

is-nonzero-integral-domain-Prop : type-Integral-Domain → Prop l
is-nonzero-integral-domain-Prop x =
neg-Prop (is-zero-integral-domain-Prop x)

(x : type-Integral-Domain) →

(x : type-Integral-Domain) →


### Additive inverses in an integral domain

  has-negatives-Integral-Domain :
is-group-is-unital-Semigroup
( has-zero-Integral-Domain)
has-negatives-Integral-Domain = has-negatives-Ab ab-Integral-Domain

neg-Integral-Domain : type-Integral-Domain → type-Integral-Domain
neg-Integral-Domain = neg-Commutative-Ring commutative-ring-Integral-Domain

(x : type-Integral-Domain) →
add-Integral-Domain (neg-Integral-Domain x) x ＝ zero-Integral-Domain

(x : type-Integral-Domain) →
add-Integral-Domain x (neg-Integral-Domain x) ＝ zero-Integral-Domain

neg-neg-Integral-Domain :
(x : type-Integral-Domain) →
neg-Integral-Domain (neg-Integral-Domain x) ＝ x
neg-neg-Integral-Domain = neg-neg-Ab ab-Integral-Domain

(x y : type-Integral-Domain) →


### Multiplication in an integral domain

  has-associative-mul-Integral-Domain :
has-associative-mul-Set set-Integral-Domain
has-associative-mul-Integral-Domain =
has-associative-mul-Commutative-Ring commutative-ring-Integral-Domain

mul-Integral-Domain :
(x y : type-Integral-Domain) → type-Integral-Domain
mul-Integral-Domain =
mul-Commutative-Ring commutative-ring-Integral-Domain

mul-Integral-Domain' :
(x y : type-Integral-Domain) → type-Integral-Domain
mul-Integral-Domain' =
mul-Commutative-Ring' commutative-ring-Integral-Domain

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

associative-mul-Integral-Domain :
(x y z : type-Integral-Domain) →
mul-Integral-Domain (mul-Integral-Domain x y) z ＝
mul-Integral-Domain x (mul-Integral-Domain y z)
associative-mul-Integral-Domain =
associative-mul-Commutative-Ring commutative-ring-Integral-Domain

multiplicative-semigroup-Integral-Domain : Semigroup l
multiplicative-semigroup-Integral-Domain =
multiplicative-semigroup-Commutative-Ring
commutative-ring-Integral-Domain

(x y z : type-Integral-Domain) →
( mul-Integral-Domain x (add-Integral-Domain y z)) ＝
( mul-Integral-Domain x y)
( mul-Integral-Domain x z))
commutative-ring-Integral-Domain

(x y z : type-Integral-Domain) →
( mul-Integral-Domain (add-Integral-Domain x y) z) ＝
( mul-Integral-Domain x z)
( mul-Integral-Domain y z))
commutative-ring-Integral-Domain

commutative-mul-Integral-Domain :
(x y : type-Integral-Domain) →
mul-Integral-Domain x y ＝ mul-Integral-Domain y x
commutative-mul-Integral-Domain =
commutative-mul-Commutative-Ring
commutative-ring-Integral-Domain


### Multiplicative units in an integral domain

  is-unital-Integral-Domain : is-unital mul-Integral-Domain
is-unital-Integral-Domain =
is-unital-Commutative-Ring
commutative-ring-Integral-Domain

multiplicative-monoid-Integral-Domain : Monoid l
multiplicative-monoid-Integral-Domain =
multiplicative-monoid-Commutative-Ring
commutative-ring-Integral-Domain

one-Integral-Domain : type-Integral-Domain
one-Integral-Domain =
one-Commutative-Ring
commutative-ring-Integral-Domain

left-unit-law-mul-Integral-Domain :
(x : type-Integral-Domain) →
mul-Integral-Domain one-Integral-Domain x ＝ x
left-unit-law-mul-Integral-Domain =
left-unit-law-mul-Commutative-Ring
commutative-ring-Integral-Domain

right-unit-law-mul-Integral-Domain :
(x : type-Integral-Domain) →
mul-Integral-Domain x one-Integral-Domain ＝ x
right-unit-law-mul-Integral-Domain =
right-unit-law-mul-Commutative-Ring
commutative-ring-Integral-Domain

right-swap-mul-Integral-Domain :
(x y z : type-Integral-Domain) →
mul-Integral-Domain (mul-Integral-Domain x y) z ＝
mul-Integral-Domain (mul-Integral-Domain x z) y
right-swap-mul-Integral-Domain x y z =
( associative-mul-Integral-Domain x y z) ∙
( ( ap
( mul-Integral-Domain x)
( commutative-mul-Integral-Domain y z)) ∙
( inv (associative-mul-Integral-Domain x z y)))

left-swap-mul-Integral-Domain :
(x y z : type-Integral-Domain) →
mul-Integral-Domain x (mul-Integral-Domain y z) ＝
mul-Integral-Domain y (mul-Integral-Domain x z)
left-swap-mul-Integral-Domain x y z =
( inv (associative-mul-Integral-Domain x y z)) ∙
( ( ap
( mul-Integral-Domain' z)
( commutative-mul-Integral-Domain x y)) ∙
( associative-mul-Integral-Domain y x z))

interchange-mul-mul-Integral-Domain :
(x y z w : type-Integral-Domain) →
mul-Integral-Domain
( mul-Integral-Domain x y)
( mul-Integral-Domain z w) ＝
mul-Integral-Domain
( mul-Integral-Domain x z)
( mul-Integral-Domain y w)
interchange-mul-mul-Integral-Domain =
interchange-law-commutative-and-associative
mul-Integral-Domain
commutative-mul-Integral-Domain
associative-mul-Integral-Domain


### The zero laws for multiplication of a integral domains

  left-zero-law-mul-Integral-Domain :
(x : type-Integral-Domain) →
mul-Integral-Domain zero-Integral-Domain x ＝
zero-Integral-Domain
left-zero-law-mul-Integral-Domain =
left-zero-law-mul-Commutative-Ring commutative-ring-Integral-Domain

right-zero-law-mul-Integral-Domain :
(x : type-Integral-Domain) →
mul-Integral-Domain x zero-Integral-Domain ＝
zero-Integral-Domain
right-zero-law-mul-Integral-Domain =
right-zero-law-mul-Commutative-Ring commutative-ring-Integral-Domain


### Integral domains are commutative semirings

  multiplicative-commutative-monoid-Integral-Domain : Commutative-Monoid l
multiplicative-commutative-monoid-Integral-Domain =
multiplicative-commutative-monoid-Commutative-Ring
commutative-ring-Integral-Domain

semiring-Integral-Domain : Semiring l
semiring-Integral-Domain =
semiring-Commutative-Ring commutative-ring-Integral-Domain

commutative-semiring-Integral-Domain : Commutative-Semiring l
commutative-semiring-Integral-Domain =
commutative-semiring-Commutative-Ring
commutative-ring-Integral-Domain


### Computing multiplication with minus one in an integral domain

  neg-one-Integral-Domain : type-Integral-Domain
neg-one-Integral-Domain =
neg-one-Commutative-Ring
commutative-ring-Integral-Domain

mul-neg-one-Integral-Domain :
(x : type-Integral-Domain) →
mul-Integral-Domain neg-one-Integral-Domain x ＝
neg-Integral-Domain x
mul-neg-one-Integral-Domain =
mul-neg-one-Commutative-Ring
commutative-ring-Integral-Domain

mul-neg-one-Integral-Domain' :
(x : type-Integral-Domain) →
mul-Integral-Domain x neg-one-Integral-Domain ＝
neg-Integral-Domain x
mul-neg-one-Integral-Domain' =
mul-neg-one-Commutative-Ring'
commutative-ring-Integral-Domain

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

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


### Left and right negative laws for multiplication

  left-negative-law-mul-Integral-Domain :
(x y : type-Integral-Domain) →
mul-Integral-Domain (neg-Integral-Domain x) y ＝
neg-Integral-Domain (mul-Integral-Domain x y)
left-negative-law-mul-Integral-Domain =
left-negative-law-mul-Commutative-Ring
commutative-ring-Integral-Domain

right-negative-law-mul-Integral-Domain :
(x y : type-Integral-Domain) →
mul-Integral-Domain x (neg-Integral-Domain y) ＝
neg-Integral-Domain (mul-Integral-Domain x y)
right-negative-law-mul-Integral-Domain =
right-negative-law-mul-Commutative-Ring
commutative-ring-Integral-Domain

mul-neg-Integral-Domain :
(x y : type-Integral-Domain) →
mul-Integral-Domain (neg-Integral-Domain x) (neg-Integral-Domain y) ＝
mul-Integral-Domain x y
mul-neg-Integral-Domain =
mul-neg-Commutative-Ring
commutative-ring-Integral-Domain


### Scalar multiplication of elements of a integral domain by natural numbers

  mul-nat-scalar-Integral-Domain :
ℕ → type-Integral-Domain → type-Integral-Domain
mul-nat-scalar-Integral-Domain =
mul-nat-scalar-Commutative-Ring
commutative-ring-Integral-Domain

ap-mul-nat-scalar-Integral-Domain :
{m n : ℕ} {x y : type-Integral-Domain} →
(m ＝ n) → (x ＝ y) →
mul-nat-scalar-Integral-Domain m x ＝
mul-nat-scalar-Integral-Domain n y
ap-mul-nat-scalar-Integral-Domain =
ap-mul-nat-scalar-Commutative-Ring
commutative-ring-Integral-Domain

left-zero-law-mul-nat-scalar-Integral-Domain :
(x : type-Integral-Domain) →
mul-nat-scalar-Integral-Domain 0 x ＝ zero-Integral-Domain
left-zero-law-mul-nat-scalar-Integral-Domain =
left-zero-law-mul-nat-scalar-Commutative-Ring
commutative-ring-Integral-Domain

right-zero-law-mul-nat-scalar-Integral-Domain :
(n : ℕ) →
mul-nat-scalar-Integral-Domain n zero-Integral-Domain ＝
zero-Integral-Domain
right-zero-law-mul-nat-scalar-Integral-Domain =
right-zero-law-mul-nat-scalar-Commutative-Ring
commutative-ring-Integral-Domain

left-unit-law-mul-nat-scalar-Integral-Domain :
(x : type-Integral-Domain) →
mul-nat-scalar-Integral-Domain 1 x ＝ x
left-unit-law-mul-nat-scalar-Integral-Domain =
left-unit-law-mul-nat-scalar-Commutative-Ring
commutative-ring-Integral-Domain

left-nat-scalar-law-mul-Integral-Domain :
(n : ℕ) (x y : type-Integral-Domain) →
mul-Integral-Domain (mul-nat-scalar-Integral-Domain n x) y ＝
mul-nat-scalar-Integral-Domain n (mul-Integral-Domain x y)
left-nat-scalar-law-mul-Integral-Domain =
left-nat-scalar-law-mul-Commutative-Ring
commutative-ring-Integral-Domain

right-nat-scalar-law-mul-Integral-Domain :
(n : ℕ) (x y : type-Integral-Domain) →
mul-Integral-Domain x (mul-nat-scalar-Integral-Domain n y) ＝
mul-nat-scalar-Integral-Domain n (mul-Integral-Domain x y)
right-nat-scalar-law-mul-Integral-Domain =
right-nat-scalar-law-mul-Commutative-Ring
commutative-ring-Integral-Domain

(n : ℕ) (x y : type-Integral-Domain) →
mul-nat-scalar-Integral-Domain n (add-Integral-Domain x y) ＝
( mul-nat-scalar-Integral-Domain n x)
( mul-nat-scalar-Integral-Domain n y)
commutative-ring-Integral-Domain

(m n : ℕ) (x : type-Integral-Domain) →
mul-nat-scalar-Integral-Domain (m +ℕ n) x ＝
( mul-nat-scalar-Integral-Domain m x)
( mul-nat-scalar-Integral-Domain n x)
commutative-ring-Integral-Domain


### Addition of a list of elements in an integral domain

  add-list-Integral-Domain :
list type-Integral-Domain → type-Integral-Domain