NYLL
Module

FiniteSupportLocalReciprocityIdeleCharacter.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FiniteSupportLocalReciprocityIdeleCharacter
15 declarations indexed from sourceView source ↗

Module documentation

Idele characters from finitely many local reciprocity characters

A finite family of continuous local mod-p characters evaluates on actual idele coordinates. The finite product is continuous, and its value on a principal idele is the sum of the localized power-class pairings.

Imports4
Imported by8

Declarations

instance

finiteSupportReciprocityTopology

L32 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportReciprocityTopology
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]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p)
instance

finiteSupportReciprocityDiscreteTopology

L33 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportReciprocityDiscreteTopology
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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p)
instance

finiteSupportReciprocityValuativeRel

L35 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportReciprocityValuativeRel
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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F)
instance

finiteSupportReciprocityLocalField

L37 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportReciprocityLocalField
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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
Lean source · statement
instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F)
instance

finiteSupportReciprocityH1Module

L40 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportReciprocityH1Module
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
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

finiteSupportLocalReciprocityIdeleCharacter

L50 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter
Documentation

The continuous finite product of local reciprocity characters on the actual finite coordinates of an idele.

Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · full declaration
def finiteSupportLocalReciprocityIdeleCharacter :
    IdeleGroup F →ₜ* Multiplicative (ZMod p) where
  toFun x := ∏ v : ↥S, localReciprocityUnitCharacter (v.1.adicCompletion F) p (chi v)
    (IdeleGroup.finiteComponent v.1 x)
  map_one' := by simp only [map_one, Finset.prod_const_one]
  map_mul' x y := by simp only [map_mul, Finset.prod_mul_distrib]
  continuous_toFun := continuous_finsetProd Finset.univ fun v _ ↦
    (localReciprocityUnitCharacter (v.1.adicCompletion F) p (chi v)).continuous_toFun.comp
      (IdeleGroup.finiteComponentContinuous v.1).continuous_toFun
theorem

finiteSupportLocalReciprocityIdeleCharacter_apply

L61 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter_apply
Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
theorem finiteSupportLocalReciprocityIdeleCharacter_apply (x : IdeleGroup F) :
    finiteSupportLocalReciprocityIdeleCharacter F p S chi x =
      ∏ v : ↥S, localReciprocityUnitCharacter (v.1.adicCompletion F) p (chi v)
        (IdeleGroup.finiteComponent v.1 x)
def

finiteSupportLocalReciprocityPowerClassFunctional

L68 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityPowerClassFunctional
Documentation

The corresponding functional on global power classes is the finite sum of local reciprocity pairings after localization.

Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
def finiteSupportLocalReciprocityPowerClassFunctional :
    Module.Dual (ZMod p) (absolutePowerClassModP F p)
theorem

finiteSupportLocalReciprocityPowerClassFunctional_apply

L74 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityPowerClassFunctional_apply
Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
theorem finiteSupportLocalReciprocityPowerClassFunctional_apply
    (x : absolutePowerClassModP F p) :
    finiteSupportLocalReciprocityPowerClassFunctional F p S chi x =
      ∑ v : ↥S, localReciprocityH1PowerClassPairing (v.1.adicCompletion F) p (chi v)
        (finitePlacePowerClassLocalization F p v.1 x)
theorem

finiteSupportLocalReciprocityIdeleCharacter_principal

L84 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter_principal
Documentation

Principal idele evaluation is the finite sum of actual localized power-class pairings. No coefficient-root hypothesis is used.

Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
theorem finiteSupportLocalReciprocityIdeleCharacter_principal
    (a : Fˣ) :
    (finiteSupportLocalReciprocityIdeleCharacter F p S chi
      (IdeleGroup.principalIdele F a)).toAdd =
      ∑ v : ↥S, localReciprocityH1PowerClassPairing (v.1.adicCompletion F) p (chi v)
        (finitePlacePowerClassLocalization F p v.1
          (Additive.ofMul (QuotientGroup.mk' (powMonoidHom p : Fˣ →* Fˣ).range a)))
theorem

finiteSupportLocalReciprocityIdeleCharacter_principal_functional

L103 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter_principal_functional
Documentation

The principal evaluation formula as one global power-class functional.

Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
theorem finiteSupportLocalReciprocityIdeleCharacter_principal_functional
    (a : Fˣ) :
    (finiteSupportLocalReciprocityIdeleCharacter F p S chi
      (IdeleGroup.principalIdele F a)).toAdd =
      finiteSupportLocalReciprocityPowerClassFunctional F p S chi
        (Additive.ofMul (QuotientGroup.mk' (powMonoidHom p : Fˣ →* Fˣ).range a))
theorem

finiteSupportLocalReciprocityIdeleCharacter_finitePlace_mem

L121 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter_finitePlace_mem
Documentation

A supporting finite-place embedding recovers its prescribed local reciprocity character.

Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
theorem finiteSupportLocalReciprocityIdeleCharacter_finitePlace_mem
    (v : ↥S) (a : (v.1.adicCompletion F)ˣ) :
    finiteSupportLocalReciprocityIdeleCharacter F p S chi (IdeleGroup.finitePlaceIdele v.1 a) =
      localReciprocityUnitCharacter (v.1.adicCompletion F) p (chi v) a
theorem

finiteSupportLocalReciprocityIdeleCharacter_finitePlace_notMem

L134 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter_finitePlace_notMem
Documentation

Outside the finite support, every finite-place idele has value one.

Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
theorem finiteSupportLocalReciprocityIdeleCharacter_finitePlace_notMem
    (v : HeightOneSpectrum (𝓞 F)) (hv : v ∉ S) (a : (v.adicCompletion F)ˣ) :
    finiteSupportLocalReciprocityIdeleCharacter F p S chi (IdeleGroup.finitePlaceIdele v a) =
      1
theorem

finiteSupportLocalReciprocityIdeleCharacter_finitePlace

L149 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter_finitePlace
Documentation

Evaluation at an arbitrary finite-place embedding, with its actual support test.

Source context 15 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
open scoped Classical in
Lean source · full declaration
theorem finiteSupportLocalReciprocityIdeleCharacter_finitePlace
    (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ) :
    finiteSupportLocalReciprocityIdeleCharacter F p S chi (IdeleGroup.finitePlaceIdele v a) =
      if hv : v ∈ S then localReciprocityUnitCharacter (v.adicCompletion F) p (chi ⟨v, hv⟩) a
      else 1 := by
  classical
  by_cases hv : v ∈ S
  · rw [dite_eq_left hv]
    exact finiteSupportLocalReciprocityIdeleCharacter_finitePlace_mem F p S chi ⟨v, hv⟩ a
  · rw [dite_eq_right hv]
    exact finiteSupportLocalReciprocityIdeleCharacter_finitePlace_notMem F p S chi v hv a
theorem

finiteSupportLocalReciprocityIdeleCharacter_infinitePlace

L163 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportLocalReciprocityIdeleCharacter_infinitePlace
Documentation

Every archimedean-place embedding is killed by a family supported at finite places.

Source context 14 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]
variable (p : ℕ) [Fact p.Prime]
local instance finiteSupportReciprocityTopology : TopologicalSpace (ZMod p) := ⊥
local instance finiteSupportReciprocityDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance finiteSupportReciprocityValuativeRel (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finiteSupportReciprocityLocalField (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
local instance finiteSupportReciprocityH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (chi : ∀ v : ↥S, ContinuousH1ZMod (p := p)
  (G := Field.absoluteGaloisGroup (v.1.adicCompletion F)))
Lean source · statement
theorem finiteSupportLocalReciprocityIdeleCharacter_infinitePlace
    (v : InfinitePlace F) (a : v.Completionˣ) :
    finiteSupportLocalReciprocityIdeleCharacter F p S chi (IdeleGroup.infinitePlaceIdele v a) =
      1

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