Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

UniqueFactorizationMonoid.normalizedFactors definition

(a : α) : Multiset α

Full source

/-- Noncomputably determines the multiset of prime factors. -/
noncomputable def normalizedFactors (a : α) : Multiset α :=
  Multiset.map normalize <| factors a

Normalized prime factorization multiset

Informal description

For any nonzero element $ a $ in a unique factorization monoid $ \alpha $, the function returns the multiset of prime factors of $ a $ (with multiplicities) after normalizing each factor. If $ a = 0 $, it returns the empty multiset.

UniqueFactorizationMonoid.factors_eq_normalizedFactors theorem

 {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] [Subsingleton Mˣ] (x : M) :
  factors x = normalizedFactors x

Full source

/-- An arbitrary choice of factors of `x : M` is exactly the (unique) normalized set of factors,
if `M` has a trivial group of units. -/
@[simp]
theorem factors_eq_normalizedFactors {M : Type*} [CancelCommMonoidWithZero M]
    [UniqueFactorizationMonoid M] [Subsingleton Mˣ] (x : M) : factors x = normalizedFactors x := by
  unfold normalizedFactors
  convert (Multiset.map_id (factors x)).symm
  ext p
  exact normalize_eq p

Factorization Equals Normalized Factorization in UFM with Trivial Units

Informal description

Let $M$ be a unique factorization monoid with a trivial group of units (i.e., the only units are the identity elements). Then for any element $x \in M$, the multiset of prime factors of $x$ is equal to its normalized multiset of prime factors, i.e., $\mathrm{factors}(x) = \mathrm{normalizedFactors}(x)$.

UniqueFactorizationMonoid.prod_normalizedFactors theorem

{a : α} (ane0 : a ≠ 0) : Associated (normalizedFactors a).prod a

Full source

theorem prod_normalizedFactors {a : α} (ane0 : a ≠ 0) :
    Associated (normalizedFactors a).prod a := by
  rw [normalizedFactors, factors, dif_neg ane0]
  refine Associated.trans ?_ (Classical.choose_spec (exists_prime_factors a ane0)).2
  rw [← Associates.mk_eq_mk_iff_associated, ← Associates.prod_mk, ← Associates.prod_mk,
    Multiset.map_map]
  congr 2
  ext
  rw [Function.comp_apply, Associates.mk_normalize]

Product of Normalized Prime Factors is Associated to Original Element

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$, the product of the elements in the multiset of normalized prime factors of $a$ is associated with $a$. That is, if $f$ is the multiset of normalized prime factors of $a$, then $\prod f \sim a$, where $\sim$ denotes the associated relation (differing by a unit factor).

UniqueFactorizationMonoid.prod_normalizedFactors_eq theorem

{a : α} (ane0 : a ≠ 0) : (normalizedFactors a).prod = normalize a

Full source

theorem prod_normalizedFactors_eq {a : α} (ane0 : a ≠ 0) :
    (normalizedFactors a).prod = normalize a := by
  trans normalize (normalizedFactors a).prod
  · rw [normalizedFactors, ← map_multiset_prod, normalize_idem]
  · exact normalize_eq_normalize_iff.mpr (dvd_dvd_iff_associated.mpr (prod_normalizedFactors ane0))

Product of Normalized Factors Equals Normalization of Element in UFM

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$, the product of the normalized prime factors of $a$ equals the normalization of $a$. That is, if $f$ is the multiset of normalized prime factors of $a$, then $\prod f = \text{normalize}(a)$.

UniqueFactorizationMonoid.prime_of_normalized_factor theorem

{a : α} : ∀ x : α, x ∈ normalizedFactors a → Prime x

Full source

theorem prime_of_normalized_factor {a : α} : ∀ x : α, x ∈ normalizedFactors a → Prime x := by
  rw [normalizedFactors, factors]
  split_ifs with ane0; · simp
  intro x hx; rcases Multiset.mem_map.1 hx with ⟨y, ⟨hy, rfl⟩⟩
  rw [(normalize_associated _).prime_iff]
  exact (Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 y hy

Normalized Factors are Prime in a Unique Factorization Monoid

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$, every element $x$ in the multiset of normalized prime factors of $a$ is a prime element.

UniqueFactorizationMonoid.irreducible_of_normalized_factor theorem

{a : α} : ∀ x : α, x ∈ normalizedFactors a → Irreducible x

Full source

theorem irreducible_of_normalized_factor {a : α} :
    ∀ x : α, x ∈ normalizedFactors a → Irreducible x := fun x h =>
  (prime_of_normalized_factor x h).irreducible

Irreducibility of Normalized Factors in a Unique Factorization Monoid

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$, every element $x$ in the multiset of normalized prime factors of $a$ is irreducible.

UniqueFactorizationMonoid.normalize_normalized_factor theorem

{a : α} : ∀ x : α, x ∈ normalizedFactors a → normalize x = x

Full source

theorem normalize_normalized_factor {a : α} :
    ∀ x : α, x ∈ normalizedFactors a → normalize x = x := by
  rw [normalizedFactors, factors]
  split_ifs with h; · simp
  intro x hx
  obtain ⟨y, _, rfl⟩ := Multiset.mem_map.1 hx
  apply normalize_idem

Normalized Factors are Already Normalized

Informal description

For any element $a$ in a unique factorization monoid $\alpha$, if $x$ is a prime factor in the normalized multiset factorization of $a$, then $x$ is already normalized, i.e., $\text{normalize}(x) = x$.

UniqueFactorizationMonoid.normalizedFactors_irreducible theorem

{a : α} (ha : Irreducible a) : normalizedFactors a = {normalize a}

Full source

theorem normalizedFactors_irreducible {a : α} (ha : Irreducible a) :
    normalizedFactors a = {normalize a} := by
  obtain ⟨p, a_assoc, hp⟩ :=
    prime_factors_irreducible ha ⟨prime_of_normalized_factor, prod_normalizedFactors ha.ne_zero⟩
  have p_mem : p ∈ normalizedFactors a := by
    rw [hp]
    exact Multiset.mem_singleton_self _
  convert hp
  rwa [← normalize_normalized_factor p p_mem, normalize_eq_normalize_iff, dvd_dvd_iff_associated]

Normalized Factors of an Irreducible Element Form a Singleton Multiset

Informal description

For any irreducible element $a$ in a unique factorization monoid $\alpha$, the multiset of normalized prime factors of $a$ is the singleton multiset containing the normalization of $a$, i.e., $\text{normalizedFactors}(a) = \{\text{normalize}(a)\}$.

UniqueFactorizationMonoid.normalizedFactors_eq_of_dvd theorem

(a : α) : ∀ᵉ (p ∈ normalizedFactors a) (q ∈ normalizedFactors a), p ∣ q → p = q

Full source

theorem normalizedFactors_eq_of_dvd (a : α) :
    ∀ᵉ (p ∈ normalizedFactors a) (q ∈ normalizedFactors a), p ∣ q → p = q := by
  intro p hp q hq hdvd
  convert normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd) <;>
    apply (normalize_normalized_factor _ ‹_›).symm

Distinct Normalized Prime Factors are Incomparable under Divisibility

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$, if two elements $p$ and $q$ in the multiset of normalized prime factors of $a$ satisfy $p \mid q$, then $p = q$.

UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd theorem

{a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) : p ∣ a → ∃ q ∈ normalizedFactors a, p ~ᵤ q

Full source

theorem exists_mem_normalizedFactors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    p ∣ a → ∃ q ∈ normalizedFactors a, p ~ᵤ q := fun ⟨b, hb⟩ =>
  have hb0 : b ≠ 0 := fun hb0 => by simp_all
  have : Multiset.Rel Associated (p ::ₘ normalizedFactors b) (normalizedFactors a) :=
    factors_unique
      (fun _ hx =>
        (Multiset.mem_cons.1 hx).elim (fun h => h.symm ▸ hp) (irreducible_of_normalized_factor _))
      irreducible_of_normalized_factor
      (Associated.symm <|
        calc
          Multiset.prod (normalizedFactors a) ~ᵤ a := prod_normalizedFactors ha0
          _ = p * b := hb
          _ ~ᵤ Multiset.prod (p ::ₘ normalizedFactors b) := by
            rw [Multiset.prod_cons]
            exact (prod_normalizedFactors hb0).symm.mul_left _
          )
  Multiset.exists_mem_of_rel_of_mem this (by simp)

Existence of Associated Normalized Factor for Irreducible Divisors

Informal description

For any nonzero element $a$ and irreducible element $p$ in a unique factorization monoid $\alpha$, if $p$ divides $a$, then there exists an element $q$ in the multiset of normalized prime factors of $a$ such that $p$ is associated with $q$ (i.e., $p \sim q$).

UniqueFactorizationMonoid.exists_mem_normalizedFactors theorem

{x : α} (hx : x ≠ 0) (h : ¬IsUnit x) : ∃ p, p ∈ normalizedFactors x

Full source

theorem exists_mem_normalizedFactors {x : α} (hx : x ≠ 0) (h : ¬IsUnit x) :
    ∃ p, p ∈ normalizedFactors x := by
  obtain ⟨p', hp', hp'x⟩ := WfDvdMonoid.exists_irreducible_factor h hx
  obtain ⟨p, hp, _⟩ := exists_mem_normalizedFactors_of_dvd hx hp' hp'x
  exact ⟨p, hp⟩

Existence of Normalized Prime Factors for Nonzero Nonunits in UFM

Informal description

For any nonzero element $x$ in a unique factorization monoid $\alpha$ that is not a unit, there exists a prime element $p$ in the multiset of normalized prime factors of $x$.

UniqueFactorizationMonoid.normalizedFactors_zero theorem

: normalizedFactors (0 : α) = 0

Full source

@[simp]
theorem normalizedFactors_zero : normalizedFactors (0 : α) = 0 := by
  simp [normalizedFactors, factors]

Normalized Factors of Zero is Empty

Informal description

The multiset of normalized prime factors of the zero element in a unique factorization monoid $\alpha$ is the empty multiset, i.e., $\text{normalizedFactors}(0) = 0$.

UniqueFactorizationMonoid.normalizedFactors_one theorem

: normalizedFactors (1 : α) = 0

Full source

@[simp]
theorem normalizedFactors_one : normalizedFactors (1 : α) = 0 := by
  rcases subsingleton_or_nontrivial α with h | h
  · dsimp [normalizedFactors, factors]
    simp [Subsingleton.elim (1 : α) 0]
  · rw [← Multiset.rel_zero_right]
    apply factors_unique irreducible_of_normalized_factor
    · intro x hx
      exfalso
      apply Multiset.not_mem_zero x hx
    · apply prod_normalizedFactors one_ne_zero

Normalized Factors of One is Empty

Informal description

The multiset of normalized prime factors of the multiplicative identity element $1$ in a unique factorization monoid $\alpha$ is the empty multiset, i.e., $\text{normalizedFactors}(1) = 0$.

UniqueFactorizationMonoid.normalizedFactors_mul theorem

{x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y

Full source

@[simp]
theorem normalizedFactors_mul {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    normalizedFactors (x * y) = normalizedFactors x + normalizedFactors y := by
  have h : (normalize : α → α) = Associates.outAssociates.out ∘ Associates.mk := by
    ext
    rw [Function.comp_apply, Associates.out_mk]
  rw [← Multiset.map_id' (normalizedFactors (x * y)), ← Multiset.map_id' (normalizedFactors x), ←
    Multiset.map_id' (normalizedFactors y), ← Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ←
    Multiset.map_congr rfl normalize_normalized_factor, ← Multiset.map_add, h, ←
    Multiset.map_map Associates.out, eq_comm, ← Multiset.map_map Associates.out]
  refine congr rfl ?_
  apply Multiset.map_mk_eq_map_mk_of_rel
  apply factors_unique
  · intro x hx
    rcases Multiset.mem_add.1 hx with (hx | hx) <;> exact irreducible_of_normalized_factor x hx
  · exact irreducible_of_normalized_factor
  · rw [Multiset.prod_add]
    exact
      ((prod_normalizedFactors hx).mul_mul (prod_normalizedFactors hy)).trans
        (prod_normalizedFactors (mul_ne_zero hx hy)).symm

Factorization of Product in Unique Factorization Monoid: $\text{normalizedFactors}(x \cdot y) = \text{normalizedFactors}(x) + \text{normalizedFactors}(y)$

Informal description

For any nonzero elements $x$ and $y$ in a unique factorization monoid $\alpha$, the multiset of normalized prime factors of their product $x \cdot y$ is equal to the sum of the multisets of normalized prime factors of $x$ and $y$, i.e., \[ \text{normalizedFactors}(x \cdot y) = \text{normalizedFactors}(x) + \text{normalizedFactors}(y). \]

UniqueFactorizationMonoid.normalizedFactors_pow theorem

{x : α} (n : ℕ) : normalizedFactors (x ^ n) = n • normalizedFactors x

Full source

@[simp]
theorem normalizedFactors_pow {x : α} (n : ℕ) :
    normalizedFactors (x ^ n) = n • normalizedFactors x := by
  induction' n with n ih
  · simp [zero_nsmul]
  by_cases h0 : x = 0
  · simp [h0, zero_pow n.succ_ne_zero, nsmul_zero]
  rw [pow_succ', succ_nsmul', normalizedFactors_mul h0 (pow_ne_zero _ h0), ih]

Factorization of Powers in Unique Factorization Monoid: $\text{normalizedFactors}(x^n) = n \cdot \text{normalizedFactors}(x)$

Informal description

For any nonzero element $x$ in a unique factorization monoid $\alpha$ and any natural number $n$, the multiset of normalized prime factors of $x^n$ is equal to $n$ times the multiset of normalized prime factors of $x$, i.e., \[ \text{normalizedFactors}(x^n) = n \cdot \text{normalizedFactors}(x). \]

Irreducible.normalizedFactors_pow theorem

{p : α} (hp : Irreducible p) (k : ℕ) : normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Full source

theorem _root_.Irreducible.normalizedFactors_pow {p : α} (hp : Irreducible p) (k : ℕ) :
    normalizedFactors (p ^ k) = Multiset.replicate k (normalize p) := by
  rw [UniqueFactorizationMonoid.normalizedFactors_pow, normalizedFactors_irreducible hp,
    Multiset.nsmul_singleton]

Factorization of Powers of Irreducible Elements: $\text{normalizedFactors}(p^k) = k \cdot \{\text{normalize}(p)\}$

Informal description

For any irreducible element $p$ in a unique factorization monoid $\alpha$ and any natural number $k$, the multiset of normalized prime factors of $p^k$ is equal to the multiset consisting of $k$ copies of the normalization of $p$, i.e., \[ \text{normalizedFactors}(p^k) = \{\text{normalize}(p), \dots, \text{normalize}(p)\} \quad (k \text{ times}). \]

UniqueFactorizationMonoid.normalizedFactors_prod_eq theorem

(s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) : normalizedFactors s.prod = s.map normalize

Full source

theorem normalizedFactors_prod_eq (s : Multiset α) (hs : ∀ a ∈ s, Irreducible a) :
    normalizedFactors s.prod = s.map normalize := by
  induction' s using Multiset.induction with a s ih
  · rw [Multiset.prod_zero, normalizedFactors_one, Multiset.map_zero]
  · have ia := hs a (Multiset.mem_cons_self a _)
    have ib := fun b h => hs b (Multiset.mem_cons_of_mem h)
    obtain rfl | ⟨b, hb⟩ := s.empty_or_exists_mem
    · rw [Multiset.cons_zero, Multiset.prod_singleton, Multiset.map_singleton,
        normalizedFactors_irreducible ia]
    haveI := nontrivial_of_ne b 0 (ib b hb).ne_zero
    rw [Multiset.prod_cons, Multiset.map_cons,
      normalizedFactors_mul ia.ne_zero (Multiset.prod_ne_zero fun h => (ib 0 h).ne_zero rfl),
      normalizedFactors_irreducible ia, ih ib, Multiset.singleton_add]

Factorization of Product of Irreducibles: $\text{normalizedFactors}(\prod s) = \text{map normalize } s$

Informal description

For any multiset $s$ of irreducible elements in a unique factorization monoid $\alpha$, the multiset of normalized prime factors of the product of all elements in $s$ is equal to the multiset obtained by normalizing each element of $s$. That is, \[ \text{normalizedFactors}\left(\prod s\right) = \text{map normalize } s. \]

UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors theorem

{x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y

Full source

theorem dvd_iff_normalizedFactors_le_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    x ∣ yx ∣ y ↔ normalizedFactors x ≤ normalizedFactors y := by
  constructor
  · rintro ⟨c, rfl⟩
    simp [hx, right_ne_zero_of_mul hy]
  · rw [← (prod_normalizedFactors hx).dvd_iff_dvd_left, ←
      (prod_normalizedFactors hy).dvd_iff_dvd_right]
    apply Multiset.prod_dvd_prod_of_le

Divisibility Criterion via Normalized Prime Factors: $x \mid y \leftrightarrow \text{normalizedFactors}(x) \leq \text{normalizedFactors}(y)$

Informal description

For any nonzero elements $x$ and $y$ in a unique factorization monoid $\alpha$, $x$ divides $y$ if and only if the multiset of normalized prime factors of $x$ is a sub-multiset of the multiset of normalized prime factors of $y$. That is, \[ x \mid y \leftrightarrow \text{normalizedFactors}(x) \leq \text{normalizedFactors}(y). \]

Associated.normalizedFactors_eq theorem

{a b : α} (h : Associated a b) : normalizedFactors a = normalizedFactors b

Full source

theorem _root_.Associated.normalizedFactors_eq {a b : α} (h : Associated a b) :
    normalizedFactors a = normalizedFactors b := by
  unfold normalizedFactors
  have h' : ⇑(normalize (α := α)) = Associates.outAssociates.out ∘ Associates.mk := funext Associates.out_mk
  rw [h', ← Multiset.map_map, ← Multiset.map_map,
    Associates.rel_associated_iff_map_eq_map.mp (factors_rel_of_associated h)]

Equality of Normalized Factors for Associated Elements

Informal description

For any two elements $a$ and $b$ in a unique factorization monoid $\alpha$, if $a$ and $b$ are associated (i.e., $a = u \cdot b$ for some unit $u$), then their normalized prime factor multisets are equal, i.e., $\text{normalizedFactors}(a) = \text{normalizedFactors}(b)$.

UniqueFactorizationMonoid.associated_iff_normalizedFactors_eq_normalizedFactors theorem

{x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : x ~ᵤ y ↔ normalizedFactors x = normalizedFactors y

Full source

theorem associated_iff_normalizedFactors_eq_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    x ~ᵤ yx ~ᵤ y ↔ normalizedFactors x = normalizedFactors y :=
  ⟨Associated.normalizedFactors_eq, fun h =>
    (prod_normalizedFactors hx).symm.trans (_root_.trans (by rw [h]) (prod_normalizedFactors hy))⟩

Associated Elements Have Equal Normalized Prime Factorizations

Informal description

For any nonzero elements $x$ and $y$ in a unique factorization monoid $\alpha$, $x$ and $y$ are associated (i.e., $x = u \cdot y$ for some unit $u$) if and only if their multisets of normalized prime factors are equal, i.e., $\text{normalizedFactors}(x) = \text{normalizedFactors}(y)$.

UniqueFactorizationMonoid.normalizedFactors_of_irreducible_pow theorem

{p : α} (hp : Irreducible p) (k : ℕ) : normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Full source

theorem normalizedFactors_of_irreducible_pow {p : α} (hp : Irreducible p) (k : ℕ) :
    normalizedFactors (p ^ k) = Multiset.replicate k (normalize p) := by
  rw [normalizedFactors_pow, normalizedFactors_irreducible hp, Multiset.nsmul_singleton]

Factorization of Powers of Irreducible Elements: $\text{normalizedFactors}(p^k) = k \cdot \{\text{normalize}(p)\}$

Informal description

For any irreducible element $p$ in a unique factorization monoid $\alpha$ and any natural number $k$, the multiset of normalized prime factors of $p^k$ consists of $k$ copies of the normalization of $p$, i.e., \[ \text{normalizedFactors}(p^k) = \{\text{normalize}(p), \dots, \text{normalize}(p)\} \] where the multiset contains $\text{normalize}(p)$ exactly $k$ times.

UniqueFactorizationMonoid.zero_not_mem_normalizedFactors theorem

(x : α) : (0 : α) ∉ normalizedFactors x

Full source

theorem zero_not_mem_normalizedFactors (x : α) : (0 : α) ∉ normalizedFactors x := fun h =>
  Prime.ne_zero (prime_of_normalized_factor _ h) rfl

Zero is Not a Normalized Prime Factor

Informal description

For any element $x$ in a unique factorization monoid $\alpha$, the zero element $0$ does not belong to the multiset of normalized prime factors of $x$.

UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors theorem

{a p : α} (H : p ∈ normalizedFactors a) : p ∣ a

Full source

theorem dvd_of_mem_normalizedFactors {a p : α} (H : p ∈ normalizedFactors a) : p ∣ a := by
  by_cases hcases : a = 0
  · rw [hcases]
    exact dvd_zero p
  · exact dvd_trans (Multiset.dvd_prod H) (Associated.dvd (prod_normalizedFactors hcases))

Prime Factor Divides Original Element in Unique Factorization Monoid

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$ and any prime element $p$ in the multiset of normalized prime factors of $a$, we have that $p$ divides $a$, i.e., $p \mid a$.

UniqueFactorizationMonoid.mem_normalizedFactors_iff theorem

[Subsingleton αˣ] {p x : α} (hx : x ≠ 0) : p ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x

Full source

theorem mem_normalizedFactors_iff [Subsingleton αˣ] {p x : α} (hx : x ≠ 0) :
    p ∈ normalizedFactors xp ∈ normalizedFactors x ↔ Prime p ∧ p ∣ x := by
  constructor
  · intro h
    exact ⟨prime_of_normalized_factor p h, dvd_of_mem_normalizedFactors h⟩
  · rintro ⟨hprime, hdvd⟩
    obtain ⟨q, hqmem, hqeq⟩ := exists_mem_normalizedFactors_of_dvd hx hprime.irreducible hdvd
    rw [associated_iff_eq] at hqeq
    exact hqeq ▸ hqmem

Characterization of Normalized Prime Factors in a UFM with Trivial Units

Informal description

Let $\alpha$ be a unique factorization monoid with a trivial group of units (i.e., $\alpha^\times$ is a subsingleton). For any nonzero element $x \in \alpha$ and any element $p \in \alpha$, the following are equivalent: 1. $p$ is in the multiset of normalized prime factors of $x$, 2. $p$ is a prime element and $p$ divides $x$. In other words, $p \in \text{normalizedFactors}(x) \iff \text{Prime}(p) \land p \mid x$.

UniqueFactorizationMonoid.exists_associated_prime_pow_of_unique_normalized_factor theorem

{p r : α} (h : ∀ {m}, m ∈ normalizedFactors r → m = p) (hr : r ≠ 0) : ∃ i : ℕ, Associated (p ^ i) r

Full source

theorem exists_associated_prime_pow_of_unique_normalized_factor {p r : α}
    (h : ∀ {m}, m ∈ normalizedFactors r → m = p) (hr : r ≠ 0) : ∃ i : ℕ, Associated (p ^ i) r := by
  use (normalizedFactors r).card
  have := UniqueFactorizationMonoid.prod_normalizedFactors hr
  rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this

Existence of Prime Power Associated to Element with Unique Normalized Factor

Informal description

Let $r$ be a nonzero element in a unique factorization monoid $\alpha$, and suppose that every element in the multiset of normalized prime factors of $r$ is equal to a fixed prime element $p$. Then there exists a natural number $i$ such that $r$ is associated with $p^i$, i.e., $r \sim p^i$.

UniqueFactorizationMonoid.normalizedFactors_prod_of_prime theorem

[Subsingleton αˣ] {m : Multiset α} (h : ∀ p ∈ m, Prime p) : normalizedFactors m.prod = m

Full source

theorem normalizedFactors_prod_of_prime [Subsingleton αˣ] {m : Multiset α}
    (h : ∀ p ∈ m, Prime p) : normalizedFactors m.prod = m := by
  cases subsingleton_or_nontrivial α
  · obtain rfl : m = 0 := by
      refine Multiset.eq_zero_of_forall_not_mem fun x hx ↦ ?_
      simpa [Subsingleton.elim x 0] using h x hx
    simp
  · simpa only [← Multiset.rel_eq, ← associated_eq_eq] using
      prime_factors_unique prime_of_normalized_factor h
        (prod_normalizedFactors (m.prod_ne_zero_of_prime h))

Normalized Factors of a Product of Primes in a UFM with Unique Units

Informal description

Let $\alpha$ be a unique factorization monoid such that the group of units $\alpha^\times$ is a subsingleton (i.e., all units are equal). For any multiset $m$ of prime elements in $\alpha$, the multiset of normalized prime factors of the product $\prod m$ is equal to $m$ itself, i.e., $\text{normalizedFactors}(\prod m) = m$.

UniqueFactorizationMonoid.mem_normalizedFactors_eq_of_associated theorem

{a b c : α} (ha : a ∈ normalizedFactors c) (hb : b ∈ normalizedFactors c) (h : Associated a b) : a = b

Full source

theorem mem_normalizedFactors_eq_of_associated {a b c : α} (ha : a ∈ normalizedFactors c)
    (hb : b ∈ normalizedFactors c) (h : Associated a b) : a = b := by
  rw [← normalize_normalized_factor a ha, ← normalize_normalized_factor b hb,
    normalize_eq_normalize_iff]
  exact Associated.dvd_dvd h

Uniqueness of Normalized Prime Factors up to Association

Informal description

Let $a$, $b$, and $c$ be elements of a unique factorization monoid $\alpha$, with $c \neq 0$. If $a$ and $b$ are both in the multiset of normalized prime factors of $c$ (i.e., $a \in \text{normalizedFactors}(c)$ and $b \in \text{normalizedFactors}(c)$) and $a$ is associated to $b$ (i.e., $a \sim b$), then $a = b$.

UniqueFactorizationMonoid.normalizedFactors_pos theorem

(x : α) (hx : x ≠ 0) : 0 < normalizedFactors x ↔ ¬IsUnit x

Full source

@[simp]
theorem normalizedFactors_pos (x : α) (hx : x ≠ 0) : 0 < normalizedFactors x ↔ ¬IsUnit x := by
  constructor
  · intro h hx
    obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'
    exact
      (prime_of_normalized_factor _ hp).not_unit
        (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)
  · intro h
    obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h
    exact
      bot_lt_iff_ne_bot.mpr
        (mt Multiset.eq_zero_iff_forall_not_mem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

Nonempty Normalized Factors Characterization for Nonunits in UFM

Informal description

For any nonzero element $x$ in a unique factorization monoid $\alpha$, the multiset of normalized prime factors of $x$ is nonempty (i.e., $0 < \text{normalizedFactors}(x)$) if and only if $x$ is not a unit.

UniqueFactorizationMonoid.dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors theorem

{x y : α} (hx : x ≠ 0) (hy : y ≠ 0) : DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y

Full source

theorem dvdNotUnit_iff_normalizedFactors_lt_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    DvdNotUnitDvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y := by
  constructor
  · rintro ⟨_, c, hc, rfl⟩
    simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne, not_false_iff,
      lt_add_iff_pos_right, normalizedFactors_pos, hc]
  · intro h
    exact
      dvdNotUnit_of_dvd_of_not_dvd
        ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
        (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_le)

Characterization of Non-Unit Divisibility via Normalized Factors: $x \mid_{\text{not unit}} y \leftrightarrow \text{normalizedFactors}(x) < \text{normalizedFactors}(y)$

Informal description

For any nonzero elements $x$ and $y$ in a unique factorization monoid $\alpha$, the following are equivalent: 1. $x$ is a non-unit divisor of $y$ (i.e., $x$ divides $y$ but is not a unit and does not differ from $y$ by a unit). 2. The multiset of normalized prime factors of $x$ is strictly contained in the multiset of normalized prime factors of $y$ (i.e., $\text{normalizedFactors}(x) < \text{normalizedFactors}(y)$).

UniqueFactorizationMonoid.normalizedFactors_multiset_prod theorem

(s : Multiset α) (hs : 0 ∉ s) : normalizedFactors (s.prod) = (s.map normalizedFactors).sum

Full source

theorem normalizedFactors_multiset_prod (s : Multiset α) (hs : 0 ∉ s) :
    normalizedFactors (s.prod) = (s.map normalizedFactors).sum := by
  cases subsingleton_or_nontrivial α
  · obtain rfl : s = 0 := by
      apply Multiset.eq_zero_of_forall_not_mem
      intro _
      convert hs
    simp
  induction s using Multiset.induction with
  | empty => simp
  | cons _ _ IH =>
    rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
    · exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
    · exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
    · apply Multiset.prod_ne_zero
      exact fun h ↦ hs (Multiset.mem_cons_of_mem h)

Factorization of Multiset Product in Unique Factorization Monoid

Informal description

For any multiset $s$ of elements in a unique factorization monoid $\alpha$ such that $0 \notin s$, the multiset of normalized prime factors of the product of $s$ is equal to the sum of the multisets of normalized prime factors of each element in $s$. That is, \[ \text{normalizedFactors}\left(\prod s\right) = \sum_{x \in s} \text{normalizedFactors}(x). \]

UniqueFactorizationMonoid.normalizationMonoid definition

: NormalizationMonoid α

Full source

/-- Noncomputably defines a `normalizationMonoid` structure on a `UniqueFactorizationMonoid`. -/
protected noncomputable def normalizationMonoid : NormalizationMonoid α :=
  normalizationMonoidOfMonoidHomRightInverse
    { toFun := fun a : Associates α =>
        if a = 0 then 0
        else
          ((normalizedFactors a).map
              (Classical.choose mk_surjective.hasRightInverse : Associates α → α)).prod
      map_one' := by nontriviality α; simp
      map_mul' := fun x y => by
        by_cases hx : x = 0
        · simp [hx]
        by_cases hy : y = 0
        · simp [hy]
        simp [hx, hy] }
    (by
      intro x
      dsimp
      by_cases hx : x = 0
      · simp [hx]
      have h : Associates.mkMonoidHomAssociates.mkMonoidHom ∘ Classical.choose mk_surjective.hasRightInverse =
          (id : Associates α → Associates α) := by
        ext x
        rw [Function.comp_apply, mkMonoidHom_apply,
          Classical.choose_spec mk_surjective.hasRightInverse x]
        rfl
      rw [if_neg hx, ← mkMonoidHom_apply, MonoidHom.map_multiset_prod, map_map, h, map_id, ←
        associated_iff_eq]
      apply prod_normalizedFactors hx)

Normalization monoid structure on a unique factorization monoid

Informal description

Given a unique factorization monoid $\alpha$, this definition noncomputably constructs a `NormalizationMonoid` structure on $\alpha$. The normalization is defined via a monoid homomorphism that maps each element to the product of its normalized prime factors (with multiplicities), and this homomorphism has a right inverse. Specifically, for any nonzero element $a \in \alpha$, the normalization homomorphism first computes the multiset of normalized prime factors of $a$ (using `normalizedFactors`), then maps each factor back to $\alpha$ via a chosen right inverse of the canonical projection to associates, and finally takes the product of this multiset. The zero element is mapped to zero. The construction ensures that the composition of the normalization homomorphism with the projection to associates is the identity.

Main definitions