Basic results on unique factorization monoids

Main results

• prime_factors_unique: the prime factors of an element in a cancellative commutative monoid with zero (e.g. an integral domain) are unique up to associates
• UniqueFactorizationMonoid.factors_unique: the irreducible factors of an element in a unique factorization monoid (e.g. a UFD) are unique up to associates
• UniqueFactorizationMonoid.iff_exists_prime_factors: unique factorization exists iff each nonzero elements factors into a product of primes
• UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors: Euclid's lemma: if a ∣ b * c and a and c have no common prime factors, a ∣ b.
• UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors: Euclid's lemma: if a ∣ b * c and a and b have no common prime factors, a ∣ c.
• UniqueFactorizationMonoid.exists_reduced_factors: in a UFM, we can divide out a common factor to get relatively prime elements.

theorem WfDvdMonoid.of_wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] : WfDvdMonoid (Associates α) → WfDvdMonoid α

instance WfDvdMonoid.wfDvdMonoid_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] : WfDvdMonoid (Associates α)

theorem WfDvdMonoid.wellFoundedLT_associates {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] : WellFoundedLT (Associates α)

theorem WfDvdMonoid.of_wellFoundedLT_associates {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] (h : WellFoundedLT (Associates α)) : WfDvdMonoid α

theorem WfDvdMonoid.iff_wellFounded_associates {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] : WfDvdMonoid α ↔ WellFoundedLT (Associates α)

instance Associates.ufm {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] : UniqueFactorizationMonoid (Associates α)

theorem prime_factors_unique {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {f g : Multiset α} : (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → Associated f.prod g.prod → Multiset.Rel Associated f g

theorem UniqueFactorizationMonoid.factors_unique {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {f g : Multiset α} (hf : ∀ x ∈ f, Irreducible x) (hg : ∀ x ∈ g, Irreducible x) (h : Associated f.prod g.prod) : Multiset.Rel Associated f g

theorem Associated.card_factors_eq {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : (UniqueFactorizationMonoid.factors a).card = (UniqueFactorizationMonoid.factors b).card

theorem prime_factors_irreducible {α : Type u_1} [CommMonoidWithZero α] {a : α} {f : Multiset α} (ha : Irreducible a) (pfa : (∀ b ∈ f, Prime b) ∧ Associated f.prod a) : ∃ (p : α), Associated a p ∧ f = {p}

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

theorem irreducible_iff_prime_of_existsUnique_irreducible_factors {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) (p : α) : Irreducible p ↔ Prime p

@[simp]

theorem UniqueFactorizationMonoid.factors_one {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] : factors 1 = 0

theorem UniqueFactorizationMonoid.exists_mem_factors_of_dvd {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : p ∣ a → ∃ q ∈ factors a, Associated p q

theorem UniqueFactorizationMonoid.exists_mem_factors {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) : ∃ (p : α), p ∈ factors x

theorem UniqueFactorizationMonoid.factors_eq_singleton_of_irreducible {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) : ∃ (b : α), Associated a b ∧ factors a = {b}

theorem UniqueFactorizationMonoid.factors_mul {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : Multiset.Rel Associated (factors (x * y)) (factors x + factors y)

theorem UniqueFactorizationMonoid.factors_pow {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) : Multiset.Rel Associated (factors (x ^ n)) (n • factors x)

theorem UniqueFactorizationMonoid.factors_pow_count_prod {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α] {x : α} (hx : x ≠ 0) : Associated (∏ p ∈ (factors x).toFinset, p ^ Multiset.count p (factors x)) x

theorem UniqueFactorizationMonoid.factors_rel_of_associated {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : Multiset.Rel Associated (factors a) (factors b)

theorem UniqueFactorizationMonoid.factors_of_isUnit {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (hx : IsUnit x) : factors x = 0

@[simp]

theorem UniqueFactorizationMonoid.factors_eq_zero {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) : factors x = 0 ↔ IsUnit x

@[simp]

theorem UniqueFactorizationMonoid.factors_pos {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) : 0 < factors x ↔ ¬IsUnit x

theorem Associates.unique' {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {p q : Multiset (Associates α)} : (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q

theorem Associates.prod_le_prod_iff_le {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α] {p q : Multiset (Associates α)} (hp : ∀ a ∈ p, Irreducible a) (hq : ∀ a ∈ q, Irreducible a) : p.prod ≤ q.prod ↔ p ≤ q

theorem WfDvdMonoid.of_exists_prime_factors {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) : WfDvdMonoid α

theorem irreducible_iff_prime_of_exists_prime_factors {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) {p : α} : Irreducible p ↔ Prime p

theorem UniqueFactorizationMonoid.of_exists_prime_factors {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] (pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a) : UniqueFactorizationMonoid α

theorem UniqueFactorizationMonoid.iff_exists_prime_factors {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] : UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ Associated f.prod a

theorem MulEquiv.uniqueFactorizationMonoid {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] [CommMonoidWithZero β] (e : α ≃* β) (hα : UniqueFactorizationMonoid α) : UniqueFactorizationMonoid β

theorem MulEquiv.uniqueFactorizationMonoid_iff {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] [CommMonoidWithZero β] (e : α ≃* β) : UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β

theorem UniqueFactorizationMonoid.of_existsUnique_irreducible_factors {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] (eif : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a) (uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → Associated f.prod g.prod → Multiset.Rel Associated f g) : UniqueFactorizationMonoid α

theorem UniqueFactorizationMonoid.isRelPrime_iff_no_prime_factors {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} (ha : a ≠ 0) : IsRelPrime a b ↔ ∀ ⦃d : R⦄, d ∣ a → d ∣ b → ¬Prime d

theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b c : R} (ha : a ≠ 0) (h : ∀ ⦃d : R⦄, d ∣ a → d ∣ c → ¬Prime d) : a ∣ b * c → a ∣ b

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

theorem UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b c : R} (ha : a ≠ 0) (no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d) : a ∣ b * c → a ∣ c

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

theorem UniqueFactorizationMonoid.exists_reduced_factors {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] (a : R) : a ≠ 0 → ∀ (b : R), ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ 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 UniqueFactorizationMonoid.exists_reduced_factors' {R : Type u_2} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] (a b : R) (hb : b ≠ 0) : ∃ (a' : R) (b' : R) (c' : R), IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b