NYLL
Module

KummerAlgebraOneNormSurjective.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.KummerAlgebraOneNormSurjective
1 declaration indexed from sourceView source ↗

Module documentation

The reducible Kummer algebra at one

Even when its rank is n, the algebra K[X]/(Xⁿ-1) has surjective norm under the local Kummer hypotheses. This is the simplest instance showing that norm index and algebra rank are different invariants.

Imports3
Imported by1

Declarations

theorem

kummerAlgebraNormSubgroup_one_eq_top

L26 ↗
ClassFieldTheory.kummerAlgebraNormSubgroup_one_eq_top
Documentation

The Kummer algebra defined by Xⁿ-1 has full unit norm image.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u
Lean source · statement
theorem kummerAlgebraNormSubgroup_one_eq_top
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    kummerAlgebraNormSubgroup K n 1 = ⊤

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