Module

LocalHilbertSymbolLaws.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertSymbolLaws

3 declarations indexed from sourceView source ↗

Module documentation

Kernel laws for the local Hilbert symbol

The local Hilbert-symbol character is the composite of the local Artin map, the injective character obtained by evaluating automorphisms on the chosen Kummer radical, and the equivalence that transports roots of unity back to the base field. Consequently its kernel is exactly the local norm subgroup. This also makes the induced character on the concrete norm quotient injective.

Imports1

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertSymbol

Imported by2

theorem

localHilbertSymbolHom_ker

L36 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbolHom_ker

Documentation

The kernel of the local Hilbert-symbol character is exactly the norm subgroup from the associated simple Kummer extension.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem localHilbertSymbolHom_ker
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
    (localHilbertSymbolHom K n hnK hmu b).ker =
      localNormSubgroup K (chosenSimpleKummerExtension K n hnK b)

theorem

localHilbertSymbol_eq_one_iff_mem_localNormSubgroup

L51 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbol_eq_one_iff_mem_localNormSubgroup

Documentation

A local Hilbert symbol is one exactly when its first argument is a norm from the simple Kummer extension determined by its second argument.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem localHilbertSymbol_eq_one_iff_mem_localNormSubgroup
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertSymbol K n hnK hmu a b = 1 ↔
      a ∈ localNormSubgroup K (chosenSimpleKummerExtension K n hnK b)

theorem

localHilbertSymbolFromNormQuotient_injective

L61 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbolFromNormQuotient_injective

Documentation

The local Hilbert-symbol character induced on the corresponding norm quotient is injective.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem localHilbertSymbolFromNormQuotient_injective
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
    Function.Injective
      (localHilbertSymbolFromNormQuotient K n hnK hmu b)

Module documentation

Kernel laws for the local Hilbert symbol

Declarations

localHilbertSymbolHom_ker

localHilbertSymbol_eq_one_iff_mem_localNormSubgroup

localHilbertSymbolFromNormQuotient_injective