NYLL
Module

LocalReciprocityCharacterFixedField.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalReciprocityCharacterFixedField
13 declarations indexed from sourceView source ↗

Module documentation

The finite local field cut out by a mod-p character

The finite abelian field is constructed from the character's actual open kernel. Its finite character recovers absolute Artin evaluation, and inertia-triviality puts inertia in the field's fixing subgroup.

Imports3
Imported by2

Declarations

instance

localReciprocityFixedFieldTopology

L31 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityFixedFieldTopology
Source context 6 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p)
instance

localReciprocityFixedFieldDiscreteTopology

L32 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityFixedFieldDiscreteTopology
Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p)
instance

localReciprocityFixedFieldH1Module

L34 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityFixedFieldH1Module
Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

localReciprocitySeparableAbelianCharacter

L39 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocitySeparableAbelianCharacter
Documentation

The absolute character in the separable-closure abelianization model.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
Lean source · statement
def localReciprocitySeparableAbelianCharacter
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    localAbsoluteAbelianProfinite K →ₜ* Multiplicative (ZMod p)
theorem

localReciprocitySeparableAbelianCharacter_mk

L48 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocitySeparableAbelianCharacter_mk
Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem localReciprocitySeparableAbelianCharacter_mk
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K))
    (sigma : Gal(SeparableClosure K/K)) :
    localReciprocitySeparableAbelianCharacter K p chi (QuotientGroup.mk sigma) =
      Multiplicative.ofAdd
        (localStandardH1LinearEquivSeparable p K chi (Additive.ofMul sigma))
def

localReciprocityCharacterKernel

L56 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityCharacterKernel
Documentation

The actual open kernel of the finite-valued abelian character.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
Lean source · full declaration
def localReciprocityCharacterKernel
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    OpenNormalSubgroup (localAbsoluteAbelianProfinite K) where
  toSubgroup := (localReciprocitySeparableAbelianCharacter K p chi).toMonoidHom.ker
  isOpen' := (isOpen_discrete {1}).preimage
    (localReciprocitySeparableAbelianCharacter K p chi).continuous_toFun
  isNormal' := MonoidHom.normal_ker _
abbrev

localReciprocityCharacterField

L65 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityCharacterField
Documentation

The finite abelian extension cut out by the given local character.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
Lean source · statement
abbrev localReciprocityCharacterField
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    IntermediateField K (SeparableClosure K)
def

localReciprocityFiniteCharacter

L71 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityFiniteCharacter
Documentation

The faithful character on the actual finite Galois group.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
Lean source · statement
def localReciprocityFiniteCharacter
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) :
    Gal(localReciprocityCharacterField K p chi / K) →* Multiplicative (ZMod p)
theorem

localReciprocityFiniteCharacter_restriction

L81 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityFiniteCharacter_restriction
Documentation

The finite character agrees with the original character after restriction.

Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem localReciprocityFiniteCharacter_restriction
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K))
    (x : localAbsoluteAbelianProfinite K) :
    localReciprocityFiniteCharacter K p chi
        (absoluteAbelianRestriction K (localReciprocityCharacterField K p chi) x) =
      localReciprocitySeparableAbelianCharacter K p chi x
theorem

localReciprocityFiniteCharacter_artin

L102 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityFiniteCharacter_artin
Documentation

Actual finite Artin evaluation recovers the power-class pairing.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localReciprocityFiniteCharacter_artin
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K)) (a : Kˣ) :
    (localReciprocityFiniteCharacter K p chi
        (abelianLocalArtinMap K (localReciprocityCharacterField K p chi) a)).toAdd =
      localReciprocityH1PowerClassPairing K p chi
        (Additive.ofMul (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a))
theorem

absoluteFiniteQuotientField_fixingSubgroup

L113 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteFiniteQuotientField_fixingSubgroup
Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem absoluteFiniteQuotientField_fixingSubgroup
    (N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
    (absoluteFiniteQuotientField K N).fixingSubgroup =
      (absoluteFiniteQuotientPreimage K N).toSubgroup
theorem

localIntrinsicUnramifiedH1_apply_inertia

L119 ↗
ClassFieldTower.Martinet.Shafarevich.localIntrinsicUnramifiedH1_apply_inertia
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localIntrinsicUnramifiedH1_apply_inertia
    (psi : ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K/K)))
    (hpsi : psi ∈ localIntrinsicUnramifiedH1 K p)
    (sigma : localIntrinsicInertiaSubgroup K) :
    psi (Additive.ofMul sigma.1) = 0
theorem

localReciprocityCharacterField_inertia_le

L130 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityCharacterField_inertia_le
Documentation

An inertia-trivial character cuts out an inertia-fixed finite field.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localReciprocityFixedFieldTopology : TopologicalSpace (ZMod p) := ⊥
local instance localReciprocityFixedFieldDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localReciprocityFixedFieldH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localReciprocityCharacterField_inertia_le
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K))
    (hchi : localStandardH1LinearEquivSeparable p K chi ∈
      localIntrinsicUnramifiedH1 K p) :
    MonoidHom.ker (localResidueDegree K).toMonoidHom ≤
      (localReciprocityCharacterField K p chi).fixingSubgroup

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