mathlib documentation

ring_theory.unique_factorization_domain

@[class]
structure wf_dvd_monoid (α : Type u_2) [comm_monoid_with_zero α] :
Prop

Well-foundedness of the strict version of |, which is equivalent to the descending chain condition on divisibility and to the ascending chain condition on principal ideals in an integral domain.

Instances
theorem wf_dvd_monoid.exists_irreducible_factor {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] {a : α} :
¬is_unit aa 0(∃ (i : α), irreducible i i a)

theorem wf_dvd_monoid.induction_on_irreducible {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] {P : α → Prop} (a : α) :
P 0(∀ (u : α), is_unit uP u)(∀ (a i : α), a 0irreducible iP aP (i * a))P a

theorem wf_dvd_monoid.exists_factors {α : Type u_1} [comm_monoid_with_zero α] [wf_dvd_monoid α] (a : α) :
a 0(∃ (f : multiset α), (∀ (b : α), b firreducible b) associated f.prod a)

@[class]
structure unique_factorization_monoid (α : Type u_2) [comm_cancel_monoid_with_zero α] :
Prop

unique factorization monoids.

These are defined as comm_cancel_monoid_with_zeros with well-founded strict divisibility relations, but this is equivalent to more familiar definitions:

Each element (except zero) is uniquely represented as a multiset of irreducible factors. Uniqueness is only up to associated elements.

Each element (except zero) is non-uniquely represented as a multiset of prime factors.

To define a UFD using the definition in terms of multisets of irreducible factors, use the definition of_exists_unique_irreducible_factors

To define a UFD using the definition in terms of multisets of prime factors, use the definition of_exists_prime_factors

Instances
theorem unique_factorization_monoid.exists_prime_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] (a : α) :
a 0(∃ (f : multiset α), (∀ (b : α), b fprime b) associated f.prod a)

theorem unique_factorization_monoid.induction_on_prime {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] {P : α → Prop} (a : α) :
P 0(∀ (x : α), is_unit xP x)(∀ (a p : α), a 0prime pP aP (p * a))P a

theorem unique_factorization_monoid.factors_unique {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] {f g : multiset α} :
(∀ (x : α), x firreducible x)(∀ (x : α), x girreducible x)associated f.prod g.prodmultiset.rel associated f g

theorem prime_factors_unique {α : Type u_1} [comm_cancel_monoid_with_zero α] {f g : multiset α} :
(∀ (x : α), x fprime x)(∀ (x : α), x gprime x)associated f.prod g.prodmultiset.rel associated f g

theorem prime_factors_irreducible {α : Type u_1} [comm_cancel_monoid_with_zero α] {a : α} {f : multiset α} :
irreducible a(∀ (b : α), b fprime b) associated f.prod a(∃ (p : α), associated a p f = p ::ₘ 0)

If an irreducible has a prime factorization, then it is an associate of one of its prime factors.

theorem wf_dvd_monoid.of_exists_prime_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] :
(∀ (a : α), a 0(∃ (f : multiset α), (∀ (b : α), b fprime b) associated f.prod a))wf_dvd_monoid α

theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] (pf : ∀ (a : α), a 0(∃ (f : multiset α), (∀ (b : α), b fprime b) associated f.prod a)) {p : α} :

theorem unique_factorization_monoid.of_exists_prime_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] :
(∀ (a : α), a 0(∃ (f : multiset α), (∀ (b : α), b fprime b) associated f.prod a))unique_factorization_monoid α

theorem unique_factorization_monoid.iff_exists_prime_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] :
unique_factorization_monoid α ∀ (a : α), a 0(∃ (f : multiset α), (∀ (b : α), b fprime b) associated f.prod a)

theorem irreducible_iff_prime_of_exists_unique_irreducible_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] (eif : ∀ (a : α), a 0(∃ (f : multiset α), (∀ (b : α), b firreducible b) associated f.prod a)) (uif : ∀ (f g : multiset α), (∀ (x : α), x firreducible x)(∀ (x : α), x girreducible x)associated f.prod g.prodmultiset.rel associated f g) (p : α) :

theorem unique_factorization_monoid.of_exists_unique_irreducible_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] :
(∀ (a : α), a 0(∃ (f : multiset α), (∀ (b : α), b firreducible b) associated f.prod a))(∀ (f g : multiset α), (∀ (x : α), x firreducible x)(∀ (x : α), x girreducible x)associated f.prod g.prodmultiset.rel associated f g)unique_factorization_monoid α

Noncomputably determines the multiset of prime factors.

Equations

Noncomputably defines a normalization_monoid structure on a unique_factorization_monoid.

Equations
theorem unique_factorization_monoid.no_factors_of_no_prime_factors {R : Type u_2} [comm_cancel_monoid_with_zero R] [unique_factorization_monoid R] {a b : R} (ha : a 0) (h : ∀ {d : R}, d ad b¬prime d) {d : R} :
d ad bis_unit d

theorem unique_factorization_monoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} [comm_cancel_monoid_with_zero R] [unique_factorization_monoid R] {a b c : R} :
a 0(∀ {d : R}, d ad c¬prime d)a b * ca b

Euclid's lemma: if a ∣ b * c and a and c have no common prime factors, a ∣ b. Compare is_coprime.dvd_of_dvd_mul_left.

theorem unique_factorization_monoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} [comm_cancel_monoid_with_zero R] [unique_factorization_monoid R] {a b c : R} :
a 0(∀ {d : R}, d ad b¬prime d)a b * ca c

Euclid's lemma: if a ∣ b * c and a and b have no common prime factors, a ∣ c. Compare is_coprime.dvd_of_dvd_mul_right.

theorem unique_factorization_monoid.exists_reduced_factors {R : Type u_2} [comm_cancel_monoid_with_zero R] [unique_factorization_monoid R] (a : R) (H : a 0) (b : R) :
∃ (a' b' c' : R), (∀ {d : R}, d a'd b'is_unit d) c' * a' = a c' * b' = b

If a ≠ 0, b are elements of a unique factorization domain, then dividing out their common factor c' gives a' and b' with no factors in common.

theorem unique_factorization_monoid.exists_reduced_factors' {R : Type u_2} [comm_cancel_monoid_with_zero R] [unique_factorization_monoid R] (a b : R) :
b 0(∃ (a' b' c' : R), (∀ {d : R}, d a'd b'is_unit d) c' * a' = a c' * b' = b)

def associates.factor_set (α : Type u) [comm_cancel_monoid_with_zero α] :
Type u

factor_set α representation elements of unique factorization domain as multisets. multiset α produced by factors are only unique up to associated elements, while the multisets in factor_set α are unqiue by equality and restricted to irreducible elements. This gives us a representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete lattice struture. Infimum is the greatest common divisor and supremum is the least common multiple.

Equations
theorem associates.factor_set.coe_add {α : Type u_1} [comm_cancel_monoid_with_zero α] {a b : multiset {a // irreducible a}} :
(a + b) = a + b

Evaluates the product of a factor_set to be the product of the corresponding multiset, or 0 if there is none.

Equations
@[simp]
theorem associates.prod_top {α : Type u_1} [comm_cancel_monoid_with_zero α] :

@[simp]
theorem associates.prod_coe {α : Type u_1} [comm_cancel_monoid_with_zero α] {s : multiset {a // irreducible a}} :

@[simp]
theorem associates.prod_add {α : Type u_1} [comm_cancel_monoid_with_zero α] (a b : associates.factor_set α) :
(a + b).prod = (a.prod) * b.prod

theorem associates.prod_mono {α : Type u_1} [comm_cancel_monoid_with_zero α] {a b : associates.factor_set α} :
a ba.prod b.prod

bcount p s is the multiplicity of p in the factor_set s (with bundled p)

Equations
def associates.count {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] :

count p s is the multiplicity of the irreducible p in the factor_set s.

If p is not irreducible, count p s is defined to be 0.

Equations
@[simp]
theorem associates.count_some {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] {p : associates α} (hp : irreducible p) (s : multiset {a // irreducible a}) :
p.count (some s) = multiset.count p, hp⟩ s

@[simp]
theorem associates.count_zero {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] {p : associates α} :
irreducible pp.count 0 = 0

theorem associates.count_reducible {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [decidable_eq (associates α)] {p : associates α} :

def associates.bfactor_set_mem {α : Type u_1} [comm_cancel_monoid_with_zero α] :
{a // irreducible a}associates.factor_set α → Prop

membership in a factor_set (bundled version)

Equations
def associates.factor_set_mem {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] :

factor_set_mem p s is the predicate that the irreducible p is a member of s : factor_set α.

If p is not irreducible, p is not a member of any factor_set.

Equations
@[simp]
theorem associates.factor_set_mem_eq_mem {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] (p : associates α) (s : associates.factor_set α) :
p.factor_set_mem s = (p s)

theorem associates.mem_factor_set_top {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] {p : associates α} :
∀ {hp : irreducible p}, p

theorem associates.mem_factor_set_some {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] {p : associates α} {hp : irreducible p} {l : multiset {a // irreducible a}} :
p l p, hp⟩ l

theorem associates.reducible_not_mem_factor_set {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] {p : associates α} (hp : ¬irreducible p) (s : associates.factor_set α) :
p s

theorem associates.unique' {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] {p q : multiset (associates α)} :
(∀ (a : associates α), a pirreducible a)(∀ (a : associates α), a qirreducible a)p.prod = q.prodp = q

theorem associates.prod_le_prod_iff_le {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] {p q : multiset (associates α)} :
(∀ (a : associates α), a pirreducible a)(∀ (a : associates α), a qirreducible a)(p.prod q.prod p q)

This returns the multiset of irreducible factors as a factor_set, a multiset of irreducible associates with_top.

Equations

This returns the multiset of irreducible factors of an associate as a factor_set, a multiset of irreducible associates with_top.

Equations
theorem associates.sup_mul_inf {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] (a b : associates α) :
(a b) * (a b) = a * b

theorem associates.dvd_of_mem_factors {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : associates α} :
∀ {hp : irreducible p}, p a.factorsp a

theorem associates.dvd_of_mem_factors' {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] {a : α} {p : associates α} {hp : irreducible p} :
∀ {hz : a 0}, p, hp⟩ associates.factors' ap associates.mk a

theorem associates.mem_factors'_iff_dvd {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] {a p : α} (ha0 : a 0) (hp : irreducible p) :

theorem associates.mem_factors_of_dvd {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a p : α} :

theorem associates.exists_prime_dvd_of_not_inf_one {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : α} :
a 0b 0associates.mk a associates.mk b 1(∃ (p : α), prime p p a p b)

theorem associates.coprime_iff_inf_one {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : α} :
a 0b 0(associates.mk a associates.mk b = 1 ∀ {d : α}, d ad b¬prime d)

theorem associates.prime_pow_dvd_iff_le {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {m p : associates α} (h₁ : m 0) (h₂ : irreducible p) {k : } :
p ^ k m k p.count m.factors

theorem associates.le_of_count_ne_zero {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {m p : associates α} :
m 0irreducible pp.count m.factors 0p m

theorem associates.count_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {b : associates α} (hb : b 0) {p : associates α} :

theorem associates.count_of_coprime {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {b : associates α} (hb : b 0) (hab : ∀ (d : associates α), d ad b¬prime d) {p : associates α} :

theorem associates.count_mul_of_coprime {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {b : associates α} (hb : b 0) {p : associates α} :
irreducible p(∀ (d : associates α), d ad b¬prime d)p.count a.factors = 0 p.count a.factors = p.count (a * b).factors

theorem associates.count_mul_of_coprime' {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {b : associates α} (hb : b 0) {p : associates α} :
irreducible p(∀ (d : associates α), d ad b¬prime d)p.count (a * b).factors = p.count a.factors p.count (a * b).factors = p.count b.factors

theorem associates.dvd_count_of_dvd_count_mul {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a b : associates α} (ha : a 0) (hb : b 0) {p : associates α} (hp : irreducible p) (hab : ∀ (d : associates α), d ad b¬prime d) {k : } :
k p.count (a * b).factorsk p.count a.factors

@[simp]

theorem associates.count_pow {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {p : associates α} (hp : irreducible p) (k : ) :
p.count (a ^ k).factors = k * p.count a.factors

theorem associates.dvd_count_pow {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {p : associates α} (hp : irreducible p) (k : ) :
k p.count (a ^ k).factors

theorem associates.is_pow_of_dvd_count {α : Type u_1} [comm_cancel_monoid_with_zero α] [dec_irr : Π (p : associates α), decidable (irreducible p)] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] [dec : decidable_eq α] [dec' : decidable_eq (associates α)] {a : associates α} (ha : a 0) {k : } :
(∀ (p : associates α), irreducible pk p.count a.factors)(∃ (b : associates α), a = b ^ k)

theorem associates.eq_pow_of_mul_eq_pow {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] [nontrivial α] [normalization_monoid α] {a b c : associates α} (ha : a 0) (hb : b 0) (hab : ∀ (d : associates α), d ad b¬prime d) {k : } :
a * b = c ^ k(∃ (d : associates α), a = d ^ k)

to_gcd_monoid constructs a GCD monoid out of a normalization on a unique factorization domain.

Equations