Module

UniformizerDecomposition.lean

Nyll.EtaleFundamentalGroups.Kummer.Henselian.UniformizerDecomposition

2 declarations indexed from sourceView source ↗

Module documentation

Uniformizer decomposition without completeness

The usual complete-DVF uniformizer decomposition is ideal-theoretic: it uses only the DVR structure of the two valuation rings and compatibility of their valuations. This file records the resulting stronger DVF statement and chooses both uniformizers from the primitive DVF data.

Imports1

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Extensions

Imported by6

theorem

exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image_of_dvf

L31 ↗

EtaleFundamentalGroups.Kummer.exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image_of_dvf

Documentation

For a specified base uniformizer in a valued extension of discrete valuation fields, one can choose a target valuation-ring unit expressing its image as that unit times the corresponding power of any specified target uniformizer.

Source context 5 commands

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

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

Lean source · statement

theorem exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image_of_dvf
    {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
    (base : DVF.{u, v} K) (target : DVF.{w, x} L)
    [base.valuation.HasExtension target.valuation]
    {ϖ : base.valuationSubring} {π : target.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K))
    (hπ : target.valuation.IsUniformizer (π : L)) :
    ∃ u : target.valuationSubringˣ,
      integerMap base target ϖ =
        (u : target.valuationSubring) *
          π ^ ramificationIndex base target

theorem

exists_uniformizers_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image

L143 ↗

EtaleFundamentalGroups.Kummer.exists_uniformizers_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image