Module

GlobalReciprocityCharacter.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.GlobalReciprocityCharacter

8 declarations indexed from sourceView source ↗

Module documentation

Global reciprocity for an absolute finite character

An absolute character factors through the actual maximal abelian subextension. Pulling that character back by global Artin gives a principal-trivial idele character. This direction is used to compare choices of global central lifts.

Imports3

Imported by6

instance

globalReciprocityCharacterTopology

L27 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityCharacterTopology

Source context 5 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]

Lean source · statement

instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p)

instance

globalReciprocityCharacterDiscrete

L28 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityCharacterDiscrete

Source context 6 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]
local instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥

Lean source · statement

instance globalReciprocityCharacterDiscrete : DiscreteTopology (ZMod p)

def

globalReciprocityMaximalAbelianCharacter

L34 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityMaximalAbelianCharacter

Documentation

Descent of a continuous absolute character to the maximal abelian Galois group.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]
local instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance globalReciprocityCharacterDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))

Lean source · statement

def globalReciprocityMaximalAbelianCharacter :
    Gal(maximalAbelianExtension F / F) →ₜ* Multiplicative (ZMod p)

theorem

globalReciprocityMaximalAbelianCharacter_restriction

L45 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityMaximalAbelianCharacter_restriction

Documentation

Restriction recovers the original character, not merely its kernel.

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]
local instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance globalReciprocityCharacterDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))

Lean source · statement

theorem globalReciprocityMaximalAbelianCharacter_restriction
    (sigma : Field.absoluteGaloisGroup F) :
    globalReciprocityMaximalAbelianCharacter F p chi
      (globalMaximalAbelianRestriction F sigma) = chi sigma

theorem

globalReciprocityMaximalAbelianCharacter_comp_restriction

L60 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityMaximalAbelianCharacter_comp_restriction

Source context 8 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]
local instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance globalReciprocityCharacterDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))

Lean source · statement

theorem globalReciprocityMaximalAbelianCharacter_comp_restriction :
    (globalReciprocityMaximalAbelianCharacter F p chi).comp
      (globalMaximalAbelianRestriction F) = chi

def

globalReciprocityIdeleCharacter

L69 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityIdeleCharacter

Documentation

The actual idele character associated with an absolute character.

Source context 9 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]
local instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance globalReciprocityCharacterDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
variable [NumberField F]

Lean source · statement

def globalReciprocityIdeleCharacter : IdeleGroup F →ₜ* Multiplicative (ZMod p)

theorem

globalReciprocityIdeleCharacter_apply

L76 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityIdeleCharacter_apply

Source context 9 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]
local instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance globalReciprocityCharacterDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
variable [NumberField F]

Lean source · statement

theorem globalReciprocityIdeleCharacter_apply (a : IdeleGroup F) :
    globalReciprocityIdeleCharacter F p chi a =
      globalReciprocityMaximalAbelianCharacter F p chi
        (maximalAbelianGlobalArtin F
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup F) a))

theorem

globalReciprocityIdeleCharacter_principal

L83 ↗

ClassFieldTower.Martinet.Shafarevich.globalReciprocityIdeleCharacter_principal

Documentation

Global reciprocity is trivial on every principal idele.

Source context 9 commands

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

open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] (p : ℕ) [Fact p.Prime]
local instance globalReciprocityCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance globalReciprocityCharacterDiscrete : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
variable [NumberField F]

Lean source · statement

theorem globalReciprocityIdeleCharacter_principal (a : Fˣ) :
    globalReciprocityIdeleCharacter F p chi (IdeleGroup.principalIdele F a) = 1

Module documentation

Global reciprocity for an absolute finite character

Declarations