Unique factorization

Main Definitions

• WfDvdMonoid holds for Monoids for which a strict divisibility relation is well-founded.
• UniqueFactorizationMonoid holds for WfDvdMonoids where Irreducible is equivalent to Prime

@[reducible, inline]

abbrev WfDvdMonoid (α : Type u_2) [CommMonoidWithZero α] : 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.

Equations

• WfDvdMonoid α = IsWellFounded α DvdNotUnit

theorem wellFounded_dvdNotUnit {α : Type u_2} [CommMonoidWithZero α] [h : WfDvdMonoid α] : WellFounded DvdNotUnit

theorem WfDvdMonoid.exists_irreducible_factor {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {a : α} (ha : ¬IsUnit a) (ha0 : a ≠ 0) : ∃ (i : α), Irreducible i ∧ i ∣ a

theorem WfDvdMonoid.induction_on_irreducible {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {motive : α → Prop} (a : α) (zero : motive 0) (unit : ∀ (u : α), IsUnit u → motive u) (mul : ∀ (a i : α), a ≠ 0 → Irreducible i → motive a → motive (i * a)) : motive a

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

theorem WfDvdMonoid.not_unit_iff_exists_factors_eq {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] (a : α) (hn0 : a ≠ 0) : ¬IsUnit a ↔ ∃ (f : Multiset α), (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅

theorem WfDvdMonoid.isRelPrime_of_no_irreducible_factors {α : Type u_1} [CommMonoidWithZero α] [WfDvdMonoid α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ (z : α), Irreducible z → z ∣ x → ¬z ∣ y) : IsRelPrime x y

class UniqueFactorizationMonoid (α : Type u_2) [CommMonoidWithZero α] extends IsCancelMulZero α, IsWellFounded α DvdNotUnit : Prop

Unique factorization monoids are defined as cancellative CommMonoidWithZeros 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_existsUnique_irreducible_factors

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

• mul_left_cancel_of_ne_zero {a : α} : a ≠ 0 → IsLeftRegular a
• mul_right_cancel_of_ne_zero {a : α} : a ≠ 0 → IsRightRegular a
• wf : WellFounded DvdNotUnit
• irreducible_iff_prime {a : α} : Irreducible a ↔ Prime a

@[instance 100]

instance ufm_of_decomposition_of_wfDvdMonoid {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] [WfDvdMonoid α] [DecompositionMonoid α] : UniqueFactorizationMonoid α

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

theorem UniqueFactorizationMonoid.exists_prime_iff {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] : (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x

theorem UniqueFactorizationMonoid.induction_on_prime {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ (x : α), IsUnit x → P x) (h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)) : P a

instance UniqueFactorizationMonoid.instDecompositionMonoid {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] : DecompositionMonoid α

noncomputable def UniqueFactorizationMonoid.factors {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] (a : α) : Multiset α

Noncomputably determines the multiset of prime factors.

Equations

• UniqueFactorizationMonoid.factors a = if h : a = 0 then 0 else Classical.choose ⋯

theorem UniqueFactorizationMonoid.factors_prod {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) : Associated (factors a).prod a

@[simp]

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

theorem UniqueFactorizationMonoid.ne_zero_of_mem_factors {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {p a : α} (h : p ∈ factors a) : a ≠ 0

theorem UniqueFactorizationMonoid.dvd_of_mem_factors {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {p a : α} (h : p ∈ factors a) : p ∣ a

theorem UniqueFactorizationMonoid.prime_of_factor {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (x : α) (hx : x ∈ factors a) : Prime x

theorem UniqueFactorizationMonoid.irreducible_of_factor {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ factors a → Irreducible x

theorem UniqueFactorizationMonoid.card_factors_of_irreducible {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) : (factors a).card = 1