Unique factorization and normalization

Main definitions

• UniqueFactorizationMonoid.normalizedFactors: choose a multiset of prime factors that are unique by normalizing them.
• UniqueFactorizationMonoid.normalizationMonoid: choose a way of normalizing the elements of a UFM

noncomputable def UniqueFactorizationMonoid.normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a : α) : Multiset α

Noncomputably determines the multiset of prime factors.

Equations

• UniqueFactorizationMonoid.normalizedFactors a = Multiset.map (⇑normalize) (UniqueFactorizationMonoid.factors a)

@[simp]

theorem UniqueFactorizationMonoid.factors_eq_normalizedFactors {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Subsingleton Mˣ] (x : M) : factors x = normalizedFactors x

An arbitrary choice of factors of x : M is exactly the (unique) normalized set of factors, if M has a trivial group of units.

theorem UniqueFactorizationMonoid.prod_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) : Associated (normalizedFactors a).prod a

@[deprecated UniqueFactorizationMonoid.prod_normalizedFactors (since := "2024-12-04")]

theorem UniqueFactorizationMonoid.normalizedFactors_prod {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) : Associated (normalizedFactors a).prod a

Alias of UniqueFactorizationMonoid.prod_normalizedFactors.

theorem UniqueFactorizationMonoid.prod_normalizedFactors_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ane0 : a ≠ 0) : (normalizedFactors a).prod = normalize a

theorem UniqueFactorizationMonoid.prime_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ normalizedFactors a → Prime x

theorem UniqueFactorizationMonoid.irreducible_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ normalizedFactors a → Irreducible x

theorem UniqueFactorizationMonoid.normalize_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (x : α) : x ∈ normalizedFactors a → normalize x = x

theorem UniqueFactorizationMonoid.dvd_of_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a x : α} (hx : x ∈ normalizedFactors a) : x ∣ a

theorem UniqueFactorizationMonoid.normalizedFactors_irreducible {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a : α} (ha : Irreducible a) : normalizedFactors a = {normalize a}

theorem UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (a p : α) : p ∈ normalizedFactors a → ∀ q ∈ normalizedFactors a, p ∣ q → p = q

theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : p ∣ a → ∃ q ∈ normalizedFactors a, Associated p q

theorem UniqueFactorizationMonoid.exists_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) : ∃ (p : α), p ∈ normalizedFactors x

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_zero {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : normalizedFactors 0 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_one {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] : normalizedFactors 1 = 0

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_mul {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (n : ℕ) : normalizedFactors (x ^ n) = n • normalizedFactors x

theorem Irreducible.normalizedFactors_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) : UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

theorem UniqueFactorizationMonoid.normalizedFactors_prod_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) : normalizedFactors s.prod = Multiset.map (⇑normalize) s

theorem UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y

theorem Associated.normalizedFactors_eq {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (h : Associated a b) : UniqueFactorizationMonoid.normalizedFactors a = UniqueFactorizationMonoid.normalizedFactors b

theorem UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : Associated x y ↔ normalizedFactors x = normalizedFactors y

theorem UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p : α} (hp : Irreducible p) (k : ℕ) : normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

theorem UniqueFactorizationMonoid.zero_notMem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) : 0 ∉ normalizedFactors x

@[deprecated UniqueFactorizationMonoid.zero_notMem_normalizedFactors (since := "2025-05-23")]

theorem UniqueFactorizationMonoid.zero_not_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) : 0 ∉ normalizedFactors x

Alias of UniqueFactorizationMonoid.zero_notMem_normalizedFactors.

theorem UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a p : α} (H : p ∈ normalizedFactors a) : p ∣ a

theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton αˣ] {p x : α} (hx : x ≠ 0) : p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x

theorem UniqueFactorizationMonoid.mem_normalizedFactors_iff' {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p x : α} (h : x ≠ 0) : p ∈ normalizedFactors x ↔ Irreducible p ∧ normalize p = p ∧ p ∣ x

theorem UniqueFactorizationMonoid.disjoint_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b : α} (hc : IsRelPrime a b) : Disjoint (normalizedFactors a) (normalizedFactors b)

Relatively prime elements have disjoint prime factors (as multisets).

theorem UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {p r : α} (h : ∀ {m : α}, m ∈ normalizedFactors r → m = p) (hr : r ≠ 0) : ∃ (i : ℕ), Associated (p ^ i) r

theorem UniqueFactorizationMonoid.normalizedFactors_prod_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] [Subsingleton αˣ] {m : Multiset α} (h : ∀ p ∈ m, Prime p) : normalizedFactors m.prod = m

theorem UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {a b c : α} (ha : a ∈ normalizedFactors c) (hb : b ∈ normalizedFactors c) (h : Associated a b) : a = b

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactors_pos {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (x : α) (hx : x ≠ 0) : 0 < normalizedFactors x ↔ ¬IsUnit x

theorem UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : x ≠ 0) : normalizedFactors x = 0 ↔ IsUnit x

The multiset of normalized factors of x is nil if and only if x is a unit. The converse is true without the nonzero assumption, see normalizedFactors_of_isUnit.

theorem UniqueFactorizationMonoid.normalizedFactors_of_isUnit {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x : α} (hx : IsUnit x) : normalizedFactors x = 0

If x is a unit, then the multiset of normalized factors of x is nil. The converse is true with a nonzero assumption, see normalizedFactors_eq_zero_iff.

theorem UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y

theorem UniqueFactorizationMonoid.normalizedFactors_multiset_prod {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (s : Multiset α) (hs : 0 ∉ s) : normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum

def UniqueFactorizationMonoid.normalizedFactorsEquiv {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} [DecidableEq α] (he : ∀ (x : α), normalize (f x) = f (normalize x)) (a : α) : { x : α // x ∈ normalizedFactors a } ≃ { y : β // y ∈ normalizedFactors (f a) }

If the monoid equiv f : α ≃* β commutes with normalize then, for a : α, it yields a bijection between the normalizedFactors of a and of f a.

Equations

• UniqueFactorizationMonoid.normalizedFactorsEquiv he a = (↑f).subtypeEquiv ⋯

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_apply {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} [DecidableEq α] (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a p : α} (hp : p ∈ normalizedFactors a) : ↑((normalizedFactorsEquiv he a) ⟨p, hp⟩) = f p

@[simp]

theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} [DecidableEq α] (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a : α} {q : β} (hq : q ∈ normalizedFactors (f a)) : ↑((normalizedFactorsEquiv he a).symm ⟨q, hq⟩) = (↑f).symm q

noncomputable def UniqueFactorizationMonoid.normalizationMonoid {α : Type u_1} [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : NormalizationMonoid α

Noncomputably defines a normalizationMonoid structure on a UniqueFactorizationMonoid.

Equations

• One or more equations did not get rendered due to their size.