NYLL
Module

FinitePlaceCyclotomicH1ValuationDual.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceCyclotomicH1ValuationDual
10 declarations indexed from sourceView source ↗

Module documentation

The cyclotomic local H¹ valuation line

At a finite place of the cyclotomic base, transport the normalized valuation functional from local power classes to intrinsic continuous H¹. Its image is exactly the annihilator of the valuation-zero subspace.

Imports2
Imported by1

Declarations

instance

finitePlaceCyclotomicH1ValuationDualFiniteDimensional

L30 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicH1ValuationDualFiniteDimensional
Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p)
instance

finitePlaceCyclotomicH1ValuationDualNumberField

L35 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicH1ValuationDualNumberField
Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
Lean source · statement
instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p)
instance

finitePlaceCyclotomicH1ValuationDualTopology

L39 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicH1ValuationDualTopology
Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
Lean source · statement
instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q)
instance

finitePlaceCyclotomicH1ValuationDualDiscreteTopology

L42 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicH1ValuationDualDiscreteTopology
Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
Lean source · statement
instance finitePlaceCyclotomicH1ValuationDualDiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q)
instance

finitePlaceCyclotomicH1ValuationDualModule

L46 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicH1ValuationDualModule
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicH1ValuationDualDiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
Lean source · statement
instance finitePlaceCyclotomicH1ValuationDualModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G))
def

finitePlaceCyclotomicCompletionH1ValuationDualEmbedding

L52 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1ValuationDualEmbedding
Documentation

The dual of the intrinsic-local Kummer valuation coordinate.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicH1ValuationDualDiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicH1ValuationDualModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceCyclotomicCompletionH1ValuationDualEmbedding
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    ZMod p →ₗ[ZMod p]
      Module.Dual (ZMod p)
        (ContinuousH1ZMod
          (p := p)
          (G := Field.absoluteGaloisGroup
            (v.adicCompletion (FinitePlaceCyclotomicBase F p))))
theorem

finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_apply

L65 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_apply
Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicH1ValuationDualDiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicH1ValuationDualModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_apply
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p)))
    (a : ZMod p)
    (chi : ContinuousH1ZMod
      (p := p)
      (G := Field.absoluteGaloisGroup
        (v.adicCompletion (FinitePlaceCyclotomicBase F p)))) :
    finitePlaceCyclotomicCompletionH1ValuationDualEmbedding F p v a chi =
      a * finitePlaceCyclotomicCompletionH1Valuation F p v chi
theorem

finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_eq_transport

L79 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_eq_transport
Documentation

The intrinsic H¹ valuation line is the old valuation-defect line transported through local Kummer theory.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicH1ValuationDualDiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicH1ValuationDualModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_eq_transport
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    finitePlaceCyclotomicCompletionH1ValuationDualEmbedding F p v =
      (finitePlaceCyclotomicCompletionKummerH1LinearEquiv F p v).symm.toLinearMap.dualMap.comp
        (finitePlaceValuationDefectDualEmbedding
          (FinitePlaceCyclotomicBase F p) p v)
theorem

finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_range

L90 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_range
Documentation

The transported valuation line is exactly the annihilator of local power classes of valuation zero.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicH1ValuationDualDiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicH1ValuationDualModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_range
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    LinearMap.range
        (finitePlaceCyclotomicCompletionH1ValuationDualEmbedding F p v) =
      (LinearMap.ker
        (finitePlaceCyclotomicCompletionH1Valuation F p v)).dualAnnihilator
theorem

finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_injective

L113 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_injective
Documentation

The transported valuation line remains injectively parametrized by ZMod p.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicH1ValuationDualFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicH1ValuationDualNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicH1ValuationDualTopology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicH1ValuationDualDiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicH1ValuationDualModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceCyclotomicCompletionH1ValuationDualEmbedding_injective
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    Function.Injective
      (finitePlaceCyclotomicCompletionH1ValuationDualEmbedding F p v)

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