NYLL
Module

ArtinSchreierResidue.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ArtinSchreierResidue
1 declaration indexed from sourceView source ↗

Module documentation

A cyclic Artin--Schreier extension with unchanged residue field

Choose a prime uniformizer in the actual base valuation ring and construct the Artin--Schreier extension from its reciprocal Eisenstein polynomial. The localized integral closure supplies an actual extension valuation. The constructed power basis and its integral minimal polynomial then give surjectivity of the actual residue-field map.

The valuation, its extension property, the power basis, and the Eisenstein condition are all outputs of the construction, never extra assumptions.

Imports6
Imported by1

Declarations

theorem

exists_cyclic_prime_extension_residueMap_surjective

L37 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_cyclic_prime_extension_residueMap_surjective
Documentation

A characteristic-p Henselian DVF has a cyclic degree-p extension with surjective actual residue-field map.

Source context 4 commands

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

namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u v
Lean source · statement
theorem HenselianDVF.exists_cyclic_prime_extension_residueMap_surjective
    {K : Type u} [Field K] (base : HenselianDVF.{u, v} K)
    (p : ℕ) [Fact p.Prime] [CharP K p] :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra K L)
      (_ : FiniteDimensional K L) (target : HenselianDVF.{u, 0} L)
      (_ : base.toDVF.valuation.HasExtension target.toDVF.valuation),
      Module.finrank K L = p ∧ IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L) ∧
      Function.Surjective (ValuedExtension.residueMap base.toDVF target.toDVF)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.