Module

FinitePlaceUnramifiedRadicalPairing.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceUnramifiedRadicalPairing

11 declarations indexed from sourceView source ↗

Module documentation

Unramified reciprocity characters on the ideal radical

An ideal-radical class has valuation zero modulo the coefficient prime at every finite place. Consequently, unramified local characters annihilate its localization, and changing a character by an unramified character does not change its value there. No roots-of-unity or parity hypothesis is needed.

Imports4

Imported by2

instance

finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup

L31 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))

Lean source · statement

instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ))

instance

finitePlaceUnramifiedRadicalValuativeRel

L35 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedRadicalValuativeRel

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup

Lean source · statement

instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F)

instance

finitePlaceUnramifiedRadicalLocalField

L37 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedRadicalLocalField

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v

Lean source · statement

instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F)

instance

finitePlaceUnramifiedRadicalTopology

L40 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedRadicalTopology

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v

Lean source · statement

instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ))

instance

finitePlaceUnramifiedRadicalDiscrete

L41 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedRadicalDiscrete

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥

Lean source · statement

instance finitePlaceUnramifiedRadicalDiscrete : DiscreteTopology (ZMod (n : ℕ))

instance

finitePlaceUnramifiedRadicalH1Module

L43 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedRadicalH1Module

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedRadicalDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _

Lean source · statement

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

theorem

finitePlaceLocalPowerClassValuation_idealRadical_eq_zero

L48 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceLocalPowerClassValuation_idealRadical_eq_zero

Documentation

An ideal-radical class has zero local valuation modulo the prime.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedRadicalDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceUnramifiedRadicalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem finitePlaceLocalPowerClassValuation_idealRadical_eq_zero
    (a : idealPowerRadicalModP F (n : ℕ)) :
    finitePlaceLocalPowerClassValuation F (n : ℕ) v
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a)) = 0

theorem

finitePlaceUnramifiedReciprocityPairing_idealRadical_eq_zero

L62 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedReciprocityPairing_idealRadical_eq_zero

Documentation

Unramified local reciprocity characters kill localized ideal radicals.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedRadicalDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceUnramifiedRadicalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem finitePlaceUnramifiedReciprocityPairing_idealRadical_eq_zero
    (chi : ContinuousH1ZMod (p := (n : ℕ))
      (G := Field.absoluteGaloisGroup (v.adicCompletion F)))
    (hchi : chi ∈ localStandardUnramifiedH1 (v.adicCompletion F) n)
    (a : idealPowerRadicalModP F (n : ℕ)) :
    localReciprocityH1PowerClassPairing (v.adicCompletion F) (n : ℕ) chi
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a)) = 0

theorem

finitePlaceReciprocityPairing_idealRadical_eq_of_sub_unramified

L79 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceReciprocityPairing_idealRadical_eq_of_sub_unramified

Documentation

The reciprocity pairing on the ideal radical depends only on ramification.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedRadicalDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceUnramifiedRadicalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem finitePlaceReciprocityPairing_idealRadical_eq_of_sub_unramified
    (chi psi : ContinuousH1ZMod (p := (n : ℕ))
      (G := Field.absoluteGaloisGroup (v.adicCompletion F)))
    (h : chi - psi ∈ localStandardUnramifiedH1 (v.adicCompletion F) n)
    (a : idealPowerRadicalModP F (n : ℕ)) :
    localReciprocityH1PowerClassPairing (v.adicCompletion F) (n : ℕ) chi
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a)) =
    localReciprocityH1PowerClassPairing (v.adicCompletion F) (n : ℕ) psi
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a))

theorem

finitePlaceDecompositionReciprocityPairing_idealRadical_eq_of_inertiaRestriction_eq

L96 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionReciprocityPairing_idealRadical_eq_of_inertiaRestriction_eq

Documentation

Equality on actual decomposition-group inertia suffices for equality of the localized ideal-radical reciprocity pairing.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedRadicalDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceUnramifiedRadicalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem finitePlaceDecompositionReciprocityPairing_idealRadical_eq_of_inertiaRestriction_eq
    (chi psi : ContinuousH1ZMod (p := (n : ℕ))
      (G := finitePlaceAbsoluteDecompositionGroup F v))
    (h : finitePlaceH1InertiaRestriction F (n : ℕ) v chi =
      finitePlaceH1InertiaRestriction F (n : ℕ) v psi)
    (a : idealPowerRadicalModP F (n : ℕ)) :
    localReciprocityH1PowerClassPairing (v.adicCompletion F) (n : ℕ)
      (finitePlaceDecompositionH1ToAdic F (n : ℕ) v chi)
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a)) =
    localReciprocityH1PowerClassPairing (v.adicCompletion F) (n : ℕ)
      (finitePlaceDecompositionH1ToAdic F (n : ℕ) v psi)
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a))

theorem

finitePlaceDecompositionReciprocityPairing_idealRadical_eq_of_character_inertia_eq

L117 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionReciprocityPairing_idealRadical_eq_of_character_inertia_eq

Documentation

Character-valued form: no passage to a chosen local cohomology representative is required of a caller comparing two global lifts.

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
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
variable (v : HeightOneSpectrum (𝓞 F))
local instance finitePlaceUnramifiedRadicalCanonicalZModAddCommGroup :
    AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finitePlaceUnramifiedRadicalValuativeRel : ValuativeRel (v.adicCompletion F) :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceUnramifiedRadicalLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finitePlaceUnramifiedRadicalTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceUnramifiedRadicalDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceUnramifiedRadicalH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule

Lean source · statement

theorem finitePlaceDecompositionReciprocityPairing_idealRadical_eq_of_character_inertia_eq
    (chi psi : finitePlaceAbsoluteDecompositionGroup F v →ₜ* Multiplicative (ZMod (n : ℕ)))
    (h : chi.comp (finitePlaceAbsoluteInertiaInclusion F v) =
      psi.comp (finitePlaceAbsoluteInertiaInclusion F v))
    (a : idealPowerRadicalModP F (n : ℕ)) :
    localReciprocityH1PowerClassPairing (v.adicCompletion F) (n : ℕ)
      (finitePlaceDecompositionH1ToAdic F (n : ℕ) v (h1OfCharacter chi))
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a)) =
    localReciprocityH1PowerClassPairing (v.adicCompletion F) (n : ℕ)
      (finitePlaceDecompositionH1ToAdic F (n : ℕ) v (h1OfCharacter psi))
      (finitePlacePowerClassLocalization F (n : ℕ) v
        (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) a))

Module documentation

Unramified reciprocity characters on the ideal radical

Declarations