Mathlib.FieldTheory.KummerPolynomial

root_X_pow_sub_C_pow theorem

(n : ℕ) (a : K) : (AdjoinRoot.root (X ^ n - C a)) ^ n = AdjoinRoot.of _ a

Full source

lemma root_X_pow_sub_C_pow (n : ℕ) (a : K) :
    (AdjoinRoot.root (X ^ n - C a)) ^ n = AdjoinRoot.of _ a := by
  rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]

Power of Adjoined Root Equals Constant Term: $(\text{root}(X^n - a))^n = a$

Informal description

For any natural number $n$ and any element $a$ in a field $K$, the $n$-th power of the adjoined root of the polynomial $X^n - a$ in the quotient ring $K[X]/(X^n - a)$ equals the image of $a$ under the canonical embedding of $K$ into the quotient ring. In other words, $(\text{root}(X^n - a))^n = a$ in $K[X]/(X^n - a)$.

root_X_pow_sub_C_ne_zero theorem

{n : ℕ} (hn : 1 < n) (a : K) : (AdjoinRoot.root (X ^ n - C a)) ≠ 0

Full source

lemma root_X_pow_sub_C_ne_zero {n : ℕ} (hn : 1 < n) (a : K) :
    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 :=
  mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.ne_zero_of_lt hn))
    X_ne_zero <| by rwa [natDegree_X_pow_sub_C, natDegree_X]

Nonzero Adjoined Root of $X^n - a$ for $n > 1$

Informal description

For any natural number $n > 1$ and any element $a$ in a field $K$, the adjoined root of the polynomial $X^n - a$ in the quotient ring $K[X]/(X^n - a)$ is nonzero, i.e., $\text{root}(X^n - a) \neq 0$.

root_X_pow_sub_C_ne_zero' theorem

{n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) : (AdjoinRoot.root (X ^ n - C a)) ≠ 0

Full source

lemma root_X_pow_sub_C_ne_zero' {n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) :
    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 := by
  obtain (rfl|hn) := (Nat.succ_le_iff.mpr hn).eq_or_lt
  · rw [pow_one]
    intro e
    refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_
    trans AdjoinRoot.mk (X - C a) (X - (X - C a))
    · rw [sub_sub_cancel]
    · rw [map_sub, mk_self, sub_zero, mk_X, e]
  · exact root_X_pow_sub_C_ne_zero hn a

Nonzero Adjoined Root of $X^n - a$ for $n > 0$ and $a \neq 0$

Informal description

For any natural number $n > 0$ and any nonzero element $a$ in a field $K$, the adjoined root of the polynomial $X^n - a$ in the quotient ring $K[X]/(X^n - a)$ is nonzero, i.e., $\text{root}(X^n - a) \neq 0$.

ne_zero_of_irreducible_X_pow_sub_C theorem

{n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) : n ≠ 0

Full source

lemma ne_zero_of_irreducible_X_pow_sub_C {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
    n ≠ 0 := by
  rintro rfl
  rw [pow_zero, ← C.map_one, ← map_sub] at H
  exact not_irreducible_C _ H

Nonzero Exponent Condition for Irreducibility of $X^n - a$

Informal description

For any natural number $n$ and any element $a$ in a field $K$, if the polynomial $X^n - a$ is irreducible over $K$, then $n$ is not zero.

ne_zero_of_irreducible_X_pow_sub_C' theorem

{n : ℕ} (hn : n ≠ 1) {a : K} (H : Irreducible (X ^ n - C a)) : a ≠ 0

Full source

lemma ne_zero_of_irreducible_X_pow_sub_C' {n : ℕ} (hn : n ≠ 1) {a : K}
    (H : Irreducible (X ^ n - C a)) : a ≠ 0 := by
  rintro rfl
  rw [map_zero, sub_zero] at H
  exact not_irreducible_pow hn H

Nonzero condition for irreducibility of $X^n - a$ when $n \neq 1$

Informal description

For any natural number $n \neq 1$ and any element $a$ in a field $K$, if the polynomial $X^n - a$ is irreducible over $K$, then $a \neq 0$.

root_X_pow_sub_C_eq_zero_iff theorem

{n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) : (AdjoinRoot.root (X ^ n - C a)) = 0 ↔ a = 0

Full source

lemma root_X_pow_sub_C_eq_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
    (AdjoinRoot.root (X ^ n - C a)) = 0 ↔ a = 0 := by
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
  rintro rfl
  have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
  rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]

Adjoined Root of $X^n - a$ is Zero if and only if $a$ is Zero

Informal description

For any natural number $n$ and any element $a$ in a field $K$, if the polynomial $X^n - a$ is irreducible over $K$, then the adjoined root of $X^n - a$ in the quotient ring $K[X]/(X^n - a)$ is zero if and only if $a$ is zero. In other words, $\text{root}(X^n - a) = 0 \leftrightarrow a = 0$.

root_X_pow_sub_C_ne_zero_iff theorem

{n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) : (AdjoinRoot.root (X ^ n - C a)) ≠ 0 ↔ a ≠ 0

Full source

lemma root_X_pow_sub_C_ne_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
    (AdjoinRoot.root (X ^ n - C a)) ≠ 0(AdjoinRoot.root (X ^ n - C a)) ≠ 0 ↔ a ≠ 0 :=
  (root_X_pow_sub_C_eq_zero_iff H).not

Nonzero Root of Irreducible $X^n - a$ if and only if $a$ is Nonzero

Informal description

For any natural number $n$ and any element $a$ in a field $K$, if the polynomial $X^n - a$ is irreducible over $K$, then the adjoined root of $X^n - a$ in the quotient ring $K[X]/(X^n - a)$ is nonzero if and only if $a$ is nonzero. In other words, $\text{root}(X^n - a) \neq 0 \leftrightarrow a \neq 0$.

pow_ne_of_irreducible_X_pow_sub_C theorem

{n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) {m : ℕ} (hm : m ∣ n) (hm' : m ≠ 1) (b : K) : b ^ m ≠ a

Full source

theorem pow_ne_of_irreducible_X_pow_sub_C {n : ℕ} {a : K}
    (H : Irreducible (X ^ n - C a)) {m : ℕ} (hm : m ∣ n) (hm' : m ≠ 1) (b : K) : b ^ m ≠ a := by
  have hn : n ≠ 0 := fun e ↦ not_irreducible_C
    (1 - a) (by simpa only [e, pow_zero, ← C.map_one, ← map_sub] using H)
  obtain ⟨k, rfl⟩ := hm
  rintro rfl
  obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m
  rw [mul_comm, pow_mul, map_pow, hq] at H
  have : degree q = 0 := by
    simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
      Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 rfl
  apply_fun degree at hq
  simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
    Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero,
    Nat.cast_injective.eq_iff] at hq
  exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)

Nonexistence of $m$-th Roots for Proper Divisors of $n$ in Irreducible $X^n - a$ Case

Informal description

Let $K$ be a field, $n$ a natural number, and $a \in K$ such that the polynomial $X^n - a$ is irreducible over $K$. For any natural number $m$ dividing $n$ with $m \neq 1$ and any $b \in K$, we have $b^m \neq a$.

X_pow_sub_C_irreducible_of_prime theorem

{p : ℕ} (hp : p.Prime) {a : K} (ha : ∀ b : K, b ^ p ≠ a) : Irreducible (X ^ p - C a)

Full source

/-- Let `p` be a prime number. Let `K` be a field.
Let `t ∈ K` be an element which does not have a `p`th root in `K`.
Then the polynomial `x ^ p - t` is irreducible over `K`. -/
@[stacks 09HF "We proved the result without the condition that `K` is char p in 09HF."]
theorem X_pow_sub_C_irreducible_of_prime {p : ℕ} (hp : p.Prime) {a : K} (ha : ∀ b : K, b ^ p ≠ a) :
    Irreducible (X ^ p - C a) := by
  -- First of all, We may find an irreducible factor `g` of `X ^ p - C a`.
  have : ¬ IsUnit (X ^ p - C a) := by
    rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
    exact hp.ne_zero
  have ⟨g, hg, hg'⟩ := WfDvdMonoid.exists_irreducible_factor this (X_pow_sub_C_ne_zero hp.pos a)
  -- It suffices to show that `deg g = p`.
  suffices natDegree g = p from (associated_of_dvd_of_natDegree_le hg'
    (X_pow_sub_C_ne_zero hp.pos a) (this.trans natDegree_X_pow_sub_C.symm).ge).irreducible hg
  -- Suppose `deg g ≠ p`.
  by_contra h
  have : Fact (Irreducible g) := ⟨hg⟩
  -- Let `r` be a root of `g`, then `N_K(r) ^ p = N_K(r ^ p) = N_K(a) = a ^ (deg g)`.
  have key : (Algebra.norm K (AdjoinRoot.root g)) ^ p = a ^ g.natDegree := by
    have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
    rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
    rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
  -- Since `a ^ (deg g)` is a `p`-power, and `p` is coprime to `deg g`, we conclude that `a` is
  -- also a `p`-power, contradicting the hypothesis
  have : p.Coprime (natDegree g) := hp.coprime_iff_not_dvd.mpr (fun e ↦ h (((natDegree_le_of_dvd hg'
    (X_pow_sub_C_ne_zero hp.pos a)).trans_eq natDegree_X_pow_sub_C).antisymm (Nat.le_of_dvd
      (natDegree_pos_iff_degree_pos.mpr <| Polynomial.degree_pos_of_irreducible hg) e)))
  exact ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec

Irreducibility of $X^p - a$ for non-$p$-th powers in a field

Informal description

Let $K$ be a field and $p$ a prime number. For any element $a \in K$ that is not a $p$-th power in $K$ (i.e., there exists no $b \in K$ such that $b^p = a$), the polynomial $X^p - a$ is irreducible over $K$.

X_pow_sub_C_irreducible_iff_of_prime theorem

{p : ℕ} (hp : p.Prime) {a : K} : Irreducible (X ^ p - C a) ↔ ∀ b, b ^ p ≠ a

Full source

theorem X_pow_sub_C_irreducible_iff_of_prime {p : ℕ} (hp : p.Prime) {a : K} :
    IrreducibleIrreducible (X ^ p - C a) ↔ ∀ b, b ^ p ≠ a :=
  ⟨(pow_ne_of_irreducible_X_pow_sub_C · dvd_rfl hp.ne_one), X_pow_sub_C_irreducible_of_prime hp⟩

Irreducibility of $X^p - a$ for Prime $p$: $X^p - a$ is irreducible iff $a$ is not a $p$-th power

Informal description

Let $K$ be a field and $p$ a prime number. For any element $a \in K$, the polynomial $X^p - a$ is irreducible over $K$ if and only if $a$ is not a $p$-th power in $K$ (i.e., there exists no $b \in K$ such that $b^p = a$).

Main result