Mathlib.Algebra.EuclideanDomain.Defs

Module docstring

{"# Euclidean domains

This file introduces Euclidean domains and provides the extended Euclidean algorithm. To be precise, a slightly more general version is provided which is sometimes called a transfinite Euclidean domain and differs in the fact that the degree function need not take values in ℕ but can take values in any well-ordered set. Transfinite Euclidean domains were introduced by Motzkin and examples which don't satisfy the classical notion were provided independently by Hiblot and Nagata.

Main definitions

EuclideanDomain: Defines Euclidean domain with functions quotient and remainder. Instances of Div and Mod are provided, so that one can write a = b * (a / b) + a % b.
gcd: defines the greatest common divisors of two elements of a Euclidean domain.
xgcd: given two elements a b : R, xgcd a b defines the pair (x, y) such that x * a + y * b = gcd a b.
lcm: defines the lowest common multiple of two elements a and b of a Euclidean domain as a * b / (gcd a b)

Main statements

See Algebra.EuclideanDomain.Basic for most of the theorems about Euclidean domains, including Bézout's lemma.

See Algebra.EuclideanDomain.Instances for the fact that ℤ is a Euclidean domain, as is any field.

Notation

≺ denotes the well founded relation on the Euclidean domain, e.g. in the example of the polynomial ring over a field, p ≺ q for polynomials p and q if and only if the degree of p is less than the degree of q.

Implementation details

Instead of working with a valuation, EuclideanDomain is implemented with the existence of a well founded relation r on the integral domain R, which in the example of ℤ would correspond to setting i ≺ j for integers i and j if the absolute value of i is smaller than the absolute value of j.

References

[Th. Motzkin, The Euclidean algorithm][MR32592]
[J.-J. Hiblot, Des anneaux euclidiens dont le plus petit algorithme n'est pas à valeurs finies] [MR399081]
[M. Nagata, On Euclid algorithm][MR541021]

Tags

Euclidean domain, transfinite Euclidean domain, Bézout's lemma "}

EuclideanDomain structure

(R : Type u) extends CommRing R, Nontrivial R

Full source

/-- A `EuclideanDomain` is a non-trivial commutative ring with a division and a remainder,
  satisfying `b * (a / b) + a % b = a`.
  The definition of a Euclidean domain usually includes a valuation function `R → ℕ`.
  This definition is slightly generalised to include a well founded relation
  `r` with the property that `r (a % b) b`, instead of a valuation. -/
class EuclideanDomain (R : Type u) extends CommRing R, Nontrivial R where
  /-- A division function (denoted `/`) on `R`.
    This satisfies the property `b * (a / b) + a % b = a`, where `%` denotes `remainder`. -/
  protected quotient : R → R → R
  /-- Division by zero should always give zero by convention. -/
  protected quotient_zero : ∀ a, quotient a 0 = 0
  /-- A remainder function (denoted `%`) on `R`.
    This satisfies the property `b * (a / b) + a % b = a`, where `/` denotes `quotient`. -/
  protected remainder : R → R → R
  /-- The property that links the quotient and remainder functions.
    This allows us to compute GCDs and LCMs. -/
  protected quotient_mul_add_remainder_eq : ∀ a b, b * quotient a b + remainder a b = a
  /-- A well-founded relation on `R`, satisfying `r (a % b) b`.
    This ensures that the GCD algorithm always terminates. -/
  protected r : R → R → Prop
  /-- The relation `r` must be well-founded.
    This ensures that the GCD algorithm always terminates. -/
  r_wellFounded : WellFounded r
  /-- The relation `r` satisfies `r (a % b) b`. -/
  protected remainder_lt : ∀ (a) {b}, b ≠ 0 → r (remainder a b) b
  /-- An additional constraint on `r`. -/
  mul_left_not_lt : ∀ (a) {b}, b ≠ 0 → ¬r (a * b) a

Euclidean Domain

Informal description

A Euclidean domain is a nontrivial commutative ring $ R $ equipped with a division operation and a remainder operation, satisfying the property that for any elements $ a, b \in R $ with $ b \neq 0 $, the equation $ a = b \cdot (a / b) + a \% b $ holds. Unlike the classical definition, this structure is generalized to include a well-founded relation $ \prec $ on $ R $ (instead of a valuation to $ \mathbb{N} $) such that $ a \% b \prec b $ whenever $ b \neq 0 $.

EuclideanDomain.wellFoundedRelation instance

: WellFoundedRelation R

Full source

local instance wellFoundedRelation : WellFoundedRelation R where
  rel := EuclideanDomain.r
  wf := r_wellFounded

Well-Founded Relation on Euclidean Domains

Informal description

Every Euclidean domain $R$ is equipped with a well-founded relation $\prec$ that is used in the definition of the Euclidean algorithm.

EuclideanDomain.isWellFounded instance

: IsWellFounded R (· ≺ ·)

Full source

instance isWellFounded : IsWellFounded R (· ≺ ·) where
  wf := r_wellFounded

Well-foundedness of the Euclidean Domain Relation

Informal description

For any Euclidean domain $R$, the relation $\prec$ on $R$ is well-founded.

EuclideanDomain.instDiv instance

: Div R

Full source

instance (priority := 70) : Div R :=
  ⟨EuclideanDomain.quotient⟩

Division Operation in Euclidean Domains

Informal description

Every Euclidean domain $R$ has a division operation $/$ satisfying $a = b \cdot (a / b) + a \% b$ for any $a, b \in R$ with $b \neq 0$.

EuclideanDomain.instMod instance

: Mod R

Full source

instance (priority := 70) : Mod R :=
  ⟨EuclideanDomain.remainder⟩

Modulus Operation in Euclidean Domains

Informal description

Every Euclidean domain $R$ has a modulus operation $\%$ satisfying $a = b \cdot (a / b) + a \% b$ for any $a, b \in R$ with $b \neq 0$.

EuclideanDomain.div_add_mod theorem

(a b : R) : b * (a / b) + a % b = a

Full source

theorem div_add_mod (a b : R) : b * (a / b) + a % b = a :=
  EuclideanDomain.quotient_mul_add_remainder_eq _ _

Division-Remainder Identity in Euclidean Domains

Informal description

For any elements $a$ and $b$ in a Euclidean domain $R$, the equation $b \cdot (a / b) + a \% b = a$ holds, where $/$ and $\%$ denote the division and remainder operations respectively.

EuclideanDomain.mod_add_div theorem

(a b : R) : a % b + b * (a / b) = a

Full source

theorem mod_add_div (a b : R) : a % b + b * (a / b) = a :=
  (add_comm _ _).trans (div_add_mod _ _)

Remainder-Division Identity in Euclidean Domains: $a \% b + b \cdot (a / b) = a$

Informal description

For any elements $a$ and $b$ in a Euclidean domain $R$, the equation $a \% b + b \cdot (a / b) = a$ holds, where $\%$ denotes the remainder operation and $/$ denotes the division operation.

EuclideanDomain.mod_add_div' theorem

(m k : R) : m % k + m / k * k = m

Full source

theorem mod_add_div' (m k : R) : m % k + m / k * k = m := by
  rw [mul_comm]
  exact mod_add_div _ _

Remainder-Division Identity in Euclidean Domains: $m \% k + (m / k) \cdot k = m$

Informal description

For any elements $m$ and $k$ in a Euclidean domain $R$, the equation $m \% k + (m / k) \cdot k = m$ holds, where $\%$ denotes the remainder operation and $/$ denotes the division operation.

EuclideanDomain.div_add_mod' theorem

(m k : R) : m / k * k + m % k = m

Full source

theorem div_add_mod' (m k : R) : m / k * k + m % k = m := by
  rw [mul_comm]
  exact div_add_mod _ _

Division-Remainder Identity in Euclidean Domains (Multiplicative Form)

Informal description

For any elements $m$ and $k$ in a Euclidean domain $R$, the equation $(m / k) \cdot k + (m \% k) = m$ holds, where $/$ and $\%$ denote the division and remainder operations respectively.

EuclideanDomain.mod_lt theorem

: ∀ (a) {b : R}, b ≠ 0 → a % b ≺ b

Full source

theorem mod_lt : ∀ (a) {b : R}, b ≠ 0 → a % b ≺ b :=
  EuclideanDomain.remainder_lt

Remainder is Smaller Than Divisor in Euclidean Domains

Informal description

For any elements $a$ and $b$ in a Euclidean domain $R$ with $b \neq 0$, the remainder $a \% b$ satisfies $a \% b \prec b$, where $\prec$ is the well-founded relation on $R$.

EuclideanDomain.mul_right_not_lt theorem

{a : R} (b) (h : a ≠ 0) : ¬a * b ≺ b

Full source

theorem mul_right_not_lt {a : R} (b) (h : a ≠ 0) : ¬a * b ≺ b := by
  rw [mul_comm]
  exact mul_left_not_lt b h

Non-decreasing Property of Multiplication in Euclidean Domains

Informal description

For any nonzero element $a$ in a Euclidean domain $R$ and any element $b \in R$, the product $a \cdot b$ is not strictly less than $b$ with respect to the well-founded relation $\prec$ on $R$.

EuclideanDomain.mod_zero theorem

(a : R) : a % 0 = a

Full source

@[simp]
theorem mod_zero (a : R) : a % 0 = a := by simpa only [zero_mul, zero_add] using div_add_mod a 0

Remainder When Dividing by Zero in Euclidean Domains

Informal description

For any element $a$ in a Euclidean domain $R$, the remainder of $a$ divided by zero is equal to $a$, i.e., $a \% 0 = a$.

EuclideanDomain.lt_one theorem

(a : R) : a ≺ (1 : R) → a = 0

Full source

theorem lt_one (a : R) : a ≺ (1 : R) → a = 0 :=
  haveI := Classical.dec
  not_imp_not.1 fun h => by simpa only [one_mul] using mul_left_not_lt 1 h

Elements Less Than One Are Zero in Euclidean Domains

Informal description

For any element $a$ in a Euclidean domain $R$, if $a$ is strictly less than the multiplicative identity $1$ with respect to the well-founded relation $\prec$, then $a$ must be zero, i.e., $a = 0$.

EuclideanDomain.div_zero theorem

(a : R) : a / 0 = 0

Full source

@[simp]
theorem div_zero (a : R) : a / 0 = 0 :=
  EuclideanDomain.quotient_zero a

Division by Zero in Euclidean Domains

Informal description

For any element $a$ in a Euclidean domain $R$, the division of $a$ by zero is defined to be zero, i.e., $a / 0 = 0$.

EuclideanDomain.GCD.induction theorem

{P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x) (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b

Full source

@[elab_as_elim]
theorem GCD.induction {P : R → R → Prop} (a b : R) (H0 : ∀ x, P 0 x)
    (H1 : ∀ a b, a ≠ 0 → P (b % a) a → P a b) : P a b := by
  classical
  exact if a0 : a = 0 then
    a0.symm ▸ H0 b
  else
    have _ := mod_lt b a0
    H1 _ _ a0 (GCD.induction (b % a) a H0 H1)
termination_by a

Induction Principle for GCD in Euclidean Domains

Informal description

Let $R$ be a Euclidean domain and $P : R \to R \to \mathrm{Prop}$ be a binary predicate on $R$. For any elements $a, b \in R$, if: 1. $P(0, x)$ holds for all $x \in R$, and 2. For any $a, b \in R$ with $a \neq 0$, if $P(b \% a, a)$ holds then $P(a, b)$ holds, then $P(a, b)$ holds. This provides an induction principle for proving properties about the greatest common divisor in Euclidean domains.

EuclideanDomain.gcd definition

(a b : R) : R

Full source

/-- `gcd a b` is a (non-unique) element such that `gcd a b ∣ a` `gcd a b ∣ b`, and for
  any element `c` such that `c ∣ a` and `c ∣ b`, then `c ∣ gcd a b` -/
def gcd (a b : R) : R :=
  if a0 : a = 0 then b
  else
    have _ := mod_lt b a0
    gcd (b % a) a
termination_by a

Greatest Common Divisor in a Euclidean Domain

Informal description

The greatest common divisor (gcd) of two elements $ a $ and $ b $ in a Euclidean domain $ R $ is an element $ \text{gcd}(a, b) $ that divides both $ a $ and $ b $, and for any other element $ c $ that divides both $ a $ and $ b $, $ c $ also divides $ \text{gcd}(a, b) $. The gcd is computed recursively using the Euclidean algorithm: if $ a = 0 $, then $ \text{gcd}(a, b) = b $; otherwise, $ \text{gcd}(a, b) = \text{gcd}(b \% a, a) $, where $ \% $ denotes the remainder operation.

EuclideanDomain.gcd_zero_left theorem

(a : R) : gcd 0 a = a

Full source

@[simp]
theorem gcd_zero_left (a : R) : gcd 0 a = a := by
  rw [gcd]
  exact if_pos rfl

GCD with Zero: $\gcd(0, a) = a$ in Euclidean Domains

Informal description

For any element $a$ in a Euclidean domain $R$, the greatest common divisor of $0$ and $a$ is equal to $a$, i.e., $\gcd(0, a) = a$.

EuclideanDomain.xgcdAux definition

(r s t r' s' t' : R) : R × R × R

Full source

/-- An implementation of the extended GCD algorithm.
At each step we are computing a triple `(r, s, t)`, where `r` is the next value of the GCD
algorithm, to compute the greatest common divisor of the input (say `x` and `y`), and `s` and `t`
are the coefficients in front of `x` and `y` to obtain `r` (i.e. `r = s * x + t * y`).
The function `xgcdAux` takes in two triples, and from these recursively computes the next triple:
```
xgcdAux (r, s, t) (r', s', t') = xgcdAux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
```
-/
def xgcdAux (r s t r' s' t' : R) : R × R × R :=
  if _hr : r = 0 then (r', s', t')
  else
    let q := r' / r
    have _ := mod_lt r' _hr
    xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
termination_by r

Extended GCD Algorithm Auxiliary Function

Informal description

The extended GCD algorithm auxiliary function. Given two triples `(r, s, t)` and `(r', s', t')`, where `r` and `r'` are successive remainders in the Euclidean algorithm, and `s, t, s', t'` are coefficients such that `r = s * x + t * y` and `r' = s' * x + t' * y` for some fixed `x` and `y`, the function recursively computes the next triple in the algorithm. The recursion step updates the triple as `(r' % r, s' - (r' / r) * s, t' - (r' / r) * t)` and continues until `r = 0`, at which point the result is `(r', s', t')`.

EuclideanDomain.xgcd_zero_left theorem

{s t r' s' t' : R} : xgcdAux 0 s t r' s' t' = (r', s', t')

Full source

@[simp]
theorem xgcd_zero_left {s t r' s' t' : R} : xgcdAux 0 s t r' s' t' = (r', s', t') := by
  unfold xgcdAux
  exact if_pos rfl

Extended GCD Auxiliary Function at Zero: $\text{xgcdAux}(0, s, t, r', s', t') = (r', s', t')$

Informal description

For any elements $s, t, r', s', t'$ in a Euclidean domain $R$, the extended GCD auxiliary function satisfies $\text{xgcdAux}(0, s, t, r', s', t') = (r', s', t')$.

EuclideanDomain.xgcdAux_rec theorem

 {r s t r' s' t' : R} (h : r ≠ 0) : xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Full source

theorem xgcdAux_rec {r s t r' s' t' : R} (h : r ≠ 0) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
  conv =>
    lhs
    rw [xgcdAux]
  exact if_neg h

Recursive Step of Extended GCD Algorithm in Euclidean Domains

Informal description

For any elements $r, s, t, r', s', t'$ in a Euclidean domain $R$ with $r \neq 0$, the extended GCD auxiliary function satisfies the recursive relation: \[ \text{xgcdAux}(r, s, t, r', s', t') = \text{xgcdAux}(r' \% r, s' - (r' / r) \cdot s, t' - (r' / r) \cdot t, r, s, t). \]

EuclideanDomain.xgcd definition

(x y : R) : R × R

Full source

/-- Use the extended GCD algorithm to generate the `a` and `b` values
  satisfying `gcd x y = x * a + y * b`. -/
def xgcd (x y : R) : R × R :=
  (xgcdAux x 1 0 y 0 1).2

Extended GCD coefficients

Informal description

Given two elements $ x $ and $ y $ in a Euclidean domain $ R $, the extended GCD algorithm computes a pair $(a, b)$ such that $ \gcd(x, y) = x \cdot a + y \cdot b $. This is achieved by applying the auxiliary function `xgcdAux` with initial coefficients $ (1, 0) $ for $ x $ and $ (0, 1) $ for $ y $, and extracting the resulting coefficients from the final triple.

EuclideanDomain.gcdA definition

(x y : R) : R

Full source

/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
def gcdA (x y : R) : R :=
  (xgcd x y).1

First coefficient in Bézout's identity

Informal description

The function `gcdA` takes two elements $ x $ and $ y $ of a Euclidean domain $ R $ and returns the coefficient $ a $ in the Bézout identity $ \gcd(x, y) = x \cdot a + y \cdot b $, where $ (a, b) $ are the coefficients computed by the extended GCD algorithm.

EuclideanDomain.gcdB definition

(x y : R) : R

Full source

/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
def gcdB (x y : R) : R :=
  (xgcd x y).2

Second coefficient in Bézout's identity

Informal description

The function `gcdB` takes two elements $ x $ and $ y $ of a Euclidean domain $ R $ and returns the coefficient $ b $ in the Bézout identity $ \gcd(x, y) = x \cdot a + y \cdot b $, where $ (a, b) $ are the coefficients computed by the extended GCD algorithm.

EuclideanDomain.gcdA_zero_left theorem

{s : R} : gcdA 0 s = 0

Full source

@[simp]
theorem gcdA_zero_left {s : R} : gcdA 0 s = 0 := by
  unfold gcdA
  rw [xgcd, xgcd_zero_left]

Bézout coefficient $\text{gcdA}(0, s) = 0$ in a Euclidean domain

Informal description

For any element $s$ in a Euclidean domain $R$, the first coefficient in Bézout's identity for $\gcd(0, s)$ is zero, i.e., $\text{gcdA}(0, s) = 0$.

EuclideanDomain.gcdB_zero_left theorem

{s : R} : gcdB 0 s = 1

Full source

@[simp]
theorem gcdB_zero_left {s : R} : gcdB 0 s = 1 := by
  unfold gcdB
  rw [xgcd, xgcd_zero_left]

Bézout coefficient identity: $\text{gcdB}(0, s) = 1$

Informal description

For any element $s$ in a Euclidean domain $R$, the second coefficient in Bézout's identity for $\gcd(0, s)$ is $1$, i.e., $\text{gcdB}(0, s) = 1$.

EuclideanDomain.xgcd_val theorem

(x y : R) : xgcd x y = (gcdA x y, gcdB x y)

Full source

theorem xgcd_val (x y : R) : xgcd x y = (gcdA x y, gcdB x y) :=
  rfl

Extended GCD Coefficients Match Bézout Coefficients

Informal description

For any elements $x$ and $y$ in a Euclidean domain $R$, the extended GCD coefficients $(a, b)$ computed by `xgcd x y` satisfy $a = \text{gcdA}(x, y)$ and $b = \text{gcdB}(x, y)$.

EuclideanDomain.lcm definition

(x y : R) : R

Full source

/-- `lcm a b` is a (non-unique) element such that `a ∣ lcm a b` `b ∣ lcm a b`, and for
  any element `c` such that `a ∣ c` and `b ∣ c`, then `lcm a b ∣ c` -/
def lcm (x y : R) : R :=
  x * y / gcd x y

Least Common Multiple in a Euclidean Domain

Informal description

The least common multiple (lcm) of two elements $ x $ and $ y $ in a Euclidean domain $ R $ is defined as $ \text{lcm}(x, y) = \frac{x \cdot y}{\text{gcd}(x, y)} $. It satisfies the properties that $ x $ divides $ \text{lcm}(x, y) $, $ y $ divides $ \text{lcm}(x, y) $, and for any element $ c $ in $ R $ such that $ x $ divides $ c $ and $ y $ divides $ c $, $ \text{lcm}(x, y) $ divides $ c $.