Module

ArtinSchreierPolynomial.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ArtinSchreierPolynomial

4 declarations indexed from sourceView source ↗

Module documentation

Splitting an Artin--Schreier polynomial from one root

In characteristic p, translating X ^ p - X by a root gives the full splitting of X ^ p - X - C a. This source is purely algebraic and places no irreducibility, degree, normality, or valuation hypothesis on the field.

Imports9

Mathlib.Algebra.Algebra.ZMod
Mathlib.Algebra.CharP.Algebra
Mathlib.Algebra.CharP.Lemmas
Mathlib.Algebra.Polynomial.Derivative
Mathlib.Algebra.Polynomial.Splits
Mathlib.FieldTheory.Finite.Basic
Mathlib.FieldTheory.Finite.GaloisField
Mathlib.FieldTheory.Separable
Mathlib.Tactic.Ring

Imported by2

def

artinSchreierPolynomial

L38 ↗

ValuationTheory.DiscreteValuationField.artinSchreierPolynomial

Documentation

The Artin--Schreier polynomial with parameter a.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u
variable {K : Type u} [CommRing K]

Lean source · statement

def artinSchreierPolynomial (p : ℕ) (a : K) : K[X]

theorem

artinSchreierPolynomial_separable

L42 ↗

ValuationTheory.DiscreteValuationField.artinSchreierPolynomial_separable

Documentation

Its derivative is -1, so it is separable.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u
variable {K : Type u} [CommRing K]

Lean source · statement

theorem artinSchreierPolynomial_separable
    (p : ℕ) [CharP K p] (a : K) :
    (artinSchreierPolynomial p a).Separable

theorem

artinSchreierPolynomial_isRoot_add_zmod

L55 ↗

ValuationTheory.DiscreteValuationField.artinSchreierPolynomial_isRoot_add_zmod

Documentation

Every prime-field translate of one root is again a root.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u
variable {K : Type u} [CommRing K]

Lean source · statement

theorem artinSchreierPolynomial_isRoot_add_zmod
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (a α : K) (hα : α ^ p - α = a) (c : ZMod p) :
    (artinSchreierPolynomial p a).IsRoot
      (α + ZMod.castHom (m := p) dvd_rfl K c)

theorem

artinSchreierPolynomial_splits_of_root

L73 ↗

ValuationTheory.DiscreteValuationField.artinSchreierPolynomial_splits_of_root

Documentation

A single root generates the full splitting after prime-field translation.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u
variable {K : Type u} [CommRing K]

Lean source · statement

theorem artinSchreierPolynomial_splits_of_root
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (a α : K) (hα : α ^ p - α = a) :
    (artinSchreierPolynomial p a).Splits

Module documentation

Splitting an Artin--Schreier polynomial from one root

Declarations

artinSchreierPolynomial

artinSchreierPolynomial_separable

artinSchreierPolynomial_isRoot_add_zmod

artinSchreierPolynomial_splits_of_root