Module

FinitePlaceCyclotomicKummerH1.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceCyclotomicKummerH1

17 declarations indexed from sourceView source ↗

Module documentation

Local Kummer H¹ over the cyclotomic base

The cyclotomic base used by the ideal-radical construction contains the required primitive p-th roots. At every finite place, those roots remain primitive in the adic completion, so absolute Kummer theory identifies local power classes with continuous degree-one characters of the completion's absolute Galois group.

This is the intrinsic-local endpoint of the desired finite-place comparison. Transport to the chosen global decomposition subgroup still requires a topological local--global Galois equivalence; the available localization comparison is only a MulEquiv.

Imports4

Imported by4

abbrev

FinitePlaceCyclotomicBase

L38 ↗

ClassFieldTower.Martinet.Shafarevich.FinitePlaceCyclotomicBase

Documentation

The ideal-radical cyclotomic base with primality supplied by the ambient Fact.

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

abbrev FinitePlaceCyclotomicBase

instance

cyclotomicBaseFiniteDimensional

L41 ↗

ClassFieldTower.Martinet.Shafarevich.cyclotomicBaseFiniteDimensional

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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p)

instance

cyclotomicBaseNumberField

L46 ↗

ClassFieldTower.Martinet.Shafarevich.cyclotomicBaseNumberField

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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)

Lean source · statement

instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p)

instance

finitePlaceCyclotomicKummerCharacterTopology

L49 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicKummerCharacterTopology

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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)

Lean source · statement

instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p))

instance

finitePlaceCyclotomicKummerCharacterDiscreteTopology

L52 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicKummerCharacterDiscreteTopology

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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥

Lean source · statement

instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p))

instance

finitePlaceCyclotomicKummerH1Topology

L56 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicKummerH1Topology

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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _

Lean source · statement

instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q)

instance

finitePlaceCyclotomicKummerH1DiscreteTopology

L59 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicKummerH1DiscreteTopology

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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥

Lean source · statement

instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q)

instance

finitePlaceCyclotomicKummerH1Module

L63 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicKummerH1Module

Source context 13 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _

Lean source · statement

instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G))

theorem

finitePlaceCyclotomicCompletion_primitiveRoots_nonempty

L70 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletion_primitiveRoots_nonempty

Documentation

A primitive p-th root in the cyclotomic base stays primitive in every finite-place completion.

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceCyclotomicCompletion_primitiveRoots_nonempty
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    (primitiveRoots p
      (v.adicCompletion (FinitePlaceCyclotomicBase F p))).Nonempty

def

finitePlaceCyclotomicCompletionKummerLinearEquiv

L87 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionKummerLinearEquiv

Documentation

Local p-power classes at a finite place of the cyclotomic base are linearly equivalent to continuous multiplicative mod-p characters of the completion's absolute Galois group.

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceCyclotomicCompletionKummerLinearEquiv
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    FinitePlaceLocalPowerClassModP (FinitePlaceCyclotomicBase F p) p v ≃ₗ[ZMod p]
      absoluteContinuousZModCharacterModP
        (v.adicCompletion (FinitePlaceCyclotomicBase F p)) p

def

finitePlaceCyclotomicCompletionCharacterH1LinearEquiv

L99 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionCharacterH1LinearEquiv

Documentation

Reinterpret continuous multiplicative mod-p characters as additive continuous H¹ classes.

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceCyclotomicCompletionCharacterH1LinearEquiv
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    absoluteContinuousZModCharacterModP
        (v.adicCompletion (FinitePlaceCyclotomicBase F p)) p ≃ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p)
        (G := Field.absoluteGaloisGroup
          (v.adicCompletion (FinitePlaceCyclotomicBase F p)))

theorem

finitePlaceCyclotomicCompletionCharacterH1LinearEquiv_apply

L127 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionCharacterH1LinearEquiv_apply

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · full declaration

theorem finitePlaceCyclotomicCompletionCharacterH1LinearEquiv_apply
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p)))
    (chi : absoluteContinuousZModCharacterModP
      (v.adicCompletion (FinitePlaceCyclotomicBase F p)) p)
    (sigma : Field.absoluteGaloisGroup
      (v.adicCompletion (FinitePlaceCyclotomicBase F p))) :
    finitePlaceCyclotomicCompletionCharacterH1LinearEquiv F p v chi
        (Additive.ofMul sigma) =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup
                (v.adicCompletion (FinitePlaceCyclotomicBase F p)) →ₜ*
              Multiplicative (ZMod p))
          from chi) sigma).toAdd :=
  rfl

def

finitePlaceCyclotomicCompletionKummerH1LinearEquiv

L146 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionKummerH1LinearEquiv

Documentation

Intrinsic local Kummer theory in the additive continuous-H¹ convention used by the finite-place localization layer.

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceCyclotomicCompletionKummerH1LinearEquiv
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    FinitePlaceLocalPowerClassModP (FinitePlaceCyclotomicBase F p) p v ≃ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p)
        (G := Field.absoluteGaloisGroup
          (v.adicCompletion (FinitePlaceCyclotomicBase F p)))

theorem

finitePlaceCyclotomicCompletionKummerH1LinearEquiv_apply

L158 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionKummerH1LinearEquiv_apply

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · full declaration

theorem finitePlaceCyclotomicCompletionKummerH1LinearEquiv_apply
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p)))
    (x : FinitePlaceLocalPowerClassModP (FinitePlaceCyclotomicBase F p) p v)
    (sigma : Field.absoluteGaloisGroup
      (v.adicCompletion (FinitePlaceCyclotomicBase F p))) :
    finitePlaceCyclotomicCompletionKummerH1LinearEquiv F p v x
        (Additive.ofMul sigma) =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup
                (v.adicCompletion (FinitePlaceCyclotomicBase F p)) →ₜ*
              Multiplicative (ZMod p))
          from finitePlaceCyclotomicCompletionKummerLinearEquiv F p v x)
        sigma).toAdd :=
  rfl

def

finitePlaceCyclotomicCompletionH1Valuation

L176 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1Valuation

Documentation

The normalized finite-place valuation, transported across intrinsic local Kummer H¹.

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceCyclotomicCompletionH1Valuation
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    ContinuousH1ZMod
        (p := p)
        (G := Field.absoluteGaloisGroup
          (v.adicCompletion (FinitePlaceCyclotomicBase F p))) →ₗ[ZMod p]
      ZMod p

theorem

finitePlaceCyclotomicCompletionH1Valuation_kummer

L190 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1Valuation_kummer

Documentation

Under local Kummer H¹, the cohomological valuation coordinate is exactly the normalized adic valuation of the originating local power class.

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceCyclotomicCompletionH1Valuation_kummer
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p)))
    (x : FinitePlaceLocalPowerClassModP (FinitePlaceCyclotomicBase F p) p v) :
    finitePlaceCyclotomicCompletionH1Valuation F p v
        (finitePlaceCyclotomicCompletionKummerH1LinearEquiv F p v x) =
      finitePlaceLocalPowerClassValuation (FinitePlaceCyclotomicBase F p) p v x

theorem

finitePlaceCyclotomicCompletionH1Valuation_surjective

L200 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicCompletionH1Valuation_surjective

Documentation

The transported valuation on intrinsic local H¹ is surjective.

Source context 14 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 cyclotomicBaseFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance cyclotomicBaseNumberField : NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicKummerCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceCyclotomicKummerCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Topology (q : ℕ) :
    TopologicalSpace (ZMod q) := ⊥
local instance finitePlaceCyclotomicKummerH1DiscreteTopology (q : ℕ) :
    DiscreteTopology (ZMod q) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicKummerH1Module
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceCyclotomicCompletionH1Valuation_surjective
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    Function.Surjective
      (finitePlaceCyclotomicCompletionH1Valuation F p v)

Module documentation

Local Kummer H¹ over the cyclotomic base

Declarations