NYLL
Module

KummerResidue.lean

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

Module documentation

A cyclic Kummer extension with unchanged residue field

A prime uniformizer supplies an Eisenstein Kummer polynomial. A primitive root of unity makes its actual root extension cyclic Galois. The localized integral closure then supplies the extension valuation, and the Eisenstein power basis proves that the actual residue-field map is surjective.

The comparison uses only the canonical coefficient-ring algebra belonging to that valuation tower. No residue characteristic or residue separability condition is imposed.

Imports6
Imported by2

Declarations

theorem

exists_cyclic_kummer_extension_residueMap_surjective

L36 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_cyclic_kummer_extension_residueMap_surjective
Documentation

A Henselian DVF containing a primitive r-th root of unity has a cyclic degree-r 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_kummer_extension_residueMap_surjective
    {K : Type u} [Field K] (base : HenselianDVF.{u, v} K)
    (r : ℕ) [Fact r.Prime] (ζ : K) (hζ : IsPrimitiveRoot ζ r) :
    ∃ (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 = r ∧ 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.