NYLL
Module

FinitePlaceCyclotomicLocalDuality.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceCyclotomicLocalDuality
11 declarations indexed from sourceView source ↗

Module documentation

Artin--Kummer local duality at cyclotomic finite places

This file specializes the local Artin--Kummer H¹ pairing to completions of the cyclotomic base used in the ideal-radical construction. The representative formula is also stated for the natural mu_p Kummer class after the coefficient trivialization comparison.

Imports2
Imported by1

Declarations

instance

finitePlaceCyclotomicLocalDualityFiniteDimensional

L31 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicLocalDualityFiniteDimensional
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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ))
instance

finitePlaceCyclotomicLocalDualityNumberField

L36 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicLocalDualityNumberField
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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
Lean source · statement
instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ))
instance

finitePlaceCyclotomicLocalDualityValuativeRel

L40 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicLocalDualityValuativeRel
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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
Lean source · statement
instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ)))
instance

finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField

L49 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
Lean source · statement
instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ)))
instance

finitePlaceCyclotomicLocalDualityH1Topology

L58 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicLocalDualityH1Topology
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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
Lean source · statement
instance finitePlaceCyclotomicLocalDualityH1Topology :
    TopologicalSpace (ZMod (p : ℕ))
instance

finitePlaceCyclotomicLocalDualityH1DiscreteTopology

L61 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicLocalDualityH1DiscreteTopology
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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityH1Topology :
    TopologicalSpace (ZMod (p : ℕ)) := ⊥
Lean source · statement
instance finitePlaceCyclotomicLocalDualityH1DiscreteTopology :
    DiscreteTopology (ZMod (p : ℕ))
instance

finitePlaceCyclotomicLocalDualityH1Module

L65 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicLocalDualityH1Module
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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityH1Topology :
    TopologicalSpace (ZMod (p : ℕ)) := ⊥
local instance finitePlaceCyclotomicLocalDualityH1DiscreteTopology :
    DiscreteTopology (ZMod (p : ℕ)) :=
  discreteTopology_bot _
Lean source · statement
instance finitePlaceCyclotomicLocalDualityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (p : ℕ))
      (ContinuousH1ZMod (p := (p : ℕ)) (G := G))
def

finitePlaceCyclotomicArtinKummerH1DualEmbedding

L73 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicArtinKummerH1DualEmbedding
Documentation

The local Artin--Kummer pairing on continuous H¹ of a cyclotomic 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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityH1Topology :
    TopologicalSpace (ZMod (p : ℕ)) := ⊥
local instance finitePlaceCyclotomicLocalDualityH1DiscreteTopology :
    DiscreteTopology (ZMod (p : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicLocalDualityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (p : ℕ))
      (ContinuousH1ZMod (p := (p : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceCyclotomicArtinKummerH1DualEmbedding
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ContinuousH1ZMod
        (p := (p : ℕ))
        (G := Field.absoluteGaloisGroup
          (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ)))) →ₗ[ZMod (p : ℕ)]
      Module.Dual (ZMod (p : ℕ))
        (ContinuousH1ZMod
          (p := (p : ℕ))
          (G := Field.absoluteGaloisGroup
            (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ)))))
theorem

finitePlaceCyclotomicArtinKummerH1DualEmbedding_kummer

L93 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicArtinKummerH1DualEmbedding_kummer
Documentation

On local Kummer classes, the specialized pairing is the original local Hilbert pairing on completion power 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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityH1Topology :
    TopologicalSpace (ZMod (p : ℕ)) := ⊥
local instance finitePlaceCyclotomicLocalDualityH1DiscreteTopology :
    DiscreteTopology (ZMod (p : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicLocalDualityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (p : ℕ))
      (ContinuousH1ZMod (p := (p : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceCyclotomicArtinKummerH1DualEmbedding_kummer
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ))))
    (x y : FinitePlaceLocalPowerClassModP
      (FinitePlaceCyclotomicBase F (p : ℕ)) (p : ℕ) v) :
    finitePlaceCyclotomicArtinKummerH1DualEmbedding F p v
        (absoluteKummerContinuousH1LinearEquiv
          (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ)))
          (p : ℕ)
          (finitePlaceCyclotomicCompletion_primitiveRoots_nonempty
            F (p : ℕ) v) x)
        (absoluteKummerContinuousH1LinearEquiv
          (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ)))
          (p : ℕ)
          (finitePlaceCyclotomicCompletion_primitiveRoots_nonempty
            F (p : ℕ) v) y) =
      localHilbertDualEmbedding
        (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) p
        (finitePlaceCyclotomicCompletion_primitiveRoots_nonempty
          F (p : ℕ) v) x y
theorem

finitePlaceCyclotomicArtinKummerH1DualEmbedding_muPKummerClass

L121 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicArtinKummerH1DualEmbedding_muPKummerClass
Documentation

After the C03 coefficient trivialization, natural mu_p Kummer classes pair by the usual local Hilbert symbol on representatives.

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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityH1Topology :
    TopologicalSpace (ZMod (p : ℕ)) := ⊥
local instance finitePlaceCyclotomicLocalDualityH1DiscreteTopology :
    DiscreteTopology (ZMod (p : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicLocalDualityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (p : ℕ))
      (ContinuousH1ZMod (p := (p : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
theorem finitePlaceCyclotomicArtinKummerH1DualEmbedding_muPKummerClass
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ))))
    (a b : (v.adicCompletion
      (FinitePlaceCyclotomicBase F (p : ℕ)))ˣ) :
    let L := v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))
    let hmu := finitePlaceCyclotomicCompletion_primitiveRoots_nonempty
      F (p : ℕ) v
    finitePlaceCyclotomicArtinKummerH1DualEmbedding F p v
        (absoluteMuPH1EquivContinuousH1ZMod L (p : ℕ) hmu
          (absoluteKummerMuPH1Class L (p : ℕ) a))
        (absoluteMuPH1EquivContinuousH1ZMod L (p : ℕ) hmu
          (absoluteKummerMuPH1Class L (p : ℕ) b)) =
      ((localNthRootsEquivMultiplicativeZMod L p hmu)
        (LocalClassFieldTheory.Kummer.localHilbertSymbol L p
          (Nat.cast_ne_zero.mpr p.ne_zero) hmu a b)).toAdd := by
  dsimp only
  rw [absoluteMuPH1EquivContinuousH1ZMod_kummerClass,
    absoluteMuPH1EquivContinuousH1ZMod_kummerClass]
  exact localArtinKummerH1DualEmbedding_mk
    (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) p
    (finitePlaceCyclotomicCompletion_primitiveRoots_nonempty F (p : ℕ) v) a b
theorem

finitePlaceCyclotomicArtinKummerH1DualEmbedding_injective

L146 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicArtinKummerH1DualEmbedding_injective
Documentation

The specialized finite-place Artin--Kummer dual embedding is injective.

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 finitePlaceCyclotomicLocalDualityFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F (p : ℕ) (Fact.out : (p : ℕ).Prime)
local instance finitePlaceCyclotomicLocalDualityNumberField :
    NumberField (FinitePlaceCyclotomicBase F (p : ℕ)) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F (p : ℕ))
local instance finitePlaceCyclotomicLocalDualityValuativeRel
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    ValuativeRel
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionValuativeRel
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityIsNonarchimedeanLocalField
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    IsNonarchimedeanLocalField
      (v.adicCompletion (FinitePlaceCyclotomicBase F (p : ℕ))) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField
    (FinitePlaceCyclotomicBase F (p : ℕ)) v
local instance finitePlaceCyclotomicLocalDualityH1Topology :
    TopologicalSpace (ZMod (p : ℕ)) := ⊥
local instance finitePlaceCyclotomicLocalDualityH1DiscreteTopology :
    DiscreteTopology (ZMod (p : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceCyclotomicLocalDualityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (p : ℕ))
      (ContinuousH1ZMod (p := (p : ℕ)) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceCyclotomicArtinKummerH1DualEmbedding_injective
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers
        (FinitePlaceCyclotomicBase F (p : ℕ)))) :
    Function.Injective
      (finitePlaceCyclotomicArtinKummerH1DualEmbedding 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.