NYLL
Module

AbsoluteCharacterRadicalReciprocity.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.AbsoluteCharacterRadicalReciprocity
8 declarations indexed from sourceView source ↗

Module documentation

Reciprocity annihilates global-character ramification on the ideal radical

An absolute finite character supplies an actual principal-trivial idele character. Outside a finite support, inertia-triviality kills integral units. Global reciprocity then proves that the sum of its local pairings on that support annihilates the ideal-power radical. This is the choice-independence input for the Shafarevich obstruction functional.

Imports7
Imported by5

Declarations

instance

absoluteRadicalReciprocityTopology

L34 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteRadicalReciprocityTopology
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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
Lean source · statement
instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ))
instance

absoluteRadicalReciprocityDiscrete

L35 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteRadicalReciprocityDiscrete
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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
Lean source · statement
instance absoluteRadicalReciprocityDiscrete : DiscreteTopology (ZMod (n : ℕ))
instance

absoluteRadicalReciprocityValuative

L37 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteRadicalReciprocityValuative
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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance absoluteRadicalReciprocityDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
Lean source · statement
instance absoluteRadicalReciprocityValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F)
instance

absoluteRadicalReciprocityLocalField

L39 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteRadicalReciprocityLocalField
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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance absoluteRadicalReciprocityDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance absoluteRadicalReciprocityValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
Lean source · statement
instance absoluteRadicalReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F)
instance

absoluteRadicalReciprocityModule

L42 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteRadicalReciprocityModule
Source context 11 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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance absoluteRadicalReciprocityDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance absoluteRadicalReciprocityValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance absoluteRadicalReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
instance absoluteRadicalReciprocityModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G))
theorem

localReciprocityUnitCharacter_absoluteCharacter

L51 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitCharacter_absoluteCharacter
Documentation

Actual local reciprocity evaluates a restricted absolute character by the associated global idele character.

Source context 13 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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance absoluteRadicalReciprocityDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance absoluteRadicalReciprocityValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance absoluteRadicalReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance absoluteRadicalReciprocityModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
Lean source · statement
theorem localReciprocityUnitCharacter_absoluteCharacter
    (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ) :
    localReciprocityUnitCharacter (v.adicCompletion F) (n : ℕ)
      (finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v (Additive.ofMul chi)) a =
    globalReciprocityIdeleCharacter F (n : ℕ) chi (IdeleGroup.finitePlaceIdele v a)
theorem

globalReciprocityIdeleCharacter_integral_eq_one_of_inertia

L62 ↗
ClassFieldTower.Martinet.Shafarevich.globalReciprocityIdeleCharacter_integral_eq_one_of_inertia
Documentation

Killing actual absolute inertia kills the actual adic integral units under the associated global idele character.

Source context 13 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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance absoluteRadicalReciprocityDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance absoluteRadicalReciprocityValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance absoluteRadicalReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance absoluteRadicalReciprocityModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
Lean source · statement
theorem globalReciprocityIdeleCharacter_integral_eq_one_of_inertia
    (v : HeightOneSpectrum (𝓞 F))
    (hchi : ∀ sigma : finitePlaceAbsoluteInertiaSubgroup F v,
      chi (finitePlaceAbsoluteDecompositionInclusion F v sigma.1) = 1)
    (a : (v.adicCompletion F)ˣ) (ha : a ∈ (v.adicCompletionIntegers F).units) :
    globalReciprocityIdeleCharacter F (n : ℕ) chi (IdeleGroup.finitePlaceIdele v a) = 1
theorem

absoluteCharacter_finiteSupport_radical_annihilator

L80 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteCharacter_finiteSupport_radical_annihilator
Documentation

The finite-support reciprocity functional of a global character is zero on the ideal radical whenever all ramification is contained in the support.

Source context 13 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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance absoluteRadicalReciprocityTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance absoluteRadicalReciprocityDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance absoluteRadicalReciprocityValuative (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance absoluteRadicalReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance absoluteRadicalReciprocityModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) :=
  continuousH1ZModModule
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
Lean source · full declaration
theorem absoluteCharacter_finiteSupport_radical_annihilator
    (hpOdd : Odd (n : ℕ)) (S : Finset (HeightOneSpectrum (𝓞 F)))
    (houtside : ∀ v : HeightOneSpectrum (𝓞 F), v ∉ S →
      ∀ sigma : finitePlaceAbsoluteInertiaSubgroup F v,
        chi (finitePlaceAbsoluteDecompositionInclusion F v sigma.1) = 1) :
    absolutePowerClassDualRestriction F (n : ℕ)
      (finiteSupportLocalReciprocityPowerClassFunctional F (n : ℕ) S
        (fun v => finitePlaceAbsoluteH1AdicRestriction
          F (n : ℕ) v.1 (Additive.ofMul chi))) = 0 := by
  ext x
  change finiteSupportLocalReciprocityPowerClassFunctional F (n : ℕ) S
    (fun v => finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v.1 (Additive.ofMul chi))
    (idealPowerRadicalToAbsolutePowerClassLinearMap F (n : ℕ) x) = 0
  obtain ⟨a, ha⟩ := QuotientGroup.mk_surjective (Additive.toMul x)
  have hx : Additive.ofMul (QuotientGroup.mk a) = x := congrArg Additive.ofMul ha
  rw [← hx]
  let qa : absolutePowerClassModP F (n : ℕ) :=
    Additive.ofMul
      (QuotientGroup.mk' (powMonoidHom (n : ℕ) : Fˣ →* Fˣ).range a.1)
  change finiteSupportLocalReciprocityPowerClassFunctional F (n : ℕ) S
    (fun v => finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v.1 (Additive.ofMul chi))
    qa = 0
  have hprincipal :
      (finiteSupportLocalReciprocityIdeleCharacter F (n : ℕ) S
        (fun v => finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v.1 (Additive.ofMul chi))
        (IdeleGroup.principalIdele F a.1)).toAdd =
        finiteSupportLocalReciprocityPowerClassFunctional F (n : ℕ) S
          (fun v => finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v.1 (Additive.ofMul chi))
          qa :=
    finiteSupportLocalReciprocityIdeleCharacter_principal_functional
      F (n : ℕ) S
        (fun v => finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v.1 (Additive.ofMul chi))
        a.1
  rw [← hprincipal]
  have hprod := principalTrivialIdeleCharacter_finite_product_radical F n hpOdd S
    (globalReciprocityIdeleCharacter F (n : ℕ) chi)
    (globalReciprocityIdeleCharacter_principal F (n : ℕ) chi)
    (fun v hv a ha => globalReciprocityIdeleCharacter_integral_eq_one_of_inertia
      F n chi v (houtside v hv) a ha) a
  have heq : finiteSupportLocalReciprocityIdeleCharacter F (n : ℕ) S
      (fun v => finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v.1 (Additive.ofMul chi))
      (IdeleGroup.principalIdele F a.1) = 1 := by
    rw [finiteSupportLocalReciprocityIdeleCharacter_apply]
    convert hprod using 1
    apply Finset.prod_congr rfl
    intro v _
    rw [localReciprocityUnitCharacter_absoluteCharacter]
    rfl
  exact congrArg Multiplicative.toAdd heq

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