Module

CyclotomicKummerDescent.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.CyclotomicKummerDescent

1 declaration indexed from sourceView source ↗

Module documentation

Cyclotomic descent for maximal Kummer norm subgroups

For an exponent nonzero in the base field, adjoining the roots of unity, applying maximal Kummer theory, and descending the norm inclusion produces a finite Galois extension whose norm subgroup is contained in Kˣⁿ.

Imports4

Imported by3

theorem

exists_finiteGalois_normSubgroup_le_powMonoidHom_range

L35 ↗

LocalClassFieldTheory.exists_finiteGalois_normSubgroup_le_powMonoidHom_range

Documentation

There is a finite Galois extension whose local norm subgroup is contained in the n-th-power subgroup, without assuming roots of unity in the base.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped NNReal ValuativeRel
open CyclicCohomology KummerTheory ClassFormation
open LocalFieldTheory.DiscreteValuationField LocalFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem exists_finiteGalois_normSubgroup_le_powMonoidHom_range
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) :
    ∃ E : FiniteGaloisIntermediateField K (SeparableClosure K),
      localNormSubgroup K (E : IntermediateField K (SeparableClosure K)) ≤
        (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range

Module documentation

Cyclotomic descent for maximal Kummer norm subgroups

Declarations

exists_finiteGalois_normSubgroup_le_powMonoidHom_range