Module

LocalHilbertPairingNondegeneracy.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertPairingNondegeneracy

13 declarations indexed from sourceView source ↗

Module documentation

Nondegeneracy of the local Hilbert pairing

The maximal finite Kummer extension identifies the common kernel of the local Hilbert-symbol characters with the subgroup of powers. The resulting symbol therefore descends to a nondegenerate pairing on the local power-class group.

Imports2

Imported by3

theorem

maximalLocalKummerPairing_eq_transpose

L32 ↗

LocalClassFieldTheory.Kummer.maximalLocalKummerPairing_eq_transpose

Source context 6 commands

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

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

Lean source · full declaration

theorem maximalLocalKummerPairing_eq_transpose
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    let Delta := maximalKummerSubgroup K n
    let E := maximalLocalKummerExtension K n
    letI : FiniteDimensional K E :=
      maximalKummerRadicalExtension_finiteDimensional K n hnK hmu
    letI : IsAbelianGalois K E :=
      kummerRadicalExtension_isAbelianGalois
        (K := K) (Omega := SeparableClosure K) n hmu Delta.1
    let hDelta : Delta.1 ≤
        finiteKummerRadicalSubgroup (K := K) (L := E) n :=
      le_finiteKummerRadicalSubgroup_kummerRadicalExtension
        n hnK Delta.1
    maximalLocalKummerPairingRightHom K n hnK hmu a b =
      (nthRootsSubgroupEquivOfPrimitiveRoots K E n hmu).symm
        (restrictedKummerTranspose n hmu Delta hDelta
          (maximalLocalKummerNormResidueAutomorphism K n hnK hmu a)
          (maximalRestrictedRadicalQuotientEquiv K n
            (QuotientGroup.mk'
              (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range b))) := by
  rfl

theorem

localHilbertSymbol_left_kernel

L57 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbol_left_kernel

Documentation

An element in the left kernel of every local Hilbert-symbol character is exactly an n-th power.

Source context 6 commands

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

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

Lean source · statement

theorem localHilbertSymbol_left_kernel
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    (∀ b : Kˣ, localHilbertSymbol K n hnK hmu a b = 1) ↔
      a ∈ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range

theorem

localHilbertSymbol_right_kernel

L128 ↗

LocalClassFieldTheory.Kummer.localHilbertSymbol_right_kernel

Documentation

An element in the right kernel of every local Hilbert-symbol character is exactly an n-th power.

Source context 6 commands

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

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

Lean source · statement

theorem localHilbertSymbol_right_kernel
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
    (∀ a : Kˣ, localHilbertSymbol K n hnK hmu a b = 1) ↔
      b ∈ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range

def

localHilbertRightPowerClassHom

L140 ↗

LocalClassFieldTheory.Kummer.localHilbertRightPowerClassHom

Source context 6 commands

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

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

Lean source · statement

def localHilbertRightPowerClassHom
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    (Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) →*
      nthRootsSubgroup K (n : ℕ)

theorem

localHilbertRightPowerClassHom_mk

L160 ↗

LocalClassFieldTheory.Kummer.localHilbertRightPowerClassHom_mk

Source context 6 commands

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

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

Lean source · statement

theorem localHilbertRightPowerClassHom_mk
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertRightPowerClassHom K n hnK hmu a
        (QuotientGroup.mk'
          (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range b) =
      maximalLocalKummerPairingRightHom K n hnK hmu a b

def

localHilbertPowerClassLeftHom

L169 ↗

LocalClassFieldTheory.Kummer.localHilbertPowerClassLeftHom

Source context 6 commands

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

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

Lean source · full declaration

def localHilbertPowerClassLeftHom
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Kˣ →*
      ((Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) →*
        nthRootsSubgroup K (n : ℕ)) where
  toFun a := localHilbertRightPowerClassHom K n hnK hmu a
  map_one' := by
    apply MonoidHom.ext
    intro q
    obtain ⟨b, rfl⟩ := QuotientGroup.mk'_surjective
      (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range q
    change maximalLocalKummerPairingRightHom K n hnK hmu 1 b = 1
    rw [maximalLocalKummerPairingRightHom_eq_localHilbertSymbolHom]
    exact map_one (localHilbertSymbolHom K n hnK hmu b)
  map_mul' := by
    intro a c
    apply MonoidHom.ext
    intro q
    obtain ⟨b, rfl⟩ := QuotientGroup.mk'_surjective
      (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range q
    change
      maximalLocalKummerPairingRightHom K n hnK hmu (a * c) b =
        maximalLocalKummerPairingRightHom K n hnK hmu a b *
          maximalLocalKummerPairingRightHom K n hnK hmu c b
    rw [maximalLocalKummerPairingRightHom_eq_localHilbertSymbolHom,
      maximalLocalKummerPairingRightHom_eq_localHilbertSymbolHom,
      maximalLocalKummerPairingRightHom_eq_localHilbertSymbolHom]
    exact map_mul (localHilbertSymbolHom K n hnK hmu b) a c

theorem

powMonoidHom_range_le_localHilbertPowerClassLeftHom_ker

L199 ↗

LocalClassFieldTheory.Kummer.powMonoidHom_range_le_localHilbertPowerClassLeftHom_ker

Source context 6 commands

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

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

Lean source · statement

theorem powMonoidHom_range_le_localHilbertPowerClassLeftHom_ker
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≤
      MonoidHom.ker (localHilbertPowerClassLeftHom K n hnK hmu)

def

localHilbertPairing

L223 ↗

LocalClassFieldTheory.Kummer.localHilbertPairing

Documentation

The local Hilbert symbol descended in both variables to the local power-class group.

Source context 6 commands

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

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

Lean source · statement

def localHilbertPairing
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    (Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) →*
      ((Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) →*
        nthRootsSubgroup K (n : ℕ))

theorem

localHilbertPairing_apply

L238 ↗

LocalClassFieldTheory.Kummer.localHilbertPairing_apply

Documentation

Evaluation of the descended pairing agrees with the original local Hilbert symbol on representatives.

Source context 6 commands

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

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

Lean source · statement

theorem localHilbertPairing_apply
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertPairing K n hnK hmu
        (QuotientGroup.mk'
          (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a)
        (QuotientGroup.mk'
          (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range b) =
      localHilbertSymbol K n hnK hmu a b

def

localHilbertPairingFlip

L254 ↗

LocalClassFieldTheory.Kummer.localHilbertPairingFlip

Documentation

The transposed descended pairing, viewed as a homomorphism into the character group.

Source context 6 commands

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

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

Lean source · full declaration

def localHilbertPairingFlip
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    (Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) →*
      ((Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) →*
        nthRootsSubgroup K (n : ℕ)) where
  toFun b :=
    { toFun := fun a => localHilbertPairing K n hnK hmu a b
      map_one' := by
        change localHilbertPairing K n hnK hmu 1 b = 1
        rw [map_one]
        rfl
      map_mul' := by
        intro a c
        change localHilbertPairing K n hnK hmu (a * c) b =
          localHilbertPairing K n hnK hmu a b *
            localHilbertPairing K n hnK hmu c b
        rw [map_mul]
        rfl }
  map_one' := by
    apply MonoidHom.ext
    intro a
    exact map_one (localHilbertPairing K n hnK hmu a)
  map_mul' := by
    intro b c
    apply MonoidHom.ext
    intro a
    exact map_mul (localHilbertPairing K n hnK hmu a) b c

theorem

localHilbertPairing_injective_left

L285 ↗

LocalClassFieldTheory.Kummer.localHilbertPairing_injective_left

Documentation

The descended local Hilbert pairing separates power classes in its left variable.

Source context 6 commands

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

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

Lean source · statement

theorem localHilbertPairing_injective_left
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Function.Injective (localHilbertPairing K n hnK hmu)

theorem

localHilbertPairing_injective_right

L325 ↗

LocalClassFieldTheory.Kummer.localHilbertPairing_injective_right

Documentation

The descended local Hilbert pairing separates power classes in its right variable.

Source context 6 commands

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

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

Lean source · statement

theorem localHilbertPairing_injective_right
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Function.Injective (localHilbertPairingFlip K n hnK hmu)

theorem

localHilbertPairing_nondegenerate

L363 ↗

LocalClassFieldTheory.Kummer.localHilbertPairing_nondegenerate

Documentation

The local Hilbert pairing on power classes is nondegenerate in both variables.

Source context 6 commands

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

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

Lean source · statement

theorem localHilbertPairing_nondegenerate
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    (∀ a,
      (∀ b, localHilbertPairing K n hnK hmu a b = 1) → a = 1) ∧
    (∀ b,
      (∀ a, localHilbertPairing K n hnK hmu a b = 1) → b = 1)

Module documentation

Nondegeneracy of the local Hilbert pairing

Declarations