Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Module docstring

{"# Unique factorization and multiplicity

Main results

UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors: The multiplicity of an irreducible factor of a nonzero element is exactly the number of times the normalized factor occurs in the normalizedFactors. "}

WfDvdMonoid.max_power_factor' theorem

 [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α} (h : a₀ ≠ 0) (hx : ¬IsUnit x) :
  ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

Full source

theorem WfDvdMonoid.max_power_factor' [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α}
    (h : a₀ ≠ 0) (hx : ¬IsUnit x) : ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a := by
  obtain ⟨a, ⟨n, rfl⟩, hm⟩ := wellFounded_dvdNotUnit.has_min
    {a | ∃ n, x ^ n * a = a₀} ⟨a₀, 0, by rw [pow_zero, one_mul]⟩
  refine ⟨n, a, ?_, rfl⟩; rintro ⟨d, rfl⟩
  exact hm d ⟨n + 1, by rw [pow_succ, mul_assoc]⟩
    ⟨(right_ne_zero_of_mul <| right_ne_zero_of_mul h), x, hx, mul_comm _ _⟩

Factorization of Nonzero Elements by Non-Units in Well-Founded Divisibility Monoids

Informal description

Let $\alpha$ be a commutative monoid with zero that is a well-founded divisibility monoid. For any nonzero element $a_0 \in \alpha$ and any non-unit element $x \in \alpha$, there exist a natural number $n$ and an element $a \in \alpha$ such that $x$ does not divide $a$ and $a_0 = x^n \cdot a$.

WfDvdMonoid.max_power_factor theorem

 [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α} (h : a₀ ≠ 0) (hx : Irreducible x) :
  ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

Full source

theorem WfDvdMonoid.max_power_factor [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α}
    (h : a₀ ≠ 0) (hx : Irreducible x) : ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a :=
  max_power_factor' h hx.not_isUnit

Factorization of Nonzero Elements by Irreducibles in Well-Founded Divisibility Monoids

Informal description

Let $\alpha$ be a commutative monoid with zero that is a well-founded divisibility monoid. For any nonzero element $a_0 \in \alpha$ and any irreducible element $x \in \alpha$, there exist a natural number $n$ and an element $a \in \alpha$ such that $x$ does not divide $a$ and $a_0 = x^n \cdot a$.

FiniteMultiplicity.of_not_isUnit theorem

[CancelCommMonoidWithZero α] [WfDvdMonoid α] {a b : α} (ha : ¬IsUnit a) (hb : b ≠ 0) : FiniteMultiplicity a b

Full source

theorem FiniteMultiplicity.of_not_isUnit [CancelCommMonoidWithZero α] [WfDvdMonoid α]
    {a b : α} (ha : ¬IsUnit a) (hb : b ≠ 0) : FiniteMultiplicity a b := by
  obtain ⟨n, c, ndvd, rfl⟩ := WfDvdMonoid.max_power_factor' hb ha
  exact ⟨n, by rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]⟩

Finite Multiplicity for Non-Units in Well-Founded Divisibility Monoids

Informal description

Let $\alpha$ be a cancelative commutative monoid with zero that is a well-founded divisibility monoid. For any non-unit element $a \in \alpha$ and any nonzero element $b \in \alpha$, the multiplicity of $a$ in $b$ is finite, i.e., there exists a natural number $n$ such that $a^n$ does not divide $b$.

FiniteMultiplicity.of_prime_left theorem

[CancelCommMonoidWithZero α] [WfDvdMonoid α] {a b : α} (ha : Prime a) (hb : b ≠ 0) : FiniteMultiplicity a b

Full source

theorem FiniteMultiplicity.of_prime_left [CancelCommMonoidWithZero α] [WfDvdMonoid α]
    {a b : α} (ha : Prime a) (hb : b ≠ 0) : FiniteMultiplicity a b :=
  .of_not_isUnit ha.not_unit hb

Finite Multiplicity for Primes in Well-Founded Divisibility Monoids

Informal description

Let $\alpha$ be a cancelative commutative monoid with zero that is a well-founded divisibility monoid. For any prime element $a \in \alpha$ and any nonzero element $b \in \alpha$, the multiplicity of $a$ in $b$ is finite, i.e., there exists a natural number $n$ such that $a^n$ does not divide $b$.

UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors theorem

 {a b : R} {n : ℕ} (ha : Irreducible a) (hb : b ≠ 0) :
  ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Full source

theorem le_emultiplicity_iff_replicate_le_normalizedFactors {a b : R} {n : ℕ} (ha : Irreducible a)
    (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b := by
  rw [← pow_dvd_iff_le_emultiplicity]
  revert b
  induction' n with n ih; · simp
  intro b hb
  constructor
  · rintro ⟨c, rfl⟩
    rw [Ne, pow_succ', mul_assoc, mul_eq_zero, not_or] at hb
    rw [pow_succ', mul_assoc, normalizedFactors_mul hb.1 hb.2, replicate_succ,
      normalizedFactors_irreducible ha, singleton_add, cons_le_cons_iff, ← ih hb.2]
    apply Dvd.intro _ rfl
  · rw [Multiset.le_iff_exists_add]
    rintro ⟨u, hu⟩
    rw [← (prod_normalizedFactors hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]
    exact (Associated.pow_pow <| associated_normalize a).dvd.trans (Dvd.intro u.prod rfl)

Extended Multiplicity Bound via Normalized Factors: $n \leq \text{emultiplicity}(a, b) \leftrightarrow \text{replicate}(n, \text{normalize}(a)) \leq \text{normalizedFactors}(b)$

Informal description

Let $R$ be a unique factorization monoid, and let $a, b \in R$ with $a$ irreducible and $b \neq 0$. For any natural number $n$, the extended multiplicity of $a$ in $b$ is at least $n$ if and only if the multiset consisting of $n$ copies of the normalization of $a$ is a sub-multiset of the normalized prime factors of $b$. In symbols: \[ n \leq \text{emultiplicity}(a, b) \leftrightarrow \text{replicate}(n, \text{normalize}(a)) \leq \text{normalizedFactors}(b). \]

UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors theorem

 [DecidableEq R] {a b : R} (ha : Irreducible a) (hb : b ≠ 0) :
  emultiplicity a b = (normalizedFactors b).count (normalize a)

Full source

/-- The multiplicity of an irreducible factor of a nonzero element is exactly the number of times
the normalized factor occurs in the `normalizedFactors`.

See also `count_normalizedFactors_eq` which expands the definition of `multiplicity`
to produce a specification for `count (normalizedFactors _) _`..
-/
theorem emultiplicity_eq_count_normalizedFactors [DecidableEq R] {a b : R} (ha : Irreducible a)
    (hb : b ≠ 0) : emultiplicity a b = (normalizedFactors b).count (normalize a) := by
  apply le_antisymm
  · apply Order.le_of_lt_add_one
    rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge, ge_iff_le,
      le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]
    simp
  rw [le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]

Extended Multiplicity Equals Count in Normalized Factorization

Informal description

Let $R$ be a unique factorization monoid with decidable equality. For any irreducible element $a \in R$ and any nonzero element $b \in R$, the extended multiplicity of $a$ in $b$ equals the count of the normalized form of $a$ in the multiset of normalized prime factors of $b$. In symbols: \[ \text{emultiplicity}(a, b) = \text{count}(\text{normalize}(a), \text{normalizedFactors}(b)). \]

UniqueFactorizationMonoid.count_normalizedFactors_eq theorem

 [DecidableEq R] {p x : R} (hp : Irreducible p) (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x)
  (hlt : ¬p ^ (n + 1) ∣ x) : (normalizedFactors x).count p = n

Full source

/-- The number of times an irreducible factor `p` appears in `normalizedFactors x` is defined by
the number of times it divides `x`.

See also `multiplicity_eq_count_normalizedFactors` if `n` is given by `multiplicity p x`.
-/
theorem count_normalizedFactors_eq [DecidableEq R] {p x : R} (hp : Irreducible p)
    (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) :
    (normalizedFactors x).count p = n := by classical
  by_cases hx0 : x = 0
  · simp [hx0] at hlt
  apply Nat.cast_injective (R := ℕ∞)
  convert (emultiplicity_eq_count_normalizedFactors hp hx0).symm
  · exact hnorm.symm
  exact (emultiplicity_eq_coe.mpr ⟨hle, hlt⟩).symm

Count of Irreducible Factor in Normalized Factorization Equals Multiplicity

Informal description

Let $R$ be a unique factorization monoid with decidable equality, and let $p, x \in R$ with $p$ irreducible and $\text{normalize}(p) = p$. For any natural number $n$, if $p^n$ divides $x$ but $p^{n+1}$ does not divide $x$, then the count of $p$ in the multiset of normalized factors of $x$ equals $n$. In symbols: \[ \text{count}(p, \text{normalizedFactors}(x)) = n. \]

UniqueFactorizationMonoid.count_normalizedFactors_eq' theorem

 [DecidableEq R] {p x : R} (hp : p = 0 ∨ Irreducible p) (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x)
  (hlt : ¬p ^ (n + 1) ∣ x) : (normalizedFactors x).count p = n

Full source

/-- The number of times an irreducible factor `p` appears in `normalizedFactors x` is defined by
the number of times it divides `x`. This is a slightly more general version of
`UniqueFactorizationMonoid.count_normalizedFactors_eq` that allows `p = 0`.

See also `multiplicity_eq_count_normalizedFactors` if `n` is given by `multiplicity p x`.
-/
theorem count_normalizedFactors_eq' [DecidableEq R] {p x : R} (hp : p = 0 ∨ Irreducible p)
    (hnorm : normalize p = p) {n : ℕ} (hle : p ^ n ∣ x) (hlt : ¬p ^ (n + 1) ∣ x) :
    (normalizedFactors x).count p = n := by
  rcases hp with (rfl | hp)
  · cases n
    · exact count_eq_zero.2 (zero_not_mem_normalizedFactors _)
    · rw [zero_pow (Nat.succ_ne_zero _)] at hle hlt
      exact absurd hle hlt
  · exact count_normalizedFactors_eq hp hnorm hle hlt

Count of (Possibly Zero) Irreducible Factor in Normalized Factorization Equals Multiplicity

Informal description

Let $R$ be a unique factorization monoid with decidable equality, and let $p, x \in R$ such that either $p = 0$ or $p$ is irreducible, and $\text{normalize}(p) = p$. For any natural number $n$, if $p^n$ divides $x$ but $p^{n+1}$ does not divide $x$, then the count of $p$ in the multiset of normalized factors of $x$ equals $n$. In symbols: \[ \text{count}(p, \text{normalizedFactors}(x)) = n. \]