Module

ArtinSchreierEisenstein.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ArtinSchreierEisenstein

10 declarations indexed from sourceView source ↗

Module documentation

The reciprocal Eisenstein polynomial for an Artin--Schreier extension

The polynomial X ^ n + C π * X ^ (n - 1) - C π is Eisenstein at a prime parameter π when 1 < n. In an integrally closed domain it remains irreducible over the fraction field. An inverse of any root satisfies α ^ n - α = π⁻¹.

These algebraic sources need neither Henselianity nor a valuation. In the intended DVR application, an irreducible uniformizer supplies the prime parameter, and n is the residue characteristic. Galois and ramification claims are not assumed here.

Imports11

Mathlib.Algebra.GroupWithZero.Divisibility
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Polynomial.Coeff
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.Algebra.Ring.Divisibility.Basic
Mathlib.RingTheory.Ideal.Maximal
Mathlib.RingTheory.Ideal.Operations
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Mathlib.RingTheory.Polynomial.GaussLemma
Mathlib.Tactic.Ring

Imported by4

def

artinSchreierInversePolynomial

L47 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial

Documentation

The polynomial of the inverse of a root of X ^ n - X - π⁻¹.

Source context 7 commands

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

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

Lean source · statement

def artinSchreierInversePolynomial (π : R) (n : ℕ) : R[X]

theorem

artinSchreierInversePolynomial_natDegree_le

L50 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_natDegree_le

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_natDegree_le
    (π : R) (n : ℕ) :
    (artinSchreierInversePolynomial π n).natDegree ≤ n

theorem

artinSchreierInversePolynomial_coeff_top

L60 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_coeff_top

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_coeff_top
    (π : R) (n : ℕ) (hn : 1 < n) :
    (artinSchreierInversePolynomial π n).coeff n = 1

theorem

artinSchreierInversePolynomial_monic

L71 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_monic

Documentation

The reciprocal Artin--Schreier polynomial is monic.

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_monic
    (π : R) (n : ℕ) (hn : 1 < n) :
    (artinSchreierInversePolynomial π n).Monic

theorem

artinSchreierInversePolynomial_natDegree

L79 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_natDegree

Documentation

Its degree is the prescribed exponent.

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_natDegree [Nontrivial R]
    (π : R) (n : ℕ) (hn : 1 < n) :
    (artinSchreierInversePolynomial π n).natDegree = n

theorem

artinSchreierInversePolynomial_coeff_zero

L86 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_coeff_zero

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_coeff_zero
    (π : R) (n : ℕ) (hn : 1 < n) :
    (artinSchreierInversePolynomial π n).coeff 0 = -π

theorem

artinSchreierInversePolynomial_isEisensteinAt

L96 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_isEisensteinAt

Documentation

A prime parameter makes the reciprocal polynomial Eisenstein.

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_isEisensteinAt [IsDomain R]
    (π : R) (hπ : Prime π) (n : ℕ) (hn : 1 < n) :
    (artinSchreierInversePolynomial π n).IsEisensteinAt
      (Ideal.span ({π} : Set R))

theorem

artinSchreierInversePolynomial_irreducible

L127 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_irreducible

Documentation

Eisenstein supplies irreducibility over the coefficient domain.

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_irreducible [IsDomain R]
    (π : R) (hπ : Prime π) (n : ℕ) (hn : 1 < n) :
    Irreducible (artinSchreierInversePolynomial π n)

theorem

artinSchreierInversePolynomial_map_irreducible

L137 ↗

ValuationTheory.DiscreteValuationField.artinSchreierInversePolynomial_map_irreducible

Documentation

The same polynomial is irreducible in the fraction field.

Source context 7 commands

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

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

Lean source · statement

theorem artinSchreierInversePolynomial_map_irreducible
    [IsDomain R] [IsIntegrallyClosed R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]
    (π : R) (hπ : Prime π) (n : ℕ) (hn : 1 < n) :
    Irreducible ((artinSchreierInversePolynomial π n).map (algebraMap R K))

theorem

artinSchreier_eq_of_inversePolynomial_root

L150 ↗

ValuationTheory.DiscreteValuationField.artinSchreier_eq_of_inversePolynomial_root

Documentation

Inverting an actual root gives the Artin--Schreier equation. The root input is supplied, for example, by AdjoinRoot.eval₂_root applied to the irreducible fraction-field polynomial above.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u v w

Lean source · statement

theorem artinSchreier_eq_of_inversePolynomial_root
    {K : Type v} {L : Type w} [Field K] [Field L] [Algebra K L]
    (π : K) (hπ : π ≠ 0) (n : ℕ) (hn : 1 < n)
    (β : L) (hβ : aeval β (artinSchreierInversePolynomial π n) = 0) :
    (β⁻¹) ^ n - β⁻¹ = algebraMap K L (π⁻¹)

Module documentation

The reciprocal Eisenstein polynomial for an Artin--Schreier extension

Declarations