NYLL
Module

IdeleCharacterGlobalLift.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.IdeleCharacterGlobalLift
11 declarations indexed from sourceView source ↗

Module documentation

Lifting an idele character to an absolute Galois character

A continuous finite-valued idele character trivial on principal ideles descends first to the idele class group and then to its component quotient. Actual global reciprocity identifies that quotient with the maximal abelian Galois group. Restriction from the absolute Galois group therefore gives a genuine continuous degree-one class.

Imports4
Imported by2

Declarations

instance

ideleGlobalLiftTopology

L31 ↗
ClassFieldTower.Martinet.Shafarevich.ideleGlobalLiftTopology
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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
Lean source · statement
instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p)
instance

ideleGlobalLiftDiscreteTopology

L32 ↗
ClassFieldTower.Martinet.Shafarevich.ideleGlobalLiftDiscreteTopology
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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p)
def

ideleCharacterClassLift

L39 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterClassLift
Documentation

Descent of a principal-trivial continuous character to the actual idele class group.

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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
def ideleCharacterClassLift : IdeleClassGroup F →ₜ* Multiplicative (ZMod p)
theorem

ideleCharacterClassLift_mk

L45 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterClassLift_mk
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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
theorem ideleCharacterClassLift_mk (a : IdeleGroup F) :
    ideleCharacterClassLift F p chi hchi
      (QuotientGroup.mk' (IdeleGroup.principalSubgroup F) a) = chi a
def

ideleCharacterComponentLift

L50 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterComponentLift
Documentation

The character kills the connected component because its target is discrete.

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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
def ideleCharacterComponentLift :
    ideleClassComponentQuotient F →ₜ* Multiplicative (ZMod p)
theorem

ideleCharacterComponentLift_mk

L57 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterComponentLift_mk
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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
theorem ideleCharacterComponentLift_mk (c : IdeleClassGroup F) :
    ideleCharacterComponentLift F p chi hchi
      (QuotientGroup.mk' (ideleClassIdentityComponent F) c) =
      ideleCharacterClassLift F p chi hchi c
def

ideleCharacterMaximalAbelianLift

L63 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterMaximalAbelianLift
Documentation

The character transported through the actual component-quotient reciprocity isomorphism.

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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
def ideleCharacterMaximalAbelianLift :
    Gal(maximalAbelianExtension F / F) →ₜ* Multiplicative (ZMod p)
theorem

ideleCharacterMaximalAbelianLift_artin

L70 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterMaximalAbelianLift_artin
Documentation

Reciprocity sends an idele class back to the value of its descended 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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
theorem ideleCharacterMaximalAbelianLift_artin (c : IdeleClassGroup F) :
    ideleCharacterMaximalAbelianLift F p chi hchi (maximalAbelianGlobalArtin F c) =
      ideleCharacterClassLift F p chi hchi c
def

ideleCharacterGlobalLift

L81 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterGlobalLift
Documentation

A principal-trivial idele character gives an actual absolute Galois 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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
def ideleCharacterGlobalLift :
    Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p)
def

ideleCharacterGlobalH1

L86 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterGlobalH1
Documentation

The resulting continuous degree-one class of the absolute Galois group.

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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
def ideleCharacterGlobalH1 : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup F)
theorem

ideleCharacterGlobalH1_character

L90 ↗
ClassFieldTower.Martinet.Shafarevich.ideleCharacterGlobalH1_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 ClassFieldTower.ProP GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F] (p : ℕ) [Fact p.Prime]
local instance ideleGlobalLiftTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleGlobalLiftDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
variable (chi : IdeleGroup F →ₜ* Multiplicative (ZMod p))
variable (hchi : ∀ a : Fˣ, chi (IdeleGroup.principalIdele F a) = 1)
Lean source · statement
theorem ideleCharacterGlobalH1_character :
    characterOfH1 (ideleCharacterGlobalH1 F p chi hchi) =
      ideleCharacterGlobalLift F p chi hchi

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