doc-next-gen

Mathlib.Algebra.Prime.Lemmas

Module docstring

{"# Associated, prime, and irreducible elements.

In this file we define the predicate Prime p saying that an element of a commutative monoid with zero is prime. Namely, Prime p means that p isn't zero, it isn't a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b;

In decomposition monoids (e.g., ℕ, ℤ), this predicate is equivalent to Irreducible, however this is not true in general.

We also define an equivalence relation Associated saying that two elements of a monoid differ by a multiplication by a unit. Then we show that the quotient type Associates is a monoid and prove basic properties of this quotient. "}

comap_prime theorem
(hinv : ∀ a, g (f a : N) = a) (hp : Prime (f p)) : Prime p
Full source 
theorem comap_prime (hinv : ∀ a, g (f a : N) = a) (hp : Prime (f p)) : Prime p :=
  ⟨fun h => hp.1 <| by simp [h], fun h => hp.2.1 <| h.map f, fun a b h => by
    refine
        (hp.2.2 (f a) (f b) <| by
              convert map_dvd f h
              simp).imp
          ?_ ?_ <;>
      · intro h
        convert ← map_dvd g h <;> apply hinv⟩
Prime Element Preservation Under Homomorphism with Left Inverse
Informal description
Let $M$ and $N$ be commutative monoids with zero, and let $f \colon M \to N$ and $g \colon N \to M$ be homomorphisms such that $g \circ f = \text{id}_M$. If $f(p) \in N$ is a prime element, then $p \in M$ is also a prime element.
MulEquiv.prime_iff theorem
{E : Type*} [EquivLike E M N] [MulEquivClass E M N] (e : E) : Prime (e p) ↔ Prime p
Full source 
theorem MulEquiv.prime_iff {E : Type*} [EquivLike E M N] [MulEquivClass E M N] (e : E) :
    PrimePrime (e p) ↔ Prime p := by
  let e := MulEquivClass.toMulEquiv e
  exact ⟨comap_prime e e.symm fun a => by simp,
    fun h => (comap_prime e.symm e fun a => by simp) <| (e.symm_apply_apply p).substr h⟩
Prime Element Preservation Under Multiplicative Equivalence: $p$ prime $\iff$ $e(p)$ prime
Informal description
Let $M$ and $N$ be commutative monoids with zero, and let $E$ be a type of multiplicative equivalences between $M$ and $N$. For any multiplicative equivalence $e \in E$, an element $p \in M$ is prime if and only if its image $e(p) \in N$ is prime.
Prime.left_dvd_or_dvd_right_of_dvd_mul theorem
[CancelCommMonoidWithZero M] {p : M} (hp : Prime p) {a b : M} : a ∣ p * b → p ∣ a ∨ a ∣ b
Full source 
theorem Prime.left_dvd_or_dvd_right_of_dvd_mul [CancelCommMonoidWithZero M] {p : M} (hp : Prime p)
    {a b : M} : a ∣ p * b → p ∣ ap ∣ a ∨ a ∣ b := by
  rintro ⟨c, hc⟩
  rcases hp.2.2 a c (hc ▸ dvd_mul_right _ _) with (h | ⟨x, rfl⟩)
  · exact Or.inl h
  · rw [mul_left_comm, mul_right_inj' hp.ne_zero] at hc
    exact Or.inr (hc.symm ▸ dvd_mul_right _ _)
Prime Element Divisibility Property: $a \mid p \cdot b \Rightarrow p \mid a \lor a \mid b$
Informal description
Let $M$ be a cancellative commutative monoid with zero, and let $p \in M$ be a prime element. For any elements $a, b \in M$, if $a$ divides $p \cdot b$, then either $p$ divides $a$ or $a$ divides $b$.
Prime.pow_dvd_of_dvd_mul_left theorem
[CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p) (n : ℕ) (h : ¬p ∣ a) (h' : p ^ n ∣ a * b) : p ^ n ∣ b
Full source 
theorem Prime.pow_dvd_of_dvd_mul_left [CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p)
    (n : ℕ) (h : ¬p ∣ a) (h' : p ^ n ∣ a * b) : p ^ n ∣ b := by
  induction n with
  | zero =>
    rw [pow_zero]
    exact one_dvd b
  | succ n ih =>
    obtain ⟨c, rfl⟩ := ih (dvd_trans (pow_dvd_pow p n.le_succ) h')
    rw [pow_succ]
    apply mul_dvd_mul_left _ ((hp.dvd_or_dvd _).resolve_left h)
    rwa [← mul_dvd_mul_iff_left (pow_ne_zero n hp.ne_zero), ← pow_succ, mul_left_comm]
Prime Power Divisibility Property: $p^n \mid a \cdot b \Rightarrow p^n \mid b$ when $p \nmid a$
Informal description
Let $M$ be a cancellative commutative monoid with zero, and let $p \in M$ be a prime element. For any natural number $n$ and elements $a, b \in M$, if $p$ does not divide $a$ and $p^n$ divides $a \cdot b$, then $p^n$ divides $b$.
Prime.pow_dvd_of_dvd_mul_right theorem
[CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p) (n : ℕ) (h : ¬p ∣ b) (h' : p ^ n ∣ a * b) : p ^ n ∣ a
Full source 
theorem Prime.pow_dvd_of_dvd_mul_right [CancelCommMonoidWithZero M] {p a b : M} (hp : Prime p)
    (n : ℕ) (h : ¬p ∣ b) (h' : p ^ n ∣ a * b) : p ^ n ∣ a := by
  rw [mul_comm] at h'
  exact hp.pow_dvd_of_dvd_mul_left n h h'
Prime Power Divisibility Property: $p^n \mid a \cdot b \Rightarrow p^n \mid a$ when $p \nmid b$
Informal description
Let $M$ be a cancellative commutative monoid with zero, and let $p \in M$ be a prime element. For any natural number $n$ and elements $a, b \in M$, if $p$ does not divide $b$ and $p^n$ divides $a \cdot b$, then $p^n$ divides $a$.
Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd theorem
[CancelCommMonoidWithZero M] {p a b : M} {n : ℕ} (hp : Prime p) (hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 ∣ b) : p ∣ a
Full source 
theorem Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd [CancelCommMonoidWithZero M] {p a b : M}
    {n : ℕ} (hp : Prime p) (hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n) (hb : ¬p ^ 2 ∣ b) : p ∣ a := by
  -- Suppose `p ∣ b`, write `b = p * x` and `hy : a ^ n.succ * b ^ n = p ^ n.succ * y`.
  rcases hp.dvd_or_dvd ((dvd_pow_self p (Nat.succ_ne_zero n)).trans hpow) with H | hbdiv
  · exact hp.dvd_of_dvd_pow H
  obtain ⟨x, rfl⟩ := hp.dvd_of_dvd_pow hbdiv
  obtain ⟨y, hy⟩ := hpow
  -- Then we can divide out a common factor of `p ^ n` from the equation `hy`.
  have : a ^ n.succ * x ^ n = p * y := by
    refine mul_left_cancel₀ (pow_ne_zero n hp.ne_zero) ?_
    rw [← mul_assoc _ p, ← pow_succ, ← hy, mul_pow, ← mul_assoc (a ^ n.succ), mul_comm _ (p ^ n),
      mul_assoc]
  -- So `p ∣ a` (and we're done) or `p ∣ x`, which can't be the case since it implies `p^2 ∣ b`.
  refine hp.dvd_of_dvd_pow ((hp.dvd_or_dvd ⟨_, this⟩).resolve_right fun hdvdx => hb ?_)
  obtain ⟨z, rfl⟩ := hp.dvd_of_dvd_pow hdvdx
  rw [pow_two, ← mul_assoc]
  exact dvd_mul_right _ _
Prime Divisibility from Power Divisibility: $p^{n+1} \mid a^{n+1}b^n \Rightarrow p \mid a$ when $p^2 \nmid b$
Informal description
Let $M$ be a cancellative commutative monoid with zero, and let $p \in M$ be a prime element. For any elements $a, b \in M$ and natural number $n$, if $p^{n+1}$ divides $a^{n+1} \cdot b^n$ and $p^2$ does not divide $b$, then $p$ divides $a$.
prime_pow_succ_dvd_mul theorem
{M : Type*} [CancelCommMonoidWithZero M] {p x y : M} (h : Prime p) {i : ℕ} (hxy : p ^ (i + 1) ∣ x * y) : p ^ (i + 1) ∣ x ∨ p ∣ y
Full source 
theorem prime_pow_succ_dvd_mul {M : Type*} [CancelCommMonoidWithZero M] {p x y : M} (h : Prime p)
    {i : ℕ} (hxy : p ^ (i + 1) ∣ x * y) : p ^ (i + 1) ∣ xp ^ (i + 1) ∣ x ∨ p ∣ y := by
  rw [or_iff_not_imp_right]
  intro hy
  induction i generalizing x with
  | zero => rw [pow_one] at hxy ⊢; exact (h.dvd_or_dvd hxy).resolve_right hy
  | succ i ih =>
    rw [pow_succ'] at hxy ⊢
    obtain ⟨x', rfl⟩ := (h.dvd_or_dvd (dvd_of_mul_right_dvd hxy)).resolve_right hy
    rw [mul_assoc] at hxy
    exact mul_dvd_mul_left p (ih ((mul_dvd_mul_iff_left h.ne_zero).mp hxy))
Prime Power Divisibility in Cancellative Monoids: $p^{i+1} \mid x \cdot y \Rightarrow p^{i+1} \mid x \lor p \mid y$
Informal description
Let $M$ be a cancellative commutative monoid with zero, and let $p \in M$ be a prime element. For any elements $x, y \in M$ and natural number $i$, if $p^{i+1}$ divides the product $x \cdot y$, then either $p^{i+1}$ divides $x$ or $p$ divides $y$.
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul theorem
(hp : Prime p) {a b : M} {k l : ℕ} : p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b
Full source 
theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul (hp : Prime p) {a b : M} {k l : ℕ} :
    p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ ap ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b :=
  fun ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩ =>
  have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z) := by
    simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz
  have hp0 : p ^ (k + l) ≠ 0 := pow_ne_zero _ hp.ne_zero
  have hpd : p ∣ x * y := ⟨z, by rwa [mul_right_inj' hp0] at h⟩
  (hp.dvd_or_dvd hpd).elim
    (fun ⟨d, hd⟩ => Or.inl ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
    fun ⟨d, hd⟩ => Or.inr ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩
Prime Power Divisibility Property: $p^{k+l+1} \mid a \cdot b \Rightarrow p^{k+1} \mid a \lor p^{l+1} \mid b$
Informal description
Let $p$ be a prime element in a cancellative commutative monoid with zero $M$. For any elements $a, b \in M$ and natural numbers $k, l$, if $p^k$ divides $a$, $p^l$ divides $b$, and $p^{k+l+1}$ divides $a \cdot b$, then either $p^{k+1}$ divides $a$ or $p^{l+1}$ divides $b$.
Prime.not_isSquare theorem
(hp : Prime p) : ¬IsSquare p
Full source 
theorem Prime.not_isSquare (hp : Prime p) : ¬IsSquare p :=
  hp.irreducible.not_isSquare
Prime Elements Are Not Squares
Informal description
If an element $p$ in a cancelative commutative monoid with zero is prime, then $p$ is not a square, i.e., there does not exist an element $r$ such that $p = r \cdot r$.
IsSquare.not_prime theorem
(ha : IsSquare a) : ¬Prime a
Full source 
theorem IsSquare.not_prime (ha : IsSquare a) : ¬Prime a := fun h => h.not_isSquare ha
Square elements are not prime
Informal description
If an element $a$ in a cancelative commutative monoid with zero is a square (i.e., there exists an element $r$ such that $a = r \cdot r$), then $a$ is not a prime element.
not_prime_pow theorem
{n : ℕ} (hn : n ≠ 1) : ¬Prime (a ^ n)
Full source 
theorem not_prime_pow {n : ℕ} (hn : n ≠ 1) : ¬Prime (a ^ n) := fun hp =>
  not_irreducible_pow hn hp.irreducible
Powers with exponent not equal to one are not prime
Informal description
For any natural number $n \neq 1$, the element $a^n$ is not prime in a cancelative commutative monoid with zero.
DvdNotUnit.isUnit_of_irreducible_right theorem
[CommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) (hq : Irreducible q) : IsUnit p
Full source 
theorem DvdNotUnit.isUnit_of_irreducible_right [CommMonoidWithZero M] {p q : M}
    (h : DvdNotUnit p q) (hq : Irreducible q) : IsUnit p := by
  obtain ⟨_, x, hx, hx'⟩ := h
  exact ((irreducible_iff.1 hq).right hx').resolve_right hx
Strict Divisor of Irreducible Element is Unit in Commutative Monoid with Zero
Informal description
Let $M$ be a commutative monoid with zero. For any elements $p, q \in M$, if $p$ strictly divides $q$ (i.e., $p \neq 0$ and $q = p \cdot x$ for some non-unit $x$) and $q$ is irreducible, then $p$ must be a unit.
not_irreducible_of_not_unit_dvdNotUnit theorem
[CommMonoidWithZero M] {p q : M} (hp : ¬IsUnit p) (h : DvdNotUnit p q) : ¬Irreducible q
Full source 
theorem not_irreducible_of_not_unit_dvdNotUnit [CommMonoidWithZero M] {p q : M} (hp : ¬IsUnit p)
    (h : DvdNotUnit p q) : ¬Irreducible q :=
  mt h.isUnit_of_irreducible_right hp
Non-unit strict divisor implies reducibility in commutative monoid with zero
Informal description
Let $M$ be a commutative monoid with zero. For any elements $p, q \in M$, if $p$ is not a unit and $p$ strictly divides $q$ (i.e., $p \neq 0$ and $q = p \cdot x$ for some non-unit $x$), then $q$ is not irreducible.
DvdNotUnit.not_unit theorem
[CommMonoidWithZero M] {p q : M} (hp : DvdNotUnit p q) : ¬IsUnit q
Full source 
theorem DvdNotUnit.not_unit [CommMonoidWithZero M] {p q : M} (hp : DvdNotUnit p q) : ¬IsUnit q := by
  obtain ⟨-, x, hx, rfl⟩ := hp
  exact fun hc => hx (isUnit_iff_dvd_one.mpr (dvd_of_mul_left_dvd (isUnit_iff_dvd_one.mp hc)))
Non-unit Property of Strictly Divided Elements in Commutative Monoid with Zero
Informal description
Let $M$ be a commutative monoid with zero. For any elements $p, q \in M$, if $p$ strictly divides $q$ (i.e., $p \neq 0$ and there exists a non-unit $x$ such that $q = p \cdot x$), then $q$ is not a unit.
DvdNotUnit.ne theorem
[CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) : p ≠ q
Full source 
theorem DvdNotUnit.ne [CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) : p ≠ q := by
  by_contra hcontra
  obtain ⟨hp, x, hx', hx''⟩ := h
  conv_lhs at hx'' => rw [← hcontra, ← mul_one p]
  rw [(mul_left_cancel₀ hp hx'').symm] at hx'
  exact hx' isUnit_one
Non-Equality of Strict Divisor and Dividend in Cancelative Commutative Monoid with Zero
Informal description
Let $M$ be a cancelative commutative monoid with zero. For any elements $p, q \in M$ such that $p$ strictly divides $q$ (i.e., $p \neq 0$ and there exists a non-unit $x$ with $q = p \cdot x$), we have $p \neq q$.
pow_injective_of_not_isUnit theorem
[CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q ≠ 0) : Function.Injective fun n : ℕ => q ^ n
Full source 
theorem pow_injective_of_not_isUnit [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q)
    (hq' : q ≠ 0) : Function.Injective fun n : ℕ => q ^ n := by
  refine injective_of_lt_imp_ne fun n m h => DvdNotUnit.ne ⟨pow_ne_zero n hq', q ^ (m - n), ?_, ?_⟩
  · exact not_isUnit_of_not_isUnit_dvd hq (dvd_pow (dvd_refl _) (Nat.sub_pos_of_lt h).ne')
  · exact (pow_mul_pow_sub q h.le).symm
Injectivity of Powers for Non-Units in Cancellative Commutative Monoids with Zero
Informal description
Let $M$ be a cancellative commutative monoid with zero. For any element $q \in M$ that is neither a unit nor zero, the function $n \mapsto q^n$ is injective on the natural numbers $\mathbb{N}$.
pow_inj_of_not_isUnit theorem
[CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q) (hq' : q ≠ 0) {m n : ℕ} : q ^ m = q ^ n ↔ m = n
Full source 
theorem pow_inj_of_not_isUnit [CancelCommMonoidWithZero M] {q : M} (hq : ¬IsUnit q)
    (hq' : q ≠ 0) {m n : ℕ} : q ^ m = q ^ n ↔ m = n :=
  (pow_injective_of_not_isUnit hq hq').eq_iff
Equality of Powers for Non-Units in Cancellative Commutative Monoids with Zero
Informal description
Let $M$ be a cancellative commutative monoid with zero. For any element $q \in M$ that is neither a unit nor zero, and for any natural numbers $m, n \in \mathbb{N}$, we have $q^m = q^n$ if and only if $m = n$.