Nyll.GaloisCohomology.Kummer.Concrete.LocalUnitKummerUnramified

Module documentation

Unramified local unit Kummer generators

This file packages the complete-DVF derivative criterion for a field extension generated by an n-th root of a unit, with n itself a unit in the base field. The statement is independent of the global Kummer construction so it can be reused by local reciprocity arguments.

theorem

isUnramifiedValuedExtension_of_unit_kummer_generator

L34 ↗

KummerTheory.isUnramifiedValuedExtension_of_unit_kummer_generator

Documentation

A finite separable extension generated by an n-th root of a unit is unramified when n is a unit in the base field.

Source context 5 commands

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

open scoped ValuativeRel
open LocalFieldTheory
noncomputable section
namespace KummerTheory
open _root_.RamificationTheory.DiscreteValuationField.ValuedExtension (
  isUnramifiedAt_of_aeval_derivative_isUnit
) in

Lean source · statement

theorem isUnramifiedValuedExtension_of_unit_kummer_generator
    {C F : Type}
    [Field C] [Field F] [Algebra C F]
    [FiniteDimensional C F]
    [Algebra.IsSeparable C F]
    [ValuativeRel C] [ValuativeRel F]
    [TopologicalSpace C] [TopologicalSpace F]
    [IsNonarchimedeanLocalField C]
    [IsNonarchimedeanLocalField F]
    [Valuation.HasExtension
      (ValuativeRel.valuation C) (ValuativeRel.valuation F)]
    [Algebra 𝒪[C] F]
    [Module.Finite 𝒪[C] 𝒪[F]]
    (n : ℕ+)
    (b : C)
    (beta : F)
    (hb : ValuativeRel.valuation C b = 1)
    (hn : ValuativeRel.valuation C ((n : ℕ) : C) = 1)
    (hbeta : ValuativeRel.valuation F beta = 1)
    (hpow : beta ^ (n : ℕ) = algebraMap C F b)
    (hgen : Algebra.adjoin C {beta} = ⊤) :
    LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension C F

Module documentation

Unramified local unit Kummer generators

Declarations

isUnramifiedValuedExtension_of_unit_kummer_generator