NYLL
Module

LocalUnramifiedKummerValuationDual.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalUnramifiedKummerValuationDual
13 declarations indexed from sourceView source ↗

Module documentation

The valuation dual of an unramified Kummer class

Unramified Hilbert characters are scalar multiples of reduced normalized valuation. Nondegeneracy shows that the Frobenius scalar of a nonzero class is nonzero, including at places above the Kummer exponent.

Imports2
Imported by2

Declarations

instance

(anonymous instance)

L32 ↗
Source context 8 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance : AddCommGroup (ZMod p)
instance

(anonymous instance)

L33 ↗
Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
Lean source · statement
instance : Module (ZMod p) (ZMod p)
def

localPowerClassValuationMonoidHom

L36 ↗
ClassFieldTower.Martinet.Shafarevich.localPowerClassValuationMonoidHom
Documentation

Reduced normalized valuation on local power classes.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
def localPowerClassValuationMonoidHom :
    (Kˣ ⧸ (powMonoidHom p : Kˣ →* Kˣ).range) →* Multiplicative (ZMod p)
def

localPowerClassValuation

L47 ↗
ClassFieldTower.Martinet.Shafarevich.localPowerClassValuation
Documentation

The reduced local valuation as a linear functional.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
def localPowerClassValuation :
    absolutePowerClassModP K p →ₗ[ZMod p] ZMod p
theorem

localPowerClassValuation_mk

L56 ↗
ClassFieldTower.Martinet.Shafarevich.localPowerClassValuation_mk
Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
theorem localPowerClassValuation_mk (a : Kˣ) :
    localPowerClassValuation K p
        (Additive.ofMul (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a)) =
      (valuationMap K (Additive.ofMul a) : ZMod p)
theorem

localPowerClassValuation_surjective

L65 ↗
ClassFieldTower.Martinet.Shafarevich.localPowerClassValuation_surjective
Documentation

Local valuation on power classes is onto.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
theorem localPowerClassValuation_surjective :
    Function.Surjective (localPowerClassValuation K p)
def

localPowerClassValuationDualEmbedding

L75 ↗
ClassFieldTower.Martinet.Shafarevich.localPowerClassValuationDualEmbedding
Documentation

The one-dimensional valuation line in the dual of local power classes.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
def localPowerClassValuationDualEmbedding :
    ZMod p →ₗ[ZMod p] Module.Dual (ZMod p) (absolutePowerClassModP K p)
theorem

localPowerClassValuationDualEmbedding_apply

L80 ↗
ClassFieldTower.Martinet.Shafarevich.localPowerClassValuationDualEmbedding_apply
Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
theorem localPowerClassValuationDualEmbedding_apply
    (a : ZMod p) (x : absolutePowerClassModP K p) :
    localPowerClassValuationDualEmbedding K p a x =
      a * localPowerClassValuation K p x
theorem

localPowerClassValuationDualEmbedding_injective

L86 ↗
ClassFieldTower.Martinet.Shafarevich.localPowerClassValuationDualEmbedding_injective
Documentation

The valuation line is faithfully parametrized by ZMod p.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
section Valuation
variable (p : ℕ) [Fact p.Prime]
local instance : AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance : Module (ZMod p) (ZMod p) := Semiring.toModule
Lean source · statement
theorem localPowerClassValuationDualEmbedding_injective :
    Function.Injective (localPowerClassValuationDualEmbedding K p)
instance

(anonymous instance)

L98 ↗
Source context 8 commands

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

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

unramifiedChosenSimpleKummerFrobeniusScalar

L103 ↗
ClassFieldTower.Martinet.Shafarevich.unramifiedChosenSimpleKummerFrobeniusScalar
Documentation

The scalar of an unramified Kummer Hilbert character in the normalized valuation coordinate.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [CharZero K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
Lean source · statement
def unramifiedChosenSimpleKummerFrobeniusScalar
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (ha : IsUnramifiedChosenSimpleKummer K n (Nat.cast_ne_zero.mpr n.ne_zero) a) :
    ZMod (n : ℕ)
theorem

localHilbertDualEmbedding_mk_unramified

L113 ↗
ClassFieldTower.Martinet.Shafarevich.localHilbertDualEmbedding_mk_unramified
Documentation

The Hilbert dual functional of an unramified Kummer radical is its Frobenius scalar times the reduced valuation.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [CharZero K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
Lean source · statement
theorem localHilbertDualEmbedding_mk_unramified
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (ha : IsUnramifiedChosenSimpleKummer K n (Nat.cast_ne_zero.mpr n.ne_zero) a) :
    localHilbertDualEmbedding K n hmu
        (Additive.ofMul
          (QuotientGroup.mk' (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a)) =
      localPowerClassValuationDualEmbedding K (n : ℕ)
        (unramifiedChosenSimpleKummerFrobeniusScalar K n hmu a ha)
theorem

unramifiedChosenSimpleKummerFrobeniusScalar_ne_zero

L144 ↗
ClassFieldTower.Martinet.Shafarevich.unramifiedChosenSimpleKummerFrobeniusScalar_ne_zero
Documentation

A nonzero unramified Kummer class has a nonzero Frobenius scalar.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory LocalClassFieldTheory LocalClassFieldTheory.Kummer
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [CharZero K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.commRing (n : ℕ)).toAddCommGroup
Lean source · statement
theorem unramifiedChosenSimpleKummerFrobeniusScalar_ne_zero
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (ha : IsUnramifiedChosenSimpleKummer K n (Nat.cast_ne_zero.mpr n.ne_zero) a)
    (ha0 : QuotientGroup.mk' (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a ≠ 1) :
    unramifiedChosenSimpleKummerFrobeniusScalar K n hmu a ha ≠ 0

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