Monoids with normalization functions, gcd, and lcm
This file defines extra structures on comm_cancel_monoid_with_zeros, including integral_domains.
Main Definitions
Implementation Notes
normalization_monoidis defined by assigning to each element anorm_unitsuch that multiplying by that unit normalizes the monoid, andnormalizeis an idempotent monoid homomorphism. This definition as currently implemented does casework on0.gcd_monoidextendsnormalization_monoid, so thegcdandlcmare always normalized. This makesgcds of polynomials easier to work with, but excludes Euclidean domains, and monoids without zero.
TODO
- Provide a GCD monoid instance for
ℕ, port GCD facts about nats, definition of coprime - Generalize normalization monoids to commutative (cancellative) monoids with or without zero
- Generalize GCD monoid to not require normalization in all cases
Tags
divisibility, gcd, lcm, normalize
@[class]
structure
normalization_monoid
(α : Type u_2)
[nontrivial α]
[comm_cancel_monoid_with_zero α] :
Type u_2
- norm_unit : α → units α
- norm_unit_zero : normalization_monoid.norm_unit 0 = 1
- norm_unit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normalization_monoid.norm_unit (a * b) = normalization_monoid.norm_unit a * normalization_monoid.norm_unit b
- norm_unit_coe_units : ∀ (u : units α), normalization_monoid.norm_unit ↑u = u⁻¹
Normalization monoid: multiplying with norm_unit gives a normal form for associated elements.
@[simp]
theorem
norm_unit_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α] :
def
normalize
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α] :
α →* α
Chooses an element of each associate class, by multiplying by norm_unit
@[simp]
theorem
normalize_apply
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{x : α} :
theorem
associated_normalize
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{x : α} :
associated x (⇑normalize x)
theorem
normalize_associated
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{x : α} :
associated (⇑normalize x) x
@[simp]
theorem
normalize_zero
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α] :
@[simp]
theorem
normalize_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α] :
theorem
normalize_coe_units
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(u : units α) :
theorem
normalize_eq_zero
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{x : α} :
theorem
normalize_eq_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{x : α} :
@[simp]
theorem
norm_unit_mul_norm_unit
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(a : α) :
theorem
normalize_idem
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(x : α) :
theorem
normalize_eq_normalize
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{a b : α} :
theorem
normalize_eq_normalize_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{x y : α} :
theorem
dvd_antisymm_of_normalize_eq
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{a b : α} :
theorem
dvd_normalize_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{a b : α} :
theorem
normalize_dvd_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
{a b : α} :
def
associates.out
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α] :
associates α → α
Maps an element of associates back to the normalized element of its associate class
Equations
- associates.out = quotient.lift ⇑normalize associates.out._proof_1
theorem
associates.out_mk
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(a : α) :
(associates.mk a).out = ⇑normalize a
@[simp]
theorem
associates.out_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α] :
theorem
associates.out_mul
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(a b : associates α) :
theorem
associates.dvd_out_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(a : α)
(b : associates α) :
a ∣ b.out ↔ associates.mk a ≤ b
theorem
associates.out_dvd_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(a : α)
(b : associates α) :
b.out ∣ a ↔ b ≤ associates.mk a
@[simp]
theorem
associates.out_top
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α] :
@[simp]
theorem
associates.normalize_out
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[normalization_monoid α]
(a : associates α) :
@[instance]
def
gcd_monoid.to_normalization_monoid
(α : Type u_2)
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[s : gcd_monoid α] :
@[class]
- norm_unit : α → units α
- norm_unit_zero : gcd_monoid.norm_unit 0 = 1
- norm_unit_mul : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → gcd_monoid.norm_unit (a * b) = gcd_monoid.norm_unit a * gcd_monoid.norm_unit b
- norm_unit_coe_units : ∀ (u : units α), gcd_monoid.norm_unit ↑u = u⁻¹
- gcd : α → α → α
- lcm : α → α → α
- gcd_dvd_left : ∀ (a b : α), gcd_monoid.gcd a b ∣ a
- gcd_dvd_right : ∀ (a b : α), gcd_monoid.gcd a b ∣ b
- dvd_gcd : ∀ {a b c_1 : α}, a ∣ c_1 → a ∣ b → a ∣ gcd_monoid.gcd c_1 b
- normalize_gcd : ∀ (a b : α), ⇑normalize (gcd_monoid.gcd a b) = gcd_monoid.gcd a b
- gcd_mul_lcm : ∀ (a b : α), gcd_monoid.gcd a b * gcd_monoid.lcm a b = ⇑normalize (a * b)
- lcm_zero_left : ∀ (a : α), gcd_monoid.lcm 0 a = 0
- lcm_zero_right : ∀ (a : α), gcd_monoid.lcm a 0 = 0
GCD monoid: a comm_cancel_monoid_with_zero with normalization and gcd
(greatest common divisor) and lcm (least common multiple) operations. In this setting gcd and
lcm form a bounded lattice on the associated elements where gcd is the infimum, lcm is the
supremum, 1 is bottom, and 0 is top. The type class focuses on gcd and we derive the
corresponding lcm facts from gcd.
Instances
@[simp]
theorem
normalize_gcd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
⇑normalize (gcd_monoid.gcd a b) = gcd_monoid.gcd a b
@[simp]
theorem
gcd_mul_lcm
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
gcd_monoid.gcd a b * gcd_monoid.lcm a b = ⇑normalize (a * b)
theorem
dvd_gcd_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b c : α) :
theorem
gcd_comm
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
gcd_monoid.gcd a b = gcd_monoid.gcd b a
theorem
gcd_assoc
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.gcd (gcd_monoid.gcd m n) k = gcd_monoid.gcd m (gcd_monoid.gcd n k)
@[instance]
def
gcd_monoid.gcd.is_commutative
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α] :
Equations
@[instance]
def
gcd_monoid.gcd.is_associative
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α] :
Equations
theorem
gcd_eq_normalize
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{a b c : α} :
gcd_monoid.gcd a b ∣ c → c ∣ gcd_monoid.gcd a b → gcd_monoid.gcd a b = ⇑normalize c
@[simp]
theorem
gcd_zero_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.gcd 0 a = ⇑normalize a
@[simp]
theorem
gcd_zero_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.gcd a 0 = ⇑normalize a
@[simp]
theorem
gcd_eq_zero_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
@[simp]
theorem
gcd_one_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.gcd 1 a = 1
@[simp]
theorem
gcd_one_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.gcd a 1 = 1
theorem
gcd_dvd_gcd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{a b c d : α} :
a ∣ b → c ∣ d → gcd_monoid.gcd a c ∣ gcd_monoid.gcd b d
@[simp]
theorem
gcd_same
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.gcd a a = ⇑normalize a
@[simp]
theorem
gcd_mul_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b c : α) :
gcd_monoid.gcd (a * b) (a * c) = ⇑normalize a * gcd_monoid.gcd b c
@[simp]
theorem
gcd_mul_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b c : α) :
gcd_monoid.gcd (b * a) (c * a) = gcd_monoid.gcd b c * ⇑normalize a
theorem
gcd_eq_left_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
theorem
gcd_eq_right_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
theorem
gcd_dvd_gcd_mul_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.gcd m n ∣ gcd_monoid.gcd (k * m) n
theorem
gcd_dvd_gcd_mul_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.gcd m n ∣ gcd_monoid.gcd (m * k) n
theorem
gcd_dvd_gcd_mul_left_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.gcd m n ∣ gcd_monoid.gcd m (k * n)
theorem
gcd_dvd_gcd_mul_right_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.gcd m n ∣ gcd_monoid.gcd m (n * k)
theorem
lcm_dvd_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{a b c : α} :
theorem
dvd_lcm_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
a ∣ gcd_monoid.lcm a b
theorem
dvd_lcm_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
b ∣ gcd_monoid.lcm a b
theorem
lcm_dvd
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{a b c : α} :
a ∣ b → c ∣ b → gcd_monoid.lcm a c ∣ b
@[simp]
theorem
lcm_eq_zero_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
@[simp]
theorem
normalize_lcm
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
⇑normalize (gcd_monoid.lcm a b) = gcd_monoid.lcm a b
theorem
lcm_comm
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
gcd_monoid.lcm a b = gcd_monoid.lcm b a
theorem
lcm_assoc
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.lcm (gcd_monoid.lcm m n) k = gcd_monoid.lcm m (gcd_monoid.lcm n k)
@[instance]
def
gcd_monoid.lcm.is_commutative
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α] :
Equations
@[instance]
def
gcd_monoid.lcm.is_associative
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α] :
Equations
theorem
lcm_eq_normalize
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{a b c : α} :
gcd_monoid.lcm a b ∣ c → c ∣ gcd_monoid.lcm a b → gcd_monoid.lcm a b = ⇑normalize c
theorem
lcm_dvd_lcm
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{a b c d : α} :
a ∣ b → c ∣ d → gcd_monoid.lcm a c ∣ gcd_monoid.lcm b d
@[simp]
theorem
lcm_units_coe_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(u : units α)
(a : α) :
gcd_monoid.lcm ↑u a = ⇑normalize a
@[simp]
theorem
lcm_units_coe_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α)
(u : units α) :
gcd_monoid.lcm a ↑u = ⇑normalize a
@[simp]
theorem
lcm_one_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.lcm 1 a = ⇑normalize a
@[simp]
theorem
lcm_one_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.lcm a 1 = ⇑normalize a
@[simp]
theorem
lcm_same
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a : α) :
gcd_monoid.lcm a a = ⇑normalize a
@[simp]
theorem
lcm_eq_one_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
@[simp]
theorem
lcm_mul_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b c : α) :
gcd_monoid.lcm (a * b) (a * c) = ⇑normalize a * gcd_monoid.lcm b c
@[simp]
theorem
lcm_mul_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b c : α) :
gcd_monoid.lcm (b * a) (c * a) = gcd_monoid.lcm b c * ⇑normalize a
theorem
lcm_eq_left_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
theorem
lcm_eq_right_iff
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(a b : α) :
theorem
lcm_dvd_lcm_mul_left
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.lcm m n ∣ gcd_monoid.lcm (k * m) n
theorem
lcm_dvd_lcm_mul_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.lcm m n ∣ gcd_monoid.lcm (m * k) n
theorem
lcm_dvd_lcm_mul_left_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.lcm m n ∣ gcd_monoid.lcm m (k * n)
theorem
lcm_dvd_lcm_mul_right_right
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
(m n k : α) :
gcd_monoid.lcm m n ∣ gcd_monoid.lcm m (n * k)
theorem
gcd_monoid.prime_of_irreducible
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{x : α} :
irreducible x → prime x
theorem
gcd_monoid.irreducible_iff_prime
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[nontrivial α]
[gcd_monoid α]
{p : α} :
irreducible p ↔ prime p
@[instance]
Equations
- int.normalization_monoid = {norm_unit := λ (a : ℤ), ite (0 ≤ a) 1 (-1), norm_unit_zero := int.normalization_monoid._proof_1, norm_unit_mul := int.normalization_monoid._proof_2, norm_unit_coe_units := int.normalization_monoid._proof_3}
@[instance]
Equations
- int.gcd_monoid = {norm_unit := normalization_monoid.norm_unit int.normalization_monoid, norm_unit_zero := int.gcd_monoid._proof_1, norm_unit_mul := int.gcd_monoid._proof_2, norm_unit_coe_units := int.gcd_monoid._proof_3, gcd := λ (a b : ℤ), ↑(a.gcd b), lcm := λ (a b : ℤ), ↑(a.lcm b), gcd_dvd_left := int.gcd_monoid._proof_4, gcd_dvd_right := int.gcd_monoid._proof_5, dvd_gcd := int.gcd_monoid._proof_6, normalize_gcd := int.gcd_monoid._proof_7, gcd_mul_lcm := int.gcd_monoid._proof_8, lcm_zero_left := int.gcd_monoid._proof_9, lcm_zero_right := int.gcd_monoid._proof_10}
Maps an associate class of integers consisting of -n, n to n : ℕ
Equations
- associates_int_equiv_nat = {to_fun := λ (z : associates ℤ), z.out.nat_abs, inv_fun := λ (n : ℕ), associates.mk ↑n, left_inv := associates_int_equiv_nat._proof_1, right_inv := associates_int_equiv_nat._proof_2}
@[instance]
Equations
- nat.unique_units = {to_inhabited := {default := 1}, uniq := nat.units_eq_one}
theorem
units_eq_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique (units α)]
(u : units α) :
u = 1
@[instance]
def
normalization_monoid_of_unique_units
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique (units α)]
[nontrivial α] :
Equations
- normalization_monoid_of_unique_units = {norm_unit := λ (x : α), 1, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}
@[simp]
theorem
norm_unit_eq_one
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique (units α)]
[nontrivial α]
(x : α) :
@[simp]
theorem
normalize_eq
{α : Type u_1}
[comm_cancel_monoid_with_zero α]
[unique (units α)]
[nontrivial α]
(x : α) :