NYLL
Module

MathlibHilbertPairing.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.MathlibHilbertPairing
14 declarations indexed from sourceView source ↗

Module documentation

Mathlib-facing local Hilbert pairing

The existing local Artin construction is transported to the public power-class group and root-of-unity subgroup.

Imports11
Imported by3

Declarations

def

localHilbertSymbol

L38 ↗
ClassFieldTheory.localHilbertSymbol
Documentation

The local norm-residue Hilbert symbol, expressed in Mathlib's rootsOfUnity rather than the internal subgroup of units.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
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ˣ) :
    rootsOfUnity (n : ℕ) K
def

localHilbertPairing

L47 ↗
ClassFieldTheory.localHilbertPairing
Documentation

The descended local pairing, transported to Mathlib's PowerClassGroup and rootsOfUnity.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
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) :
    HilbertPairing K n
theorem

localHilbertPairing_powerClass

L59 ↗
ClassFieldTheory.localHilbertPairing_powerClass
Documentation

The public pairing evaluates to the public Hilbert symbol on representatives.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertPairing_powerClass
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertPairing K n hnK hmu (powerClass K n a) (powerClass K n b) =
      localHilbertSymbol K n hnK hmu a b
theorem

localHilbertSymbol_mul_left

L77 ↗
ClassFieldTheory.localHilbertSymbol_mul_left
Documentation

The local Hilbert symbol is multiplicative in its first variable.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_mul_left
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b c : Kˣ) :
    localHilbertSymbol K n hnK hmu (a * b) c =
      localHilbertSymbol K n hnK hmu a c *
        localHilbertSymbol K n hnK hmu b c
theorem

localHilbertSymbol_mul_right

L91 ↗
ClassFieldTheory.localHilbertSymbol_mul_right
Documentation

The local Hilbert symbol is multiplicative in its second variable.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_mul_right
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b c : Kˣ) :
    localHilbertSymbol K n hnK hmu a (b * c) =
      localHilbertSymbol K n hnK hmu a b *
        localHilbertSymbol K n hnK hmu a c
theorem

localHilbertSymbol_steinberg

L115 ↗
ClassFieldTheory.localHilbertSymbol_steinberg
Documentation

The local Hilbert symbol satisfies the Steinberg relation (a, 1 - a) = 1.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_steinberg
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (h_one_sub : 1 - (a : K) ≠ 0) :
    localHilbertSymbol K n hnK hmu a
        (Units.mk0 (1 - (a : K)) h_one_sub) = 1
theorem

localHilbertSymbol_skew

L134 ↗
ClassFieldTheory.localHilbertSymbol_skew
Documentation

The local Hilbert symbol is skew-symmetric.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_skew
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertSymbol K n hnK hmu a b =
      (localHilbertSymbol K n hnK hmu b a)⁻¹
theorem

localHilbertSymbol_left_kernel

L155 ↗
ClassFieldTheory.localHilbertSymbol_left_kernel
Documentation

The common left kernel of the local Hilbert symbol is the subgroup of n-th powers.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
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

L185 ↗
ClassFieldTheory.localHilbertSymbol_right_kernel
Documentation

The common right kernel of the local Hilbert symbol is the subgroup of n-th powers.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
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
theorem

localHilbertPairing_nondegenerate

L214 ↗
ClassFieldTheory.localHilbertPairing_nondegenerate
Documentation

The local Hilbert pairing separates power classes in both variables.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
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 : PowerClassGroup K n,
      (∀ b : PowerClassGroup K n,
        localHilbertPairing K n hnK hmu a b = 1) → a = 1) ∧
    (∀ b : PowerClassGroup K n,
      (∀ a : PowerClassGroup K n,
        localHilbertPairing K n hnK hmu a b = 1) → b = 1)
theorem

localHilbertSymbol_eq_one_iff_isKummerNorm

L247 ↗
ClassFieldTheory.localHilbertSymbol_eq_one_iff_isKummerNorm
Documentation

A local Hilbert symbol vanishes exactly when its second argument is a norm from the canonical, possibly reducible Kummer algebra of the first.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_eq_one_iff_isKummerNorm
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    localHilbertSymbol K n hnK hmu a b = 1 ↔ IsKummerNorm K n a b
theorem

localHilbertPairing_isLocalHilbertPairing

L290 ↗
ClassFieldTheory.localHilbertPairing_isLocalHilbertPairing
Documentation

The Mathlib-facing local Hilbert pairing obeys all local algebraic laws, including the canonical Kummer norm-residue criterion.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertPairing_isLocalHilbertPairing
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    HilbertPairing.IsLocalHilbertPairing
      (localHilbertPairing K n hnK hmu)
theorem

localHilbertPairing_artin_rootQuotient

L326 ↗
ClassFieldTheory.localHilbertPairing_artin_rootQuotient
Documentation

After mapping the public Hilbert value into the simple Kummer extension, it is the quotient of the Artin image of the chosen root by that root. The left pairing argument is the input to the canonical local Artin map.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory
Lean source · full declaration
theorem localHilbertPairing_artin_rootQuotient
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    let E := KummerTheory.chosenSimpleKummerExtension K n hnK a
    Units.map (algebraMap K E).toMonoidHom
        (localHilbertPairing K n hnK hmu
          (powerClass K n b) (powerClass K n a)).1 =
      KummerTheory.rootQuotient
        (K := K) (L := E)
        (KummerTheory.chosenSimpleKummerRootUnit K n hnK a)
        (LocalClassFieldTheory.Kummer.chosenSimpleKummerNormResidueAutomorphism
          K n hnK hmu a b) := by
  dsimp only
  rw [localHilbertPairing_powerClass]
  have h := congrArg Subtype.val
    (LocalClassFieldTheory.Kummer.localHilbertSymbol_map_eq_rootQuotient
      K n hnK hmu b a)
  change
    Units.map
      (algebraMap K (KummerTheory.chosenSimpleKummerExtension K n hnK a)).toMonoidHom
      (LocalClassFieldTheory.Kummer.localHilbertSymbol K n hnK hmu b a).1 =
      KummerTheory.rootQuotient
        (K := K) (L := KummerTheory.chosenSimpleKummerExtension K n hnK a)
        (KummerTheory.chosenSimpleKummerRootUnit K n hnK a)
        (LocalClassFieldTheory.Kummer.chosenSimpleKummerNormResidueAutomorphism
          K n hnK hmu a b) at h
  exact h
theorem

localHilbertPairing_artin_rootQuotient_of_same_pow

L360 ↗
ClassFieldTheory.localHilbertPairing_artin_rootQuotient_of_same_pow
Documentation

The public Type 0 Hilbert value agrees with the Artin root quotient for any root of a in the chosen simple Kummer extension, not only the root used to construct that extension. The pairing remains Artin-first.

Source context 2 commands

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

noncomputable section
namespace ClassFieldTheory
Lean source · statement
theorem localHilbertPairing_artin_rootQuotient_of_same_pow
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ)
    (u : (KummerTheory.chosenSimpleKummerExtension K n hnK a)ˣ)
    (hu : u ^ (n : ℕ) =
      Units.map
        (algebraMap K (KummerTheory.chosenSimpleKummerExtension K n hnK a)).toMonoidHom
        a) :
    Units.map
        (algebraMap K (KummerTheory.chosenSimpleKummerExtension K n hnK a)).toMonoidHom
        (localHilbertPairing K n hnK hmu
          (powerClass K n b) (powerClass K n a)).1 =
      KummerTheory.rootQuotient
        (K := K) (L := KummerTheory.chosenSimpleKummerExtension K n hnK a)
        u
        (LocalClassFieldTheory.Kummer.chosenSimpleKummerNormResidueAutomorphism
          K n hnK hmu a b)

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