NYLL
Module

FiniteSupportDecompositionRadicalPairing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FiniteSupportDecompositionRadicalPairing
7 declarations indexed from sourceView source ↗

Module documentation

The linear radical pairing of a finite family of decomposition characters

Imports3
Imported by2

Declarations

instance

finiteDecompositionRadicalTopology

L22 ↗
ClassFieldTower.Martinet.Shafarevich.finiteDecompositionRadicalTopology
Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finiteDecompositionRadicalTopology : TopologicalSpace (ZMod p)
instance

finiteDecompositionRadicalDiscrete

L23 ↗
ClassFieldTower.Martinet.Shafarevich.finiteDecompositionRadicalDiscrete
Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteDecompositionRadicalTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance finiteDecompositionRadicalDiscrete : DiscreteTopology (ZMod p)
instance

finiteDecompositionRadicalValuative

L25 ↗
ClassFieldTower.Martinet.Shafarevich.finiteDecompositionRadicalValuative
Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteDecompositionRadicalTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteDecompositionRadicalDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
instance finiteDecompositionRadicalValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F)
instance

finiteDecompositionRadicalLocalField

L27 ↗
ClassFieldTower.Martinet.Shafarevich.finiteDecompositionRadicalLocalField
Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteDecompositionRadicalTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteDecompositionRadicalDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteDecompositionRadicalValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
Lean source · statement
instance finiteDecompositionRadicalLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F)
instance

finiteDecompositionRadicalModule

L30 ↗
ClassFieldTower.Martinet.Shafarevich.finiteDecompositionRadicalModule
Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteDecompositionRadicalTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteDecompositionRadicalDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteDecompositionRadicalValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteDecompositionRadicalLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
instance finiteDecompositionRadicalModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

finiteSupportDecompositionRadicalPairing

L38 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportDecompositionRadicalPairing
Documentation

Restrict the sum of localized reciprocity pairings to the global ideal radical. The input consists of actual characters on the absolute decomposition groups.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteDecompositionRadicalTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteDecompositionRadicalDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteDecompositionRadicalValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteDecompositionRadicalLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteDecompositionRadicalModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
Lean source · full declaration
def finiteSupportDecompositionRadicalPairing :
    (∀ v : ↥S, ContinuousH1ZMod (p := p)
      (G := finitePlaceAbsoluteDecompositionGroup F v.1)) →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP F p) where
  toFun chi := absolutePowerClassDualRestriction F p
    (finiteSupportLocalReciprocityPowerClassFunctional F p S
      (fun v => finitePlaceDecompositionH1ToAdic F p v.1 (chi v)))
  map_add' chi psi := by
    rw [← map_add (absolutePowerClassDualRestriction F p)]
    apply congrArg (absolutePowerClassDualRestriction F p)
    ext a
    simp only [finiteSupportLocalReciprocityPowerClassFunctional_apply,
      Pi.add_apply, map_add, LinearMap.add_apply, Finset.sum_add_distrib]
  map_smul' c chi := by
    change absolutePowerClassDualRestriction F p _ = c • absolutePowerClassDualRestriction F p _
    rw [← map_smul (absolutePowerClassDualRestriction F p)]
    apply congrArg (absolutePowerClassDualRestriction F p)
    ext a
    simp only [finiteSupportLocalReciprocityPowerClassFunctional_apply,
      Pi.smul_apply, map_smul, LinearMap.smul_apply, ← Finset.smul_sum]
theorem

finiteSupportDecompositionRadicalPairing_apply

L60 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportDecompositionRadicalPairing_apply
Documentation

Evaluation is the finite sum of the transported local characters' values.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteDecompositionRadicalTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteDecompositionRadicalDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteDecompositionRadicalValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteDecompositionRadicalLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteDecompositionRadicalModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
Lean source · statement
theorem finiteSupportDecompositionRadicalPairing_apply
    (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
      (G := finitePlaceAbsoluteDecompositionGroup F v.1))
    (a : idealPowerRadicalModP F p) :
    finiteSupportDecompositionRadicalPairing F p S chi a =
      ∑ v : ↥S, localReciprocityH1PowerClassPairing (v.1.adicCompletion F) p
        (finitePlaceDecompositionH1ToAdic F p v.1 (chi v))
        (finitePlacePowerClassLocalization F p v.1
          (idealPowerRadicalToAbsolutePowerClassLinearMap F p a))

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