Mathlib.RingTheory.UniqueFactorizationDomain.Defs

WfDvdMonoid abbrev

(α : Type*) [CommMonoidWithZero α] : Prop

Full source

/-- 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.
-/
abbrev WfDvdMonoid (α : Type*) [CommMonoidWithZero α] : Prop :=
  IsWellFounded α DvdNotUnit

Definition of Well-Founded Divisibility Monoid

Informal description

A commutative monoid with zero $\alpha$ is called a *well-founded divisibility monoid* if the strict divisibility relation (defined by $a \prec b$ when $a$ properly divides $b$) is well-founded. This condition is equivalent to the descending chain condition on divisibility and to the ascending chain condition on principal ideals in an integral domain.

wellFounded_dvdNotUnit theorem

{α : Type*} [CommMonoidWithZero α] [h : WfDvdMonoid α] : WellFounded (DvdNotUnit (α := α))

Full source

theorem wellFounded_dvdNotUnit {α : Type*} [CommMonoidWithZero α] [h : WfDvdMonoid α] :
    WellFounded (DvdNotUnit (α := α)) :=
  h.wf

Well-Foundedness of Proper Divisibility in Well-Founded Divisibility Monoids

Informal description

For any commutative monoid with zero $\alpha$ that is a well-founded divisibility monoid, the relation "properly divides" (denoted by $\prec$) is well-founded. That is, there are no infinite descending chains with respect to the relation $a \prec b$ defined by $a$ properly dividing $b$.

WfDvdMonoid.exists_irreducible_factor theorem

{a : α} (ha : ¬IsUnit a) (ha0 : a ≠ 0) : ∃ i, Irreducible i ∧ i ∣ a

Full source

theorem exists_irreducible_factor {a : α} (ha : ¬IsUnit a) (ha0 : a ≠ 0) :
    ∃ i, Irreducible i ∧ i ∣ a :=
  let ⟨b, hs, hr⟩ := wellFounded_dvdNotUnit.has_min { b | b ∣ a ∧ ¬IsUnit b } ⟨a, dvd_rfl, ha⟩
  ⟨b,
    ⟨hs.2, fun c d he =>
      let h := dvd_trans ⟨d, he⟩ hs.1
      or_iff_not_imp_left.2 fun hc =>
        of_not_not fun hd => hr c ⟨h, hc⟩ ⟨ne_zero_of_dvd_ne_zero ha0 h, d, hd, he⟩⟩,
    hs.1⟩

Existence of Irreducible Factors in Well-Founded Divisibility Monoids

Informal description

For any nonzero element $a$ in a well-founded divisibility monoid $\alpha$ that is not a unit, there exists an irreducible element $i$ in $\alpha$ such that $i$ divides $a$.

WfDvdMonoid.induction_on_irreducible theorem

 {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

Full source

@[elab_as_elim]
theorem induction_on_irreducible {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 :=
  haveI := Classical.dec
  wellFounded_dvdNotUnit.fix
    (fun a ih =>
      if ha0 : a = 0 then ha0.substr zero
      else
        if hau : IsUnit a then unit a hau
        else
          let ⟨i, i_irred, b, hb⟩ := exists_irreducible_factor hau ha0
          let hb0 : b ≠ 0 := ne_zero_of_dvd_ne_zero ha0 ⟨i, mul_comm i b ▸ hb⟩
          hb.symm ▸ mul b i hb0 i_irred <| ih b ⟨hb0, i, i_irred.1, mul_comm i b ▸ hb⟩)
    a

Induction Principle for Irreducible Elements in Well-Founded Divisibility Monoids

Informal description

Let $\alpha$ be a well-founded divisibility monoid. For any predicate $\text{motive} : \alpha \to \text{Prop}$, any element $a \in \alpha$, and the following hypotheses: 1. $\text{motive}(0)$ holds, 2. For any unit $u \in \alpha$, $\text{motive}(u)$ holds, 3. For any nonzero $a \in \alpha$ and irreducible $i \in \alpha$, if $\text{motive}(a)$ holds then $\text{motive}(i \cdot a)$ holds, it follows that $\text{motive}(a)$ holds for all $a \in \alpha$.

WfDvdMonoid.exists_factors theorem

(a : α) : a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a

Full source

theorem exists_factors (a : α) :
    a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a :=
  induction_on_irreducible a (fun h => (h rfl).elim)
    (fun _ hu _ => ⟨0, fun _ h => False.elim (Multiset.not_mem_zero _ h), hu.unit, one_mul _⟩)
    fun a i ha0 hi ih _ =>
    let ⟨s, hs⟩ := ih ha0
    ⟨i ::ₘ s, fun b H => (Multiset.mem_cons.1 H).elim (fun h => h.symm ▸ hi) (hs.1 b), by
      rw [s.prod_cons i]
      exact hs.2.mul_left i⟩

Existence of Irreducible Factorization in Well-Founded Divisibility Monoids

Informal description

For any nonzero element $a$ in a well-founded divisibility monoid $\alpha$, there exists a multiset $f$ of irreducible elements such that every element $b \in f$ is irreducible, and the product of the elements in $f$ is associated with $a$ (i.e., they differ by a unit factor).

WfDvdMonoid.not_unit_iff_exists_factors_eq theorem

 (a : α) (hn0 : a ≠ 0) : ¬IsUnit a ↔ ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅

Full source

theorem not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) :
    ¬IsUnit a¬IsUnit a ↔ ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅ :=
  ⟨fun hnu => by
    obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0
    obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]
    classical
      refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
      · obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
      · rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm],
    fun ⟨_, hi, he, hne⟩ =>
    let ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero hne
    not_isUnit_of_not_isUnit_dvd (hi b h).not_isUnit <| he ▸ Multiset.dvd_prod h⟩

Characterization of Non-Units via Irreducible Factorization in Well-Founded Divisibility Monoids

Informal description

For any nonzero element $a$ in a well-founded divisibility monoid $\alpha$, $a$ is not a unit if and only if there exists a nonempty multiset $f$ of irreducible elements such that every element $b \in f$ is irreducible and the product of the elements in $f$ equals $a$.

WfDvdMonoid.isRelPrime_of_no_irreducible_factors theorem

{x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z : α, Irreducible z → z ∣ x → ¬z ∣ y) : IsRelPrime x y

Full source

theorem isRelPrime_of_no_irreducible_factors {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z : α, Irreducible z → z ∣ x → ¬z ∣ y) : IsRelPrime x y :=
  isRelPrime_of_no_nonunits_factors nonzero fun _z znu znz zx zy ↦
    have ⟨i, h1, h2⟩ := exists_irreducible_factor znu znz
    H i h1 (h2.trans zx) (h2.trans zy)

Relatively Prime Elements in Well-Founded Divisibility Monoids via Irreducible Factors

Informal description

Let $x$ and $y$ be elements of a well-founded divisibility monoid $\alpha$ such that they are not both zero. If for every irreducible element $z$ in $\alpha$, $z$ divides $x$ implies that $z$ does not divide $y$, then $x$ and $y$ are relatively prime (i.e., $\text{IsRelPrime}(x, y)$ holds).

UniqueFactorizationMonoid structure

(α : Type*) [CancelCommMonoidWithZero α] : Prop
    extends IsWellFounded α DvdNotUnit

Full source

/--
Unique factorization monoids are defined as `CancelCommMonoidWithZero`s 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`
-/
class UniqueFactorizationMonoid (α : Type*) [CancelCommMonoidWithZero α] : Prop
    extends IsWellFounded α DvdNotUnit where
  protected irreducible_iff_prime : ∀ {a : α}, IrreducibleIrreducible a ↔ Prime a

Unique Factorization Monoid

Informal description

A unique factorization monoid is a commutative monoid with zero and cancellation (i.e., a `CancelCommMonoidWithZero`) where the strict divisibility relation is well-founded, and every irreducible element is prime. Equivalently, every nonzero element can be expressed as a multiset of irreducible factors (unique up to associated elements) or as a multiset of prime factors (not necessarily unique).

ufm_of_decomposition_of_wfDvdMonoid instance

[CancelCommMonoidWithZero α] [WfDvdMonoid α] [DecompositionMonoid α] : UniqueFactorizationMonoid α

Full source

instance (priority := 100) ufm_of_decomposition_of_wfDvdMonoid
    [CancelCommMonoidWithZero α] [WfDvdMonoid α] [DecompositionMonoid α] :
    UniqueFactorizationMonoid α :=
  { ‹WfDvdMonoid α› with irreducible_iff_prime := irreducible_iff_prime }

Decomposition Monoids with Well-Founded Divisibility are Unique Factorization Monoids

Informal description

Every decomposition monoid that is a well-founded divisibility monoid and a commutative monoid with zero and cancellation is a unique factorization monoid.

UniqueFactorizationMonoid.exists_prime_factors theorem

(a : α) : a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Full source

theorem exists_prime_factors (a : α) :
    a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a := by
  simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]
  apply WfDvdMonoid.exists_factors a

Existence of Prime Factorization in Unique Factorization Monoids

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$, there exists a multiset $f$ of prime elements such that every element $b \in f$ is prime, and the product of the elements in $f$ is associated with $a$ (i.e., they differ by a unit factor).

UniqueFactorizationMonoid.exists_prime_iff theorem

: (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬IsUnit x

Full source

lemma exists_prime_iff :
    (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬ IsUnit x := by
  refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩
  obtain ⟨f, hf, -⟩ := WfDvdMonoid.exists_irreducible_factor hxu hx₀
  exact ⟨f, UniqueFactorizationMonoid.irreducible_iff_prime.mp hf⟩

Existence of Prime Elements in Unique Factorization Monoids

Informal description

In a unique factorization monoid $\alpha$, there exists a prime element if and only if there exists a nonzero, non-unit element. That is, $(\exists p \in \alpha, \text{Prime}(p)) \leftrightarrow (\exists x \in \alpha, x \neq 0 \land \neg \text{IsUnit}(x))$.

UniqueFactorizationMonoid.induction_on_prime theorem

 {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

Full source

@[elab_as_elim]
theorem induction_on_prime {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 := by
  simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime] at h₃
  exact WfDvdMonoid.induction_on_irreducible a h₁ h₂ h₃

Induction Principle for Prime Elements in Unique Factorization Monoids

Informal description

Let $\alpha$ be a unique factorization monoid and $P : \alpha \to \text{Prop}$ a predicate. For any element $a \in \alpha$, if: 1. $P(0)$ holds, 2. $P(x)$ holds for every unit $x \in \alpha$, 3. For any nonzero $a \in \alpha$ and prime $p \in \alpha$, if $P(a)$ holds then $P(p \cdot a)$ holds, then $P(a)$ holds for all $a \in \alpha$.

UniqueFactorizationMonoid.instDecompositionMonoid instance

: DecompositionMonoid α

Full source

instance : DecompositionMonoid α where
  primal a := by
    obtain rfl | ha := eq_or_ne a 0; · exact isPrimal_zero
    obtain ⟨f, hf, u, rfl⟩ := exists_prime_factors a ha
    exact ((Submonoid.isPrimal α).multiset_prod_mem f (hf · ·|>.isPrimal)).mul u.isUnit.isPrimal

Unique Factorization Monoids are Decomposition Monoids

Informal description

Every unique factorization monoid $\alpha$ is a decomposition monoid, meaning that every nonzero element can be factored into a product of irreducible elements (unique up to order and units).

UniqueFactorizationMonoid.factors definition

(a : α) : Multiset α

Full source

/-- Noncomputably determines the multiset of prime factors. -/
noncomputable def factors (a : α) : Multiset α :=
  if h : a = 0 then 0 else Classical.choose (UniqueFactorizationMonoid.exists_prime_factors a h)

Prime factorization multiset of an element in a unique factorization monoid

Informal description

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

UniqueFactorizationMonoid.factors_prod theorem

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

Full source

theorem factors_prod {a : α} (ane0 : a ≠ 0) : Associated (factors a).prod a := by
  rw [factors, dif_neg ane0]
  exact (Classical.choose_spec (exists_prime_factors a ane0)).2

Product of Prime Factors is Associated to Original Element in Unique Factorization Monoid

Informal description

For any nonzero element $a$ in a unique factorization monoid $\alpha$, the product of the prime factors in the multiset $\text{factors}(a)$ is associated with $a$ (i.e., they differ by a unit factor).

UniqueFactorizationMonoid.factors_zero theorem

: factors (0 : α) = 0

Full source

@[simp]
theorem factors_zero : factors (0 : α) = 0 := by simp [factors]

Prime Factorization of Zero is Empty

Informal description

For any unique factorization monoid $\alpha$, the multiset of prime factors of the zero element is the empty multiset, i.e., $\text{factors}(0) = 0$.

UniqueFactorizationMonoid.ne_zero_of_mem_factors theorem

{p a : α} (h : p ∈ factors a) : a ≠ 0

Full source

theorem ne_zero_of_mem_factors {p a : α} (h : p ∈ factors a) : a ≠ 0 := by
  rintro rfl
  simp at h

Nonzero Element Has Prime Factors

Informal description

For any elements $p$ and $a$ in a unique factorization monoid $\alpha$, if $p$ is a member of the multiset of prime factors of $a$ (i.e., $p \in \text{factors}(a)$), then $a$ is nonzero, i.e., $a \neq 0$.

UniqueFactorizationMonoid.dvd_of_mem_factors theorem

{p a : α} (h : p ∈ factors a) : p ∣ a

Full source

theorem dvd_of_mem_factors {p a : α} (h : p ∈ factors a) : p ∣ a :=
  dvd_trans (Multiset.dvd_prod h) (Associated.dvd (factors_prod (ne_zero_of_mem_factors h)))

Prime Factor Divides Element in Unique Factorization Monoid

Informal description

For any elements $p$ and $a$ in a unique factorization monoid $\alpha$, if $p$ is a prime factor of $a$ (i.e., $p \in \text{factors}(a)$), then $p$ divides $a$ (i.e., $p \mid a$).

UniqueFactorizationMonoid.prime_of_factor theorem

{a : α} (x : α) (hx : x ∈ factors a) : Prime x

Full source

theorem prime_of_factor {a : α} (x : α) (hx : x ∈ factors a) : Prime x := by
  have ane0 := ne_zero_of_mem_factors hx
  rw [factors, dif_neg ane0] at hx
  exact (Classical.choose_spec (UniqueFactorizationMonoid.exists_prime_factors a ane0)).1 x hx

Elements in Prime Factorization are Prime

Informal description

For any element $a$ in a unique factorization monoid $\alpha$ and any element $x$ in the multiset of prime factors of $a$ (i.e., $x \in \text{factors}(a)$), the element $x$ is prime.

UniqueFactorizationMonoid.irreducible_of_factor theorem

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

Full source

theorem irreducible_of_factor {a : α} : ∀ x : α, x ∈ factors a → Irreducible x := fun x h =>
  (prime_of_factor x h).irreducible

Irreducibility of Prime Factors in a Unique Factorization Monoid

Informal description

For any element $a$ in a unique factorization monoid $\alpha$, every element $x$ in the multiset of prime factors of $a$ (i.e., $x \in \text{factors}(a)$) is irreducible.

Main Definitions