Module

LocalHilbertSymbol.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertSymbol

11 declarations indexed from sourceView source ↗

Module documentation

Local Hilbert symbols

This file constructs the local Hilbert symbol from the public Kummer-theory and local-reciprocity APIs.

For b : Kˣ, a root β of X ^ n - b is chosen in the separable closure and the literal simple extension K(β) is formed. If K contains the n-th roots of unity, Kummer theory makes this extension finite abelian Galois. The Hilbert symbol is the root quotient of the local Artin automorphism, transported back to μₙ(K).

Imports2

Imported by7

def

chosenSimpleKummerNormResidueAutomorphism

L39 ↗

LocalClassFieldTheory.Kummer.chosenSimpleKummerNormResidueAutomorphism

Documentation

The local Artin automorphism of the concrete Kummer extension.

Source context 7 commands

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

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

Lean source · statement

def chosenSimpleKummerNormResidueAutomorphism
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
    Kˣ →* Gal((chosenSimpleKummerExtension K n hnK b)/K)

def

localHilbertSymbol

L52 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbol

Documentation

The local Hilbert symbol (a,b)ₙ, valued in the actual subgroup μₙ(K).

Source context 7 commands

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

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

Lean source · statement

def localHilbertSymbol
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    nthRootsSubgroup K (n : ℕ)

def

localHilbertSymbolHom

L63 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbolHom

Documentation

For fixed b, the local Hilbert symbol is a homomorphism in its first argument.

Source context 7 commands

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

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

Lean source · statement

def localHilbertSymbolHom
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
    Kˣ →* nthRootsSubgroup K (n : ℕ)

theorem

localHilbertSymbolHom_apply

L73 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbolHom_apply

Source context 7 commands

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

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

Lean source · statement

theorem localHilbertSymbolHom_apply
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertSymbolHom K n hnK hmu b a =
      localHilbertSymbol K n hnK hmu a b

theorem

localHilbertSymbol_map_eq_rootQuotient

L81 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbol_map_eq_rootQuotient

Documentation

Base change sends the Hilbert symbol to its defining root quotient.

Source context 7 commands

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

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

Lean source · statement

theorem localHilbertSymbol_map_eq_rootQuotient
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    nthRootsSubgroupMap K (chosenSimpleKummerExtension K n hnK b) (n : ℕ)
        (localHilbertSymbol K n hnK hmu a b) =
      ⟨rootQuotient
          (K := K) (L := chosenSimpleKummerExtension K n hnK b)
          (chosenSimpleKummerRootUnit K n hnK b)
          (chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a),
        chosenSimpleKummer_rootQuotient_mem K n hnK b
          (chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a)⟩

theorem

normResidueAutomorphism_map_rootUnit_eq_hilbertSymbol_mul

L108 ↗

LocalClassFieldTheory.Kummer.normResidueAutomorphism_map_rootUnit_eq_hilbertSymbol_mul

Documentation

The local Artin automorphism acts on the chosen radical by multiplication with the Hilbert symbol.

Source context 7 commands

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

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

Lean source · full declaration

theorem normResidueAutomorphism_map_rootUnit_eq_hilbertSymbol_mul
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    let E := chosenSimpleKummerExtension K n hnK b
    let sigma : Gal(E/K) :=
      chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a
    let beta : Eˣ := chosenSimpleKummerRootUnit K n hnK b
    Units.map sigma beta =
      Units.map (algebraMap K E).toMonoidHom
          (localHilbertSymbol K n hnK hmu a b).1 * beta := by
  let E := chosenSimpleKummerExtension K n hnK b
  let sigma : Gal(E/K) :=
    chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a
  let beta : Eˣ := chosenSimpleKummerRootUnit K n hnK b
  change Units.map sigma beta =
    Units.map (algebraMap K E).toMonoidHom
      (localHilbertSymbol K n hnK hmu a b).1 * beta
  have hmap0 := congrArg Subtype.val
    (localHilbertSymbol_map_eq_rootQuotient K n hnK hmu a b)
  have hmap :
      Units.map (algebraMap K E).toMonoidHom
          (localHilbertSymbol K n hnK hmu a b).1 =
        rootQuotient (K := K) (L := E) beta sigma := by
    change
      Units.map
          (algebraMap K (chosenSimpleKummerExtension K n hnK b)).toMonoidHom
          (localHilbertSymbol K n hnK hmu a b).1 =
        rootQuotient
          (K := K) (L := chosenSimpleKummerExtension K n hnK b)
          (chosenSimpleKummerRootUnit K n hnK b)
          (chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a) at hmap0
    simpa only [E, beta, sigma] using hmap0
  rw [hmap]
  simpa only [AlgEquiv.smul_units_def] using
    (rootQuotient_mul_right
      (K := K) (L := E) beta sigma).symm

theorem

normResidueAutomorphism_apply_root_eq_hilbertSymbol_mul

L146 ↗

LocalClassFieldTheory.Kummer.normResidueAutomorphism_apply_root_eq_hilbertSymbol_mul

Documentation

Element-valued form of the defining Artin action.

Source context 7 commands

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

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

Lean source · full declaration

theorem normResidueAutomorphism_apply_root_eq_hilbertSymbol_mul
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    let E := chosenSimpleKummerExtension K n hnK b
    let beta : E := (chosenSimpleKummerRootUnit K n hnK b : Eˣ)
    chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a beta =
      algebraMap K E ((localHilbertSymbol K n hnK hmu a b).1 : K) * beta := by
  let E := chosenSimpleKummerExtension K n hnK b
  let betaUnit : Eˣ := chosenSimpleKummerRootUnit K n hnK b
  have hunit :
      Units.map
          (chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a) betaUnit =
        Units.map (algebraMap K E).toMonoidHom
            (localHilbertSymbol K n hnK hmu a b).1 * betaUnit := by
    simpa only [E, betaUnit] using
      (normResidueAutomorphism_map_rootUnit_eq_hilbertSymbol_mul
        K n hnK hmu a b)
  exact congrArg (fun u : Eˣ => (u : E)) hunit

theorem

chosenSimpleKummerNormResidueAutomorphism_ker

L167 ↗

LocalClassFieldTheory.Kummer.chosenSimpleKummerNormResidueAutomorphism_ker

Documentation

The concrete Artin homomorphism has precisely the local norm subgroup as its kernel.

Source context 7 commands

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

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

Lean source · statement

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

theorem

localNormSubgroup_le_localHilbertSymbolHom_ker

L183 ↗

LocalClassFieldTheory.Kummer.localNormSubgroup_le_localHilbertSymbolHom_ker

Documentation

Every norm from K(ⁿ√b) is killed by the Hilbert-symbol character.

Source context 7 commands

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

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

Lean source · statement

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

def

localHilbertSymbolFromNormQuotient

L202 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbolFromNormQuotient

Documentation

The local Hilbert symbol descended to the concrete local norm quotient.

Source context 7 commands

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

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

Lean source · statement

def localHilbertSymbolFromNormQuotient
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
    LocalFieldTheory.NormQuotient K
        (chosenSimpleKummerExtension K n hnK b) →*
      nthRootsSubgroup K (n : ℕ)

theorem

localHilbertSymbolFromNormQuotient_normClass

L214 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbolFromNormQuotient_normClass

Source context 7 commands

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

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

Lean source · statement

theorem localHilbertSymbolFromNormQuotient_normClass
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertSymbolFromNormQuotient K n hnK hmu b
        (LocalFieldTheory.normClass K
          (chosenSimpleKummerExtension K n hnK b) a) =
      localHilbertSymbol K n hnK hmu a b

Module documentation

Local Hilbert symbols

Declarations