NYLL
Module

LocalUnramifiedArtinKummerRange.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalUnramifiedArtinKummerRange
12 declarations indexed from sourceView source ↗

Module documentation

Unramified Artin--Kummer duality and the valuation line

The intrinsic inertia-trivial subspace of local continuous H¹ is sent by the Artin--Kummer pairing precisely onto the valuation line in the dual. The proof uses actual unramified Kummer extensions and their Frobenius action, and applies also when the residue characteristic is the coefficient prime.

Imports4
Imported by4

Declarations

instance

localUnramifiedArtinKummerRangeTopology

L31 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedArtinKummerRangeTopology
Source context 6 commands

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

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

localUnramifiedArtinKummerRangeDiscreteTopology

L32 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedArtinKummerRangeDiscreteTopology
Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
Lean source · statement
instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ))
instance

localUnramifiedArtinKummerRangeModule

L34 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedArtinKummerRangeModule
Source context 8 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
Lean source · statement
instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G))
def

localStandardUnramifiedH1

L39 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardUnramifiedH1
Documentation

Intrinsic unramified H¹, written in the standard absolute-Galois model.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
def localStandardUnramifiedH1 :
    Submodule (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))
theorem

isUnramifiedChosenSimpleKummer_of_kummerH1_mem

L47 ↗
ClassFieldTower.Martinet.Shafarevich.isUnramifiedChosenSimpleKummer_of_kummerH1_mem
Documentation

An inertia-trivial Kummer character defines an actually unramified chosen simple extension, including in residue characteristic n.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem isUnramifiedChosenSimpleKummer_of_kummerH1_mem
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (ha : absoluteKummerContinuousH1LinearEquiv K (n : ℕ) hmu
      (Additive.ofMul
        (QuotientGroup.mk' (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a)) ∈
          localStandardUnramifiedH1 K n) :
    IsUnramifiedChosenSimpleKummer K n
      (Nat.cast_ne_zero.mpr (Fact.out : (n : ℕ).Prime).ne_zero) a
def

localStandardH1Valuation

L65 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardH1Valuation
Documentation

The local valuation, transported through absolute Kummer theory.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
def localStandardH1Valuation
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K) →ₗ[ZMod (n : ℕ)]
      ZMod (n : ℕ)
def

localStandardH1ValuationDualEmbedding

L73 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardH1ValuationDualEmbedding
Documentation

The valuation line in the dual of standard local H¹.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
def localStandardH1ValuationDualEmbedding
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    ZMod (n : ℕ) →ₗ[ZMod (n : ℕ)] Module.Dual (ZMod (n : ℕ))
      (ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))
theorem

localStandardH1ValuationDualEmbedding_apply

L81 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardH1ValuationDualEmbedding_apply
Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localStandardH1ValuationDualEmbedding_apply
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : ZMod (n : ℕ))
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K)) :
    localStandardH1ValuationDualEmbedding K n hmu a chi =
      a * localStandardH1Valuation K n hmu chi
theorem

localArtinKummerH1DualEmbedding_mk_unramified

L89 ↗
ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding_mk_unramified
Documentation

The local Artin--Kummer functional of an unramified radical is the Frobenius-scaled valuation functional on H¹.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localArtinKummerH1DualEmbedding_mk_unramified
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ)
    (ha : IsUnramifiedChosenSimpleKummer K n
      (Nat.cast_ne_zero.mpr (Fact.out : (n : ℕ).Prime).ne_zero) a) :
    localArtinKummerH1DualEmbedding K n hmu
        (absoluteKummerContinuousH1LinearEquiv K (n : ℕ) hmu
          (Additive.ofMul
            (QuotientGroup.mk' (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a))) =
      localStandardH1ValuationDualEmbedding K n hmu
        (unramifiedChosenSimpleKummerFrobeniusScalar K n hmu a ha)
theorem

localArtinKummerH1DualEmbedding_mem_valuation_range

L114 ↗
ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding_mem_valuation_range
Documentation

Intrinsic unramified classes map into the valuation dual line under local Artin--Kummer duality.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localArtinKummerH1DualEmbedding_mem_valuation_range
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K))
    (hchi : chi ∈ localStandardUnramifiedH1 K n) :
    localArtinKummerH1DualEmbedding K n hmu chi ∈
      LinearMap.range (localStandardH1ValuationDualEmbedding K n hmu)
theorem

localStandardUnramifiedH1_exists_ne_zero

L137 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardUnramifiedH1_exists_ne_zero
Documentation

The intrinsic unramified line is not zero.

Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
omit [CharZero K] in
Lean source · statement
theorem localStandardUnramifiedH1_exists_ne_zero :
    ∃ chi : ContinuousH1ZMod (p := (n : ℕ)) (G := Field.absoluteGaloisGroup K),
      chi ∈ localStandardUnramifiedH1 K n ∧ chi ≠ 0
theorem

localArtinKummerH1DualEmbedding_unramified_range

L159 ↗
ClassFieldTower.Martinet.Shafarevich.localArtinKummerH1DualEmbedding_unramified_range
Documentation

Local Artin--Kummer duality takes intrinsic unramified H¹ exactly onto the valuation dual line.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (K : Type) [Field K] [CharZero K]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable (n : ℕ+) [Fact ((n : ℕ).Prime)]
local instance localUnramifiedArtinKummerRangeTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance localUnramifiedArtinKummerRangeDiscreteTopology : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance localUnramifiedArtinKummerRangeModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localArtinKummerH1DualEmbedding_unramified_range
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    LinearMap.range
        ((localArtinKummerH1DualEmbedding K n hmu).comp
          (localStandardUnramifiedH1 K n).subtype) =
      LinearMap.range (localStandardH1ValuationDualEmbedding K n hmu)

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