# Euclidean domains

Content created by Fredrik Bakke, Egbert Rijke and Fernando Chu.

Created on 2023-04-05.

module commutative-algebra.euclidean-domains where

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

open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-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.coproduct-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

A Euclidean domain is an integral domain R that has a Euclidean valuation, i.e., a function v : R → ℕ such that for every x y : R, if y is nonzero then there are q r : R with x = q y + r and v r < v y.

## Definition

### The condition of being a Euclidean valuation

is-euclidean-valuation :
{ l : Level} (R : Integral-Domain l) →
( type-Integral-Domain R → ℕ) →
UU l
is-euclidean-valuation R v =
( x y : type-Integral-Domain R) →
( is-nonzero-Integral-Domain R y) →
Σ ( type-Integral-Domain R × type-Integral-Domain R)
( λ (q , r) →
( Id x (add-Integral-Domain R (mul-Integral-Domain R q y) r)) ×
( is-zero-Integral-Domain R r +
( v r <-ℕ v y)))


### The condition of being a Euclidean domain

is-euclidean-domain-Integral-Domain :
{ l : Level} (R : Integral-Domain l) → UU l
is-euclidean-domain-Integral-Domain R =
Σ (type-Integral-Domain R → ℕ) (is-euclidean-valuation R)


### Euclidean domains

Euclidean-Domain : (l : Level) → UU (lsuc l)
Euclidean-Domain l =
Σ (Integral-Domain l) is-euclidean-domain-Integral-Domain

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

integral-domain-Euclidean-Domain : Integral-Domain l
integral-domain-Euclidean-Domain = pr1 R

is-euclidean-domain-Euclidean-Domain :
is-euclidean-domain-Integral-Domain integral-domain-Euclidean-Domain
is-euclidean-domain-Euclidean-Domain = pr2 R

commutative-ring-Euclidean-Domain : Commutative-Ring l
commutative-ring-Euclidean-Domain =
commutative-ring-Integral-Domain integral-domain-Euclidean-Domain

has-cancellation-property-Euclidean-Domain :
cancellation-property-Commutative-Ring commutative-ring-Euclidean-Domain
has-cancellation-property-Euclidean-Domain =
has-cancellation-property-Integral-Domain
integral-domain-Euclidean-Domain

is-nontrivial-Euclidean-Domain :
is-nontrivial-Commutative-Ring commutative-ring-Euclidean-Domain
is-nontrivial-Euclidean-Domain =
is-nontrivial-Integral-Domain
integral-domain-Euclidean-Domain

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

ring-Euclidean-Domain : Ring l
ring-Euclidean-Domain =
ring-Integral-Domain integral-domain-Euclidean-Domain

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

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

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


### Addition in a Euclidean domain

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

type-Euclidean-Domain → type-Euclidean-Domain → type-Euclidean-Domain

type-Euclidean-Domain → type-Euclidean-Domain → type-Euclidean-Domain

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

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

is-group-Ab ab-Euclidean-Domain

(x y : type-Euclidean-Domain) →

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

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

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

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

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

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

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

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

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


### The zero element of a Euclidean domain

  has-zero-Euclidean-Domain : is-unital add-Euclidean-Domain
has-zero-Euclidean-Domain =
has-zero-Integral-Domain integral-domain-Euclidean-Domain

zero-Euclidean-Domain : type-Euclidean-Domain
zero-Euclidean-Domain =
zero-Integral-Domain integral-domain-Euclidean-Domain

is-zero-Euclidean-Domain : type-Euclidean-Domain → UU l
is-zero-Euclidean-Domain =
is-zero-Integral-Domain integral-domain-Euclidean-Domain

is-nonzero-Euclidean-Domain : type-Euclidean-Domain → UU l
is-nonzero-Euclidean-Domain =
is-nonzero-Integral-Domain integral-domain-Euclidean-Domain

is-zero-euclidean-domain-Prop : type-Euclidean-Domain → Prop l
is-zero-euclidean-domain-Prop x =
Id-Prop set-Euclidean-Domain x zero-Euclidean-Domain

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

(x : type-Euclidean-Domain) →

(x : type-Euclidean-Domain) →


### Additive inverses in a Euclidean domain

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

neg-Euclidean-Domain : type-Euclidean-Domain → type-Euclidean-Domain
neg-Euclidean-Domain = neg-Integral-Domain integral-domain-Euclidean-Domain

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

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

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

(x y : type-Euclidean-Domain) →


### Multiplication in a Euclidean domain

  has-associative-mul-Euclidean-Domain :
has-associative-mul-Set set-Euclidean-Domain
has-associative-mul-Euclidean-Domain =
has-associative-mul-Integral-Domain integral-domain-Euclidean-Domain

mul-Euclidean-Domain :
(x y : type-Euclidean-Domain) → type-Euclidean-Domain
mul-Euclidean-Domain =
mul-Integral-Domain integral-domain-Euclidean-Domain

mul-Euclidean-Domain' :
(x y : type-Euclidean-Domain) → type-Euclidean-Domain
mul-Euclidean-Domain' =
mul-Integral-Domain' integral-domain-Euclidean-Domain

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

associative-mul-Euclidean-Domain :
(x y z : type-Euclidean-Domain) →
mul-Euclidean-Domain (mul-Euclidean-Domain x y) z ＝
mul-Euclidean-Domain x (mul-Euclidean-Domain y z)
associative-mul-Euclidean-Domain =
associative-mul-Integral-Domain integral-domain-Euclidean-Domain

multiplicative-semigroup-Euclidean-Domain : Semigroup l
multiplicative-semigroup-Euclidean-Domain =
multiplicative-semigroup-Integral-Domain
integral-domain-Euclidean-Domain

(x y z : type-Euclidean-Domain) →
( mul-Euclidean-Domain x (add-Euclidean-Domain y z)) ＝
( mul-Euclidean-Domain x y)
( mul-Euclidean-Domain x z))
integral-domain-Euclidean-Domain

(x y z : type-Euclidean-Domain) →
( mul-Euclidean-Domain (add-Euclidean-Domain x y) z) ＝
( mul-Euclidean-Domain x z)
( mul-Euclidean-Domain y z))
integral-domain-Euclidean-Domain

commutative-mul-Euclidean-Domain :
(x y : type-Euclidean-Domain) →
mul-Euclidean-Domain x y ＝ mul-Euclidean-Domain y x
commutative-mul-Euclidean-Domain =
commutative-mul-Integral-Domain
integral-domain-Euclidean-Domain


### Multiplicative units in a Euclidean domain

  is-unital-Euclidean-Domain : is-unital mul-Euclidean-Domain
is-unital-Euclidean-Domain =
is-unital-Integral-Domain
integral-domain-Euclidean-Domain

multiplicative-monoid-Euclidean-Domain : Monoid l
multiplicative-monoid-Euclidean-Domain =
multiplicative-monoid-Integral-Domain
integral-domain-Euclidean-Domain

one-Euclidean-Domain : type-Euclidean-Domain
one-Euclidean-Domain =
one-Integral-Domain
integral-domain-Euclidean-Domain

left-unit-law-mul-Euclidean-Domain :
(x : type-Euclidean-Domain) →
mul-Euclidean-Domain one-Euclidean-Domain x ＝ x
left-unit-law-mul-Euclidean-Domain =
left-unit-law-mul-Integral-Domain
integral-domain-Euclidean-Domain

right-unit-law-mul-Euclidean-Domain :
(x : type-Euclidean-Domain) →
mul-Euclidean-Domain x one-Euclidean-Domain ＝ x
right-unit-law-mul-Euclidean-Domain =
right-unit-law-mul-Integral-Domain
integral-domain-Euclidean-Domain

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

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

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


### The zero laws for multiplication of a Euclidean domain

  left-zero-law-mul-Euclidean-Domain :
(x : type-Euclidean-Domain) →
mul-Euclidean-Domain zero-Euclidean-Domain x ＝
zero-Euclidean-Domain
left-zero-law-mul-Euclidean-Domain =
left-zero-law-mul-Integral-Domain integral-domain-Euclidean-Domain

right-zero-law-mul-Euclidean-Domain :
(x : type-Euclidean-Domain) →
mul-Euclidean-Domain x zero-Euclidean-Domain ＝
zero-Euclidean-Domain
right-zero-law-mul-Euclidean-Domain =
right-zero-law-mul-Integral-Domain integral-domain-Euclidean-Domain


### Euclidean domains are commutative semirings

  multiplicative-commutative-monoid-Euclidean-Domain : Commutative-Monoid l
multiplicative-commutative-monoid-Euclidean-Domain =
multiplicative-commutative-monoid-Integral-Domain
integral-domain-Euclidean-Domain

semiring-Euclidean-Domain : Semiring l
semiring-Euclidean-Domain =
semiring-Integral-Domain integral-domain-Euclidean-Domain

commutative-semiring-Euclidean-Domain : Commutative-Semiring l
commutative-semiring-Euclidean-Domain =
commutative-semiring-Integral-Domain
integral-domain-Euclidean-Domain


### Computing multiplication with minus one in a Euclidean domain

  neg-one-Euclidean-Domain : type-Euclidean-Domain
neg-one-Euclidean-Domain =
neg-one-Integral-Domain
integral-domain-Euclidean-Domain

mul-neg-one-Euclidean-Domain :
(x : type-Euclidean-Domain) →
mul-Euclidean-Domain neg-one-Euclidean-Domain x ＝
neg-Euclidean-Domain x
mul-neg-one-Euclidean-Domain =
mul-neg-one-Integral-Domain
integral-domain-Euclidean-Domain

mul-neg-one-Euclidean-Domain' :
(x : type-Euclidean-Domain) →
mul-Euclidean-Domain x neg-one-Euclidean-Domain ＝
neg-Euclidean-Domain x
mul-neg-one-Euclidean-Domain' =
mul-neg-one-Integral-Domain'
integral-domain-Euclidean-Domain

is-involution-mul-neg-one-Euclidean-Domain :
is-involution (mul-Euclidean-Domain neg-one-Euclidean-Domain)
is-involution-mul-neg-one-Euclidean-Domain =
is-involution-mul-neg-one-Integral-Domain
integral-domain-Euclidean-Domain

is-involution-mul-neg-one-Euclidean-Domain' :
is-involution (mul-Euclidean-Domain' neg-one-Euclidean-Domain)
is-involution-mul-neg-one-Euclidean-Domain' =
is-involution-mul-neg-one-Integral-Domain'
integral-domain-Euclidean-Domain


### Left and right negative laws for multiplication

  left-negative-law-mul-Euclidean-Domain :
(x y : type-Euclidean-Domain) →
mul-Euclidean-Domain (neg-Euclidean-Domain x) y ＝
neg-Euclidean-Domain (mul-Euclidean-Domain x y)
left-negative-law-mul-Euclidean-Domain =
left-negative-law-mul-Integral-Domain
integral-domain-Euclidean-Domain

right-negative-law-mul-Euclidean-Domain :
(x y : type-Euclidean-Domain) →
mul-Euclidean-Domain x (neg-Euclidean-Domain y) ＝
neg-Euclidean-Domain (mul-Euclidean-Domain x y)
right-negative-law-mul-Euclidean-Domain =
right-negative-law-mul-Integral-Domain
integral-domain-Euclidean-Domain

mul-neg-Euclidean-Domain :
(x y : type-Euclidean-Domain) →
mul-Euclidean-Domain (neg-Euclidean-Domain x) (neg-Euclidean-Domain y) ＝
mul-Euclidean-Domain x y
mul-neg-Euclidean-Domain =
mul-neg-Integral-Domain
integral-domain-Euclidean-Domain


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

  mul-nat-scalar-Euclidean-Domain :
ℕ → type-Euclidean-Domain → type-Euclidean-Domain
mul-nat-scalar-Euclidean-Domain =
mul-nat-scalar-Integral-Domain
integral-domain-Euclidean-Domain

ap-mul-nat-scalar-Euclidean-Domain :
{m n : ℕ} {x y : type-Euclidean-Domain} →
(m ＝ n) → (x ＝ y) →
mul-nat-scalar-Euclidean-Domain m x ＝
mul-nat-scalar-Euclidean-Domain n y
ap-mul-nat-scalar-Euclidean-Domain =
ap-mul-nat-scalar-Integral-Domain
integral-domain-Euclidean-Domain

left-zero-law-mul-nat-scalar-Euclidean-Domain :
(x : type-Euclidean-Domain) →
mul-nat-scalar-Euclidean-Domain 0 x ＝ zero-Euclidean-Domain
left-zero-law-mul-nat-scalar-Euclidean-Domain =
left-zero-law-mul-nat-scalar-Integral-Domain
integral-domain-Euclidean-Domain

right-zero-law-mul-nat-scalar-Euclidean-Domain :
(n : ℕ) →
mul-nat-scalar-Euclidean-Domain n zero-Euclidean-Domain ＝
zero-Euclidean-Domain
right-zero-law-mul-nat-scalar-Euclidean-Domain =
right-zero-law-mul-nat-scalar-Integral-Domain
integral-domain-Euclidean-Domain

left-unit-law-mul-nat-scalar-Euclidean-Domain :
(x : type-Euclidean-Domain) →
mul-nat-scalar-Euclidean-Domain 1 x ＝ x
left-unit-law-mul-nat-scalar-Euclidean-Domain =
left-unit-law-mul-nat-scalar-Integral-Domain
integral-domain-Euclidean-Domain

left-nat-scalar-law-mul-Euclidean-Domain :
(n : ℕ) (x y : type-Euclidean-Domain) →
mul-Euclidean-Domain (mul-nat-scalar-Euclidean-Domain n x) y ＝
mul-nat-scalar-Euclidean-Domain n (mul-Euclidean-Domain x y)
left-nat-scalar-law-mul-Euclidean-Domain =
left-nat-scalar-law-mul-Integral-Domain
integral-domain-Euclidean-Domain

right-nat-scalar-law-mul-Euclidean-Domain :
(n : ℕ) (x y : type-Euclidean-Domain) →
mul-Euclidean-Domain x (mul-nat-scalar-Euclidean-Domain n y) ＝
mul-nat-scalar-Euclidean-Domain n (mul-Euclidean-Domain x y)
right-nat-scalar-law-mul-Euclidean-Domain =
right-nat-scalar-law-mul-Integral-Domain
integral-domain-Euclidean-Domain

(n : ℕ) (x y : type-Euclidean-Domain) →
mul-nat-scalar-Euclidean-Domain n (add-Euclidean-Domain x y) ＝
( mul-nat-scalar-Euclidean-Domain n x)
( mul-nat-scalar-Euclidean-Domain n y)
integral-domain-Euclidean-Domain

(m n : ℕ) (x : type-Euclidean-Domain) →
mul-nat-scalar-Euclidean-Domain (m +ℕ n) x ＝
( mul-nat-scalar-Euclidean-Domain m x)
( mul-nat-scalar-Euclidean-Domain n x)
integral-domain-Euclidean-Domain


### Addition of a list of elements in a Euclidean domain

  add-list-Euclidean-Domain :
list type-Euclidean-Domain → type-Euclidean-Domain

(l1 l2 : list type-Euclidean-Domain) →
Id
integral-domain-Euclidean-Domain


### Euclidean division in a Euclidean domain

  euclidean-valuation-Euclidean-Domain :
type-Euclidean-Domain → ℕ
euclidean-valuation-Euclidean-Domain =
pr1 is-euclidean-domain-Euclidean-Domain

euclidean-division-Euclidean-Domain :
( x y : type-Euclidean-Domain) →
( is-nonzero-Euclidean-Domain y) →
type-Euclidean-Domain × type-Euclidean-Domain
euclidean-division-Euclidean-Domain x y p =
pr1 (pr2 is-euclidean-domain-Euclidean-Domain x y p)

quotient-euclidean-division-Euclidean-Domain :
( x y : type-Euclidean-Domain) →
( is-nonzero-Euclidean-Domain y) →
type-Euclidean-Domain
quotient-euclidean-division-Euclidean-Domain x y p =
pr1 (euclidean-division-Euclidean-Domain x y p)

remainder-euclidean-division-Euclidean-Domain :
( x y : type-Euclidean-Domain) →
( is-nonzero-Euclidean-Domain y) →
type-Euclidean-Domain
remainder-euclidean-division-Euclidean-Domain x y p =
pr2 (euclidean-division-Euclidean-Domain x y p)

equation-euclidean-division-Euclidean-Domain :
( x y : type-Euclidean-Domain) →
( p : is-nonzero-Euclidean-Domain y) →
( Id
( x)
( mul-Euclidean-Domain
( quotient-euclidean-division-Euclidean-Domain x y p)
( y))
( remainder-euclidean-division-Euclidean-Domain x y p)))
equation-euclidean-division-Euclidean-Domain x y p =
pr1 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))

remainder-condition-euclidean-division-Euclidean-Domain :
( x y : type-Euclidean-Domain) →
( p : is-nonzero-Integral-Domain integral-domain-Euclidean-Domain y) →
( is-zero-Euclidean-Domain
( remainder-euclidean-division-Euclidean-Domain x y p)) +
( euclidean-valuation-Euclidean-Domain
( remainder-euclidean-division-Euclidean-Domain x y p) <-ℕ
( euclidean-valuation-Euclidean-Domain y))
remainder-condition-euclidean-division-Euclidean-Domain x y p =
pr2 (pr2 (pr2 is-euclidean-domain-Euclidean-Domain x y p))