NYLL
Module

TameRadicalGeneration.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.TameRadicalGeneration
2 declarations indexed from sourceView source ↗

Module documentation

Tame ramification implies radical generation

The corrected representatives of all value-group cosets generate an intermediate field with the same value group and residue field as the target. The immediate prime-to-p lemma then identifies that field with the target.

Imports1
Imported by4

Declarations

instance

exponentialValueGroupQuotientAddCommGroupForward

L29 ↗
AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotientAddCommGroupForward
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section FiniteTameRadicalGeneration
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
Lean source · statement
instance exponentialValueGroupQuotientAddCommGroupForward
    {F E : Type u} [Field F] [Field E]
    (v : LubinTate.Valuations.ExponentialValuation F)
    (w : LubinTate.Valuations.ExponentialValuation E) :
    AddCommGroup (ExponentialValueGroupQuotient v w)
theorem

generatedOverMaximalUnramifiedByRadicals_of_finiteTame

L39 ↗
AlgebraicNumberTheory.Valuations.generatedOverMaximalUnramifiedByRadicals_of_finiteTame
Documentation

A finite tame extension is generated over its maximal unramified subextension by prime-to-characteristic radicals.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section FiniteTameRadicalGeneration
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
local instance exponentialValueGroupQuotientAddCommGroupForward
    {F E : Type u} [Field F] [Field E]
    (v : LubinTate.Valuations.ExponentialValuation F)
    (w : LubinTate.Valuations.ExponentialValuation E) :
    AddCommGroup (ExponentialValueGroupQuotient v w) := by
  unfold ExponentialValueGroupQuotient
  infer_instance
Lean source · statement
theorem generatedOverMaximalUnramifiedByRadicals_of_finiteTame
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hTame : FiniteTamelyRamifiedExtension v w hExt) :
    GeneratedOverMaximalUnramifiedByRadicals v w hExt

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