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

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

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.

• add : R → R → R
• add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
• zero : R
• zero_add : ∀ (a : R), 0 + a = a
• add_zero : ∀ (a : R), a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero : ∀ (x : R), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : R), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm : ∀ (a b : R), a + b = b + a
• mul : R → R → R
• left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : R), 0 * a = 0
• mul_zero : ∀ (a : R), a * 0 = 0
• mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
• one : R
• one_mul : ∀ (a : R), 1 * a = a
• mul_one : ∀ (a : R), a * 1 = a
• natCast : ℕ → R
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → R → R
• npow_zero : ∀ (x : R), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : R), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : R → R
• sub : R → R → R
• sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
• zsmul : ℤ → R → R
• zsmul_zero' : ∀ (a : R), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : R), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : R), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• add_left_neg : ∀ (a : R), -a + a = 0
• intCast : ℤ → R
• intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
• intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm : ∀ (a b : R), a * b = b * a
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• quotient : R → R → R

  A division function (denoted /) on R. This satisfies the property b * (a / b) + a % b = a, where % denotes remainder.

• quotient_zero : ∀ (a : R), EuclideanDomain.quotient a 0 = 0

  Division by zero should always give zero by convention.

• remainder : R → R → R

  A remainder function (denoted %) on R. This satisfies the property b * (a / b) + a % b = a, where / denotes quotient.

• quotient_mul_add_remainder_eq : ∀ (a b : R), b * EuclideanDomain.quotient a b + EuclideanDomain.remainder a b = a

  The property that links the quotient and remainder functions. This allows us to compute GCDs and LCMs.

• r : R → R → Prop

  A well-founded relation on R, satisfying r (a % b) b. This ensures that the GCD algorithm always terminates.

• r_wellFounded : WellFounded EuclideanDomain.r

  The relation r must be well-founded. This ensures that the GCD algorithm always terminates.

• remainder_lt : ∀ (a : R) {b : R}, b ≠ 0 → EuclideanDomain.r (EuclideanDomain.remainder a b) b

  The relation r satisfies r (a % b) b.

• mul_left_not_lt : ∀ (a : R) {b : R}, b ≠ 0 → ¬EuclideanDomain.r (a * b) a

  An additional constraint on r.

theorem EuclideanDomain.quotient_zero {R : Type u} [self : EuclideanDomain R] (a : R) : EuclideanDomain.quotient a 0 = 0

Division by zero should always give zero by convention.

theorem EuclideanDomain.quotient_mul_add_remainder_eq {R : Type u} [self : EuclideanDomain R] (a : R) (b : R) : b * EuclideanDomain.quotient a b + EuclideanDomain.remainder a b = a

The property that links the quotient and remainder functions. This allows us to compute GCDs and LCMs.

theorem EuclideanDomain.r_wellFounded {R : Type u} [self : EuclideanDomain R] : WellFounded EuclideanDomain.r

The relation r must be well-founded. This ensures that the GCD algorithm always terminates.

theorem EuclideanDomain.remainder_lt {R : Type u} [self : EuclideanDomain R] (a : R) {b : R} : b ≠ 0 → EuclideanDomain.r (EuclideanDomain.remainder a b) b

The relation r satisfies r (a % b) b.

theorem EuclideanDomain.mul_left_not_lt {R : Type u} [self : EuclideanDomain R] (a : R) {b : R} : b ≠ 0 → ¬EuclideanDomain.r (a * b) a

An additional constraint on r.

def EuclideanDomain.wellFoundedRelation {R : Type u} [EuclideanDomain R] : WellFoundedRelation R

Equations

• EuclideanDomain.wellFoundedRelation = { rel := EuclideanDomain.r, wf := ⋯ }

@[instance 70]

instance EuclideanDomain.instDiv {R : Type u} [EuclideanDomain R] : Div R

Equations

• EuclideanDomain.instDiv = { div := EuclideanDomain.quotient }

@[instance 70]

instance EuclideanDomain.instMod {R : Type u} [EuclideanDomain R] : Mod R

Equations

• EuclideanDomain.instMod = { mod := EuclideanDomain.remainder }

theorem EuclideanDomain.div_add_mod {R : Type u} [EuclideanDomain R] (a : R) (b : R) : b * (a / b) + a % b = a

theorem EuclideanDomain.mod_add_div {R : Type u} [EuclideanDomain R] (a : R) (b : R) : a % b + b * (a / b) = a

theorem EuclideanDomain.mod_add_div' {R : Type u} [EuclideanDomain R] (m : R) (k : R) : m % k + m / k * k = m

theorem EuclideanDomain.div_add_mod' {R : Type u} [EuclideanDomain R] (m : R) (k : R) : m / k * k + m % k = m

theorem EuclideanDomain.mod_eq_sub_mul_div {R : Type u_1} [EuclideanDomain R] (a : R) (b : R) : a % b = a - b * (a / b)

theorem EuclideanDomain.mod_lt {R : Type u} [EuclideanDomain R] (a : R) {b : R} : b ≠ 0 → EuclideanDomain.r (a % b) b

theorem EuclideanDomain.mul_right_not_lt {R : Type u} [EuclideanDomain R] {a : R} (b : R) (h : a ≠ 0) : ¬EuclideanDomain.r (a * b) b

@[simp]

theorem EuclideanDomain.mod_zero {R : Type u} [EuclideanDomain R] (a : R) : a % 0 = a

theorem EuclideanDomain.lt_one {R : Type u} [EuclideanDomain R] (a : R) : EuclideanDomain.r a 1 → a = 0

theorem EuclideanDomain.val_dvd_le {R : Type u} [EuclideanDomain R] (a : R) (b : R) : b ∣ a → a ≠ 0 → ¬EuclideanDomain.r a b

@[simp]

theorem EuclideanDomain.div_zero {R : Type u} [EuclideanDomain R] (a : R) : a / 0 = 0

@[irreducible]

theorem EuclideanDomain.GCD.induction {R : Type u} [EuclideanDomain R] {P : R → R → Prop} (a : R) (b : R) (H0 : ∀ (x : R), P 0 x) (H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b) : P a b

@[irreducible]

def EuclideanDomain.gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) (b : R) : R

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

Equations

• EuclideanDomain.gcd a b = if a0 : a = 0 then b else let_fun x := ⋯; EuclideanDomain.gcd (b % a) a

@[simp]

theorem EuclideanDomain.gcd_zero_left {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) : EuclideanDomain.gcd 0 a = a

@[irreducible]

def EuclideanDomain.xgcdAux {R : Type u} [EuclideanDomain R] [DecidableEq R] (r : R) (s : R) (t : R) (r' : R) (s' : R) (t' : R) : R × R × R

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)

Equations

• EuclideanDomain.xgcdAux r s t r' s' t' = if _hr : r = 0 then (r', s', t') else let q := r' / r; let_fun x := ⋯; EuclideanDomain.xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t

@[simp]

theorem EuclideanDomain.xgcd_zero_left {R : Type u} [EuclideanDomain R] [DecidableEq R] {s : R} {t : R} {r' : R} {s' : R} {t' : R} : EuclideanDomain.xgcdAux 0 s t r' s' t' = (r', s', t')

theorem EuclideanDomain.xgcdAux_rec {R : Type u} [EuclideanDomain R] [DecidableEq R] {r : R} {s : R} {t : R} {r' : R} {s' : R} {t' : R} (h : r ≠ 0) : EuclideanDomain.xgcdAux r s t r' s' t' = EuclideanDomain.xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

def EuclideanDomain.xgcd {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (y : R) : R × R

Use the extended GCD algorithm to generate the a and b values satisfying gcd x y = x * a + y * b.

Equations

• EuclideanDomain.xgcd x y = (EuclideanDomain.xgcdAux x 1 0 y 0 1).2

def EuclideanDomain.gcdA {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (y : R) : R

The extended GCD a value in the equation gcd x y = x * a + y * b.

Equations

• EuclideanDomain.gcdA x y = (EuclideanDomain.xgcd x y).1

def EuclideanDomain.gcdB {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (y : R) : R

The extended GCD b value in the equation gcd x y = x * a + y * b.

Equations

• EuclideanDomain.gcdB x y = (EuclideanDomain.xgcd x y).2

@[simp]

theorem EuclideanDomain.gcdA_zero_left {R : Type u} [EuclideanDomain R] [DecidableEq R] {s : R} : EuclideanDomain.gcdA 0 s = 0

@[simp]

theorem EuclideanDomain.gcdB_zero_left {R : Type u} [EuclideanDomain R] [DecidableEq R] {s : R} : EuclideanDomain.gcdB 0 s = 1

theorem EuclideanDomain.xgcd_val {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (y : R) : EuclideanDomain.xgcd x y = (EuclideanDomain.gcdA x y, EuclideanDomain.gcdB x y)

def EuclideanDomain.lcm {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (y : R) : R

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

Equations

• EuclideanDomain.lcm x y = x * y / EuclideanDomain.gcd x y