NYLL
Module

LocalHilbertKummerDual.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalHilbertKummerDual
7 declarations indexed from sourceView source ↗

Module documentation

The local Hilbert pairing as a linear dual embedding

Imports5
Imported by4

Declarations

instance

localHilbertDualCanonicalZModAddCommGroup

L25 ↗
ClassFieldTower.Martinet.Shafarevich.localHilbertDualCanonicalZModAddCommGroup
Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
Lean source · statement
instance localHilbertDualCanonicalZModAddCommGroup : AddCommGroup (ZMod (n : ℕ))
def

localNthRootsEquivMultiplicativeZMod

L29 ↗
ClassFieldTower.Martinet.Shafarevich.localNthRootsEquivMultiplicativeZMod
Documentation

A primitive root identifies the n-th roots of unity with additive ZMod n.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localHilbertDualCanonicalZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
def localNthRootsEquivMultiplicativeZMod
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty) :
    nthRootsSubgroup L (n : ℕ) ≃* Multiplicative (ZMod (n : ℕ))
def

localHilbertPairingZMod

L43 ↗
ClassFieldTower.Martinet.Shafarevich.localHilbertPairingZMod
Documentation

The local Hilbert pairing with its roots-of-unity values written in ZMod n.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localHilbertDualCanonicalZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
def localHilbertPairingZMod
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty) :
    (Lˣ ⧸ (powMonoidHom (n : ℕ) : Lˣ →* Lˣ).range) →*
      ((Lˣ ⧸ (powMonoidHom (n : ℕ) : Lˣ →* Lˣ).range) →*
        Multiplicative (ZMod (n : ℕ)))
def

localHilbertLinearFunctional

L68 ↗
ClassFieldTower.Martinet.Shafarevich.localHilbertLinearFunctional
Documentation

The Hilbert character of one local power class, regarded as a linear functional.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localHilbertDualCanonicalZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
def localHilbertLinearFunctional
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty)
    (a : absolutePowerClassModP L (n : ℕ)) :
    Module.Dual (ZMod (n : ℕ)) (absolutePowerClassModP L (n : ℕ))
def

localHilbertDualEmbedding

L82 ↗
ClassFieldTower.Martinet.Shafarevich.localHilbertDualEmbedding
Documentation

The local Hilbert pairing, curried as a ZMod n-linear map into the dual.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localHilbertDualCanonicalZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
def localHilbertDualEmbedding
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty) :
    absolutePowerClassModP L (n : ℕ) →ₗ[ZMod (n : ℕ)]
      Module.Dual (ZMod (n : ℕ)) (absolutePowerClassModP L (n : ℕ))
theorem

localHilbertDualEmbedding_apply

L118 ↗
ClassFieldTower.Martinet.Shafarevich.localHilbertDualEmbedding_apply
Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localHilbertDualCanonicalZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
theorem localHilbertDualEmbedding_apply
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty)
    (a b : absolutePowerClassModP L (n : ℕ)) :
    localHilbertDualEmbedding L n hmu a b =
      (localHilbertPairingZMod L n hmu
        (Additive.toMul a) (Additive.toMul b)).toAdd
theorem

localHilbertDualEmbedding_injective

L127 ↗
ClassFieldTower.Martinet.Shafarevich.localHilbertDualEmbedding_injective
Documentation

Nondegeneracy makes the dual-valued local Hilbert map injective.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
variable (L : Type) [Field L] [CharZero L]
variable [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localHilbertDualCanonicalZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
theorem localHilbertDualEmbedding_injective
    (hmu : (primitiveRoots (n : ℕ) L).Nonempty) :
    Function.Injective (localHilbertDualEmbedding L n hmu)

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