Module

HilbertPairingPerfect.lean

Nyll.ClassFieldTheory.Theorems.HilbertSymbols.HilbertPairingPerfect

3 declarations indexed from sourceView source ↗

Module documentation

Perfectness of a finite nondegenerate Hilbert pairing

When the power-class group is finite and the field contains a primitive n-th root of unity, its full group of μₙ-valued characters has the same order. Hence a nondegenerate pairing gives an equivalence with that dual.

Imports4

Nyll.ClassFieldTheory.Definitions.HilbertSymbols.IsLocalHilbertPairing
Mathlib.GroupTheory.FiniteAbelian.Duality
Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
Mathlib.SetTheory.Cardinal.Finite

Imported by3

theorem

powerClass_pow_order

L26 ↗

ClassFieldTheory.HilbertPairing.powerClass_pow_order

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

theorem powerClass_pow_order
    (K : Type u) [Field K] (n : ℕ+)
    (a : PowerClassGroup K n) : a ^ (n : ℕ) = 1

def

characterUnitsEquiv

L35 ↗

ClassFieldTheory.HilbertPairing.characterUnitsEquiv

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · full declaration

def characterUnitsEquiv
    (K : Type u) [Field K] (n : ℕ+) :
    (PowerClassGroup K n →* rootsOfUnity (n : ℕ) K) ≃
      (PowerClassGroup K n →* Kˣ) where
  toFun f := (rootsOfUnity (n : ℕ) K).subtype.comp f
  invFun f := f.codRestrict (rootsOfUnity (n : ℕ) K) (by
    intro a
    change (f a) ^ (n : ℕ) = 1
    rw [← map_pow, powerClass_pow_order K n a, map_one])
  left_inv f := by
    ext a
    rfl
  right_inv f := by
    ext a
    rfl

theorem

bijective

L53 ↗

ClassFieldTheory.HilbertPairing.IsNondegenerate.bijective

Documentation

A finite nondegenerate pairing on power classes is perfect: its adjoint map onto the full group of μₙ-valued characters is bijective.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory.HilbertPairing
universe u

Lean source · statement

theorem IsNondegenerate.bijective
    {K : Type u} [Field K] {n : ℕ+}
    [Finite (PowerClassGroup K n)]
    {B : HilbertPairing K n}
    (hB : B.IsNondegenerate)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Function.Bijective B

Module documentation

Perfectness of a finite nondegenerate Hilbert pairing

Declarations

powerClass_pow_order

characterUnitsEquiv

bijective