Nyll.EtaleFundamentalGroups.Kummer.Henselian.TameUniformizerRadical

Module documentation

A uniformizer radical for a totally tamely ramified Henselian DVF extension

Suppose that the base residue field is separably closed of characteristic zero and that the target valuation ring is finite over the base valuation ring. The residue extension is then finite and separable, hence trivial. The local Dedekind identity makes the ramification index equal to the field degree, and characteristic zero makes this index invertible in both residue fields. Hensel's lemma absorbs the unit in the uniformizer comparison. The resulting root of a base uniformizer has an Eisenstein minimal polynomial of full degree, hence generates the target field.

theorem

exists_uniformizer_radical_generator_of_moduleFinite_of_charZeroResidue

L43 ↗

EtaleFundamentalGroups.Kummer.exists_uniformizer_radical_generator_of_moduleFinite_of_charZeroResidue

Documentation

A finite extension of Henselian valuation rings over a separably closed characteristic-zero residue field is generated by a root of a base uniformizer. Finiteness and characteristic zero make the residue extension finite separable, so separable closedness forces residue degree one. The final equivalence is the concrete AdjoinRoot standard form and sends its distinguished root to the chosen generator.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v w x

Lean source · statement

theorem exists_uniformizer_radical_generator_of_moduleFinite_of_charZeroResidue
    {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (base : HenselianDVF.{u, v} K) (target : HenselianDVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring]
    [IsScalarTower base.valuationSubring target.valuationSubring L]
    [IsSepClosed base.residueField]
    [CharZero base.residueField] :
    ∃ (ϖ : base.valuationSubring) (α : L)
        (e : AdjoinRoot
          (X ^ ramificationIndex base.toDVF target.toDVF - C (ϖ : K)) ≃ₐ[K] L),
      base.valuation.IsUniformizer (ϖ : K) ∧
        Prime ϖ ∧
          α ^ ramificationIndex base.toDVF target.toDVF =
            algebraMap K L (ϖ : K) ∧
            IntermediateField.adjoin K ({α} : Set L) = ⊤ ∧
              e (AdjoinRoot.root
                (X ^ ramificationIndex base.toDVF target.toDVF - C (ϖ : K))) = α

Module documentation

A uniformizer radical for a totally tamely ramified Henselian DVF extension

Declarations

exists_uniformizer_radical_generator_of_moduleFinite_of_charZeroResidue