Module

FiniteSupportIdeleCorrection.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FiniteSupportIdeleCorrection

7 declarations indexed from sourceView source ↗

Module documentation

Global correction of a finite local character family

If the local reciprocity functional annihilates the ideal-power radical, exactness of finite-valuation localization expresses it as a valuation functional. Subtracting the corresponding continuous idele character kills all principal ideles. Global reciprocity then gives an actual maximal abelian character agreeing with the prescribed family on local integral units; the valuation correction changes only the unramified part.

Imports3

Imported by2

instance

finiteSupportIdeleCorrectionZModAddCommGroup

L32 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSupportIdeleCorrectionZModAddCommGroup

Source context 6 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 GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]

Lean source · statement

instance finiteSupportIdeleCorrectionZModAddCommGroup : AddCommGroup (ZMod p)

instance

finiteSupportIdeleCorrectionTopology

L35 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSupportIdeleCorrectionTopology

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 GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteSupportIdeleCorrectionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup

Lean source · statement

instance finiteSupportIdeleCorrectionTopology : TopologicalSpace (ZMod p)

instance

finiteSupportIdeleCorrectionDiscreteTopology

L36 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSupportIdeleCorrectionDiscreteTopology

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 GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteSupportIdeleCorrectionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteSupportIdeleCorrectionTopology : TopologicalSpace (ZMod p) := ⊥

Lean source · statement

instance finiteSupportIdeleCorrectionDiscreteTopology : DiscreteTopology (ZMod p)

def

finiteSupportValuationCorrectedIdeleCharacter

L44 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSupportValuationCorrectedIdeleCharacter

Documentation

The local reciprocity product corrected by an algebraic valuation functional.

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 GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteSupportIdeleCorrectionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteSupportIdeleCorrectionTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportIdeleCorrectionDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))

Lean source · statement

def finiteSupportValuationCorrectedIdeleCharacter
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP F p)) :
    IdeleGroup F →ₜ* Multiplicative (ZMod p)

theorem

finiteSupportValuationCorrectedIdeleCharacter_principal

L50 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSupportValuationCorrectedIdeleCharacter_principal

Documentation

A functional explaining the principal values makes the corrected character principal-trivial.

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 GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteSupportIdeleCorrectionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteSupportIdeleCorrectionTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportIdeleCorrectionDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))

Lean source · statement

theorem finiteSupportValuationCorrectedIdeleCharacter_principal
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP F p))
    (hφ : finiteValuationLocalizationDual F p φ =
      finiteSupportLocalReciprocityPowerClassFunctional F p S chi) (a : Fˣ) :
    finiteSupportValuationCorrectedIdeleCharacter F p S chi φ
      (IdeleGroup.principalIdele F a) = 1

theorem

finiteSupportValuationCorrectedIdeleCharacter_finitePlace_integral

L64 ↗

ClassFieldTower.Martinet.Shafarevich.finiteSupportValuationCorrectedIdeleCharacter_finitePlace_integral

Documentation

Valuation correction preserves every prescribed local integral-unit value.

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 GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteSupportIdeleCorrectionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteSupportIdeleCorrectionTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportIdeleCorrectionDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))

Lean source · statement

theorem finiteSupportValuationCorrectedIdeleCharacter_finitePlace_integral
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP F p))
    (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ)
    (ha : a ∈ (v.adicCompletionIntegers F).units) :
    finiteSupportValuationCorrectedIdeleCharacter F p S chi φ
        (IdeleGroup.finitePlaceIdele v a) =
      finiteSupportLocalReciprocityIdeleCharacter F p S chi
        (IdeleGroup.finitePlaceIdele v a)

theorem

exists_maximalAbelianCharacter_of_finiteSupport_radical_annihilator

L78 ↗

ClassFieldTower.Martinet.Shafarevich.exists_maximalAbelianCharacter_of_finiteSupport_radical_annihilator

Documentation

Annihilating the ideal-power radical supplies a genuine global reciprocity character with the same integral-unit values as the finite local family.

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 GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance finiteSupportIdeleCorrectionZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finiteSupportIdeleCorrectionTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportIdeleCorrectionDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))

Lean source · statement

theorem exists_maximalAbelianCharacter_of_finiteSupport_radical_annihilator
    (hchi : absolutePowerClassDualRestriction F p
      (finiteSupportLocalReciprocityPowerClassFunctional F p S chi) = 0) :
    ∃ psi : Gal(maximalAbelianExtension F / F) →ₜ* Multiplicative (ZMod p),
      ∀ (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ),
        a ∈ (v.adicCompletionIntegers F).units →
          psi (maximalAbelianGlobalArtin F (IdeleGroup.finitePlaceIdeleClass v a)) =
            finiteSupportLocalReciprocityIdeleCharacter F p S chi
              (IdeleGroup.finitePlaceIdele v a)

Module documentation

Global correction of a finite local character family

Declarations

finiteSupportIdeleCorrectionZModAddCommGroup

finiteSupportIdeleCorrectionTopology

finiteSupportIdeleCorrectionDiscreteTopology

finiteSupportValuationCorrectedIdeleCharacter

finiteSupportValuationCorrectedIdeleCharacter_principal

finiteSupportValuationCorrectedIdeleCharacter_finitePlace_integral

exists_maximalAbelianCharacter_of_finiteSupport_radical_annihilator