Separable contraction of irreducible polynomials

TheoremIrreducible polynomials are expansions of separable irreducibles#✓fully proved

Let \(K\) be a field of characteristic \(p\) (with \(p = 0\) in characteristic zero) and let \(f \in K[x]\) be irreducible. Then there exist \(n \in \mathbb{N}\) and an irreducible separable polynomial \(g \in K[x]\) such that \(f(x) = g(x^{p^n})\), where \(0^0 = 1\).

theorem exists_irreducible_separable_expand_eq {f : K[X]}
    (hf : Irreducible f) :
    ∃ (n : ℕ) (g : K[X]),
      Irreducible g ∧ g.Separable ∧
        expand K ((ringChar K) ^ n) g = f

Sources

• ATLAS NumberTheoryI, Corollary 4.5 (existence).

Used by 1

Used byIrreducible polynomials are uniquely expansions of separable irreducibles

TheoremThe separable irreducible underlying an irreducible polynomial is unique#✓fully proved

Let \(K\) be a field of characteristic \(p\) (with \(p = 0\) in characteristic zero) and let \(f \in K[x]\) be irreducible. If \(n_1, n_2 \in \mathbb{N}\) and irreducible separable polynomials \(g_1, g_2 \in K[x]\) satisfy \(f(x) = g_1(x^{p^{n_1}})\) and \(f(x) = g_2(x^{p^{n_2}})\), where \(0^0 = 1\), then \(n_1 = n_2\) and \(g_1 = g_2\).

theorem unique_irreducible_separable_expand_eq {f : K[X]}
    (hf : Irreducible f) {n₁ n₂ : ℕ} {g₁ g₂ : K[X]}
    (h₁ : Irreducible g₁ ∧ g₁.Separable ∧
      expand K ((ringChar K) ^ n₁) g₁ = f)
    (h₂ : Irreducible g₂ ∧ g₂.Separable ∧
      expand K ((ringChar K) ^ n₂) g₂ = f) :
    n₁ = n₂ ∧ g₁ = g₂

Sources

• ATLAS NumberTheoryI, Corollary 4.5 (uniqueness).

Used by 1

Used byIrreducible polynomials are uniquely expansions of separable irreducibles

TheoremIrreducible polynomials are uniquely expansions of separable irreducibles#✓fully proved

Let \(K\) be a field of characteristic \(p\) (with \(p = 0\) in characteristic zero, and \(0^0 = 1\)) and let \(f \in K[x]\) be irreducible. Then there exist \(n \in \mathbb{N}\) and an irreducible separable polynomial \(g \in K[x]\) with \(f(x) = g(x^{p^n})\), and for every \(n' \in \mathbb{N}\) and every irreducible separable polynomial \(g' \in K[x]\) with \(f(x) = g'(x^{p^{n'}})\) we have \(n' = n\) and \(g' = g\).

theorem exists_unique_irreducible_separable_expand_eq {f : K[X]}
    (hf : Irreducible f) :
    ∃ (n : ℕ) (g : K[X]),
      (Irreducible g ∧ g.Separable ∧
        expand K ((ringChar K) ^ n) g = f) ∧
        ∀ (n' : ℕ) (g' : K[X]),
          Irreducible g' ∧ g'.Separable ∧
            expand K ((ringChar K) ^ n') g' = f →
              n' = n ∧ g' = g

Sources

• ATLAS NumberTheoryI, Corollary 4.5.

Uses 2

Proof usesIrreducible polynomials are expansions of separable irreducibles · The separable irreducible underlying an irreducible polynomial is unique

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.