NYLL
Module

IdeleFiniteValuationCharacters.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdeleFiniteValuationCharacters
13 declarations indexed from sourceView source ↗

Module documentation

Characters of the finite valuation vector of an idele

Any algebraic functional on the product of mod-p valuation defects gives a continuous idele character. No continuity of the functional on that product is required: its composite vanishes on the open subgroup of ideles integral at every finite place. On principal ideles the character agrees with the dual of global finite-valuation localization.

Imports3
Imported by2

Declarations

def

ideleFiniteValuationDefectHom

L31 ↗
ClassFieldTower.Martinet.Shafarevich.ideleFiniteValuationDefectHom
Documentation

All mod-p finite valuations of an idele, with the same sign as global valuations.

Source context 5 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
Lean source · statement
def ideleFiniteValuationDefectHom : IdeleGroup K →* FiniteValuationDefect K p
theorem

ideleFiniteValuationDefectHom_eq_one_of_supportedAt_empty

L37 ↗
ClassFieldTower.Martinet.Shafarevich.ideleFiniteValuationDefectHom_eq_one_of_supportedAt_empty
Documentation

Integral ideles have zero finite-valuation defect.

Source context 5 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
Lean source · statement
theorem ideleFiniteValuationDefectHom_eq_one_of_supportedAt_empty
    (a : IdeleGroup K) (ha : a ∈ IdeleGroup.supportedAt (K := K) ∅) :
    ideleFiniteValuationDefectHom K p a = 1
theorem

ideleFiniteValuationDefectHom_principalIdele

L50 ↗
ClassFieldTower.Martinet.Shafarevich.ideleFiniteValuationDefectHom_principalIdele
Documentation

The valuation defect of a principal idele is the global power-class localization.

Source context 6 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
Lean source · statement
theorem ideleFiniteValuationDefectHom_principalIdele (a : Kˣ) :
    ideleFiniteValuationDefectHom K p (principalIdele K a) =
      absolutePowerClassFiniteValuationLocalizationMonoidHom K p
        (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a)
theorem

ideleFiniteValuationDefectHom_finitePlace

L68 ↗
ClassFieldTower.Martinet.Shafarevich.ideleFiniteValuationDefectHom_finitePlace
Documentation

A one-place idele has only its own valuation coordinate.

Source context 7 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
open scoped Classical in
Lean source · statement
theorem ideleFiniteValuationDefectHom_finitePlace
    (v : HeightOneSpectrum (𝓞 K)) (a : (v.adicCompletion K)ˣ) :
    ideleFiniteValuationDefectHom K p (finitePlaceIdele v a) =
      Pi.mulSingle v (Multiplicative.ofAdd
        (-((FiniteIdeleGroup.localOrder v a).toAdd : ZMod p)))
theorem

finitePlaceIdele_mem_supportedAt_empty_of_integral

L88 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceIdele_mem_supportedAt_empty_of_integral
Documentation

An integral unit at one finite place defines an integral idele.

Source context 7 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
omit [Fact p.Prime] in
Lean source · statement
theorem finitePlaceIdele_mem_supportedAt_empty_of_integral
    (v : HeightOneSpectrum (𝓞 K)) (a : (v.adicCompletion K)ˣ)
    (ha : a ∈ (v.adicCompletionIntegers K).units) :
    finitePlaceIdele v a ∈ IdeleGroup.supportedAt (K := K) ∅
instance

ideleValuationCharacterTopology

L103 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacterTopology
Source context 6 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
Lean source · statement
instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p)
instance

ideleValuationCharacterDiscreteTopology

L105 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacterDiscreteTopology
Source context 7 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
local instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance ideleValuationCharacterDiscreteTopology : DiscreteTopology (ZMod p)
def

ideleValuationCharacterMonoidHom

L109 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacterMonoidHom
Documentation

An algebraic valuation functional, evaluated on the finite valuations of an idele.

Source context 8 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
local instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleValuationCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
def ideleValuationCharacterMonoidHom
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP K p)) :
    IdeleGroup K →* Multiplicative (ZMod p)
theorem

ideleValuationCharacterMonoidHom_eq_one_of_supportedAt_empty

L116 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacterMonoidHom_eq_one_of_supportedAt_empty
Documentation

A valuation character vanishes on ideles integral at every finite place.

Source context 8 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
local instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleValuationCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
theorem ideleValuationCharacterMonoidHom_eq_one_of_supportedAt_empty
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP K p))
    (a : IdeleGroup K) (ha : a ∈ IdeleGroup.supportedAt (K := K) ∅) :
    ideleValuationCharacterMonoidHom K p φ a = 1
theorem

ideleValuationCharacterMonoidHom_continuous

L128 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacterMonoidHom_continuous
Documentation

The open integral-idele subgroup proves continuity, without any topology on the dual.

Source context 8 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
local instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleValuationCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
theorem ideleValuationCharacterMonoidHom_continuous
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP K p)) :
    Continuous (ideleValuationCharacterMonoidHom K p φ)
def

ideleValuationCharacter

L146 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacter
Documentation

The continuous idele character furnished by a finite-valuation functional.

Source context 8 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
local instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleValuationCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
def ideleValuationCharacter
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP K p)) :
    IdeleGroup K →ₜ* Multiplicative (ZMod p)
theorem

ideleValuationCharacter_principalIdele

L153 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacter_principalIdele
Documentation

On principal ideles this is exactly the dualized global valuation map.

Source context 8 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
local instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleValuationCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
theorem ideleValuationCharacter_principalIdele
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP K p)) (a : Kˣ) :
    (ideleValuationCharacter K p φ (principalIdele K a)).toAdd =
      finiteValuationLocalizationDual K p φ
        (Additive.ofMul (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a))
theorem

ideleValuationCharacter_finitePlace_integral

L163 ↗
ClassFieldTower.Martinet.Shafarevich.ideleValuationCharacter_finitePlace_integral
Documentation

Valuation characters kill all integral local units at every finite place.

Source context 8 commands

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

open scoped NumberField WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory IdeleGroup
variable (K : Type*) [Field K] [NumberField K] (p : ℕ)
variable [Fact p.Prime]
local instance ideleValuationCharacterTopology : TopologicalSpace (ZMod p) := ⊥
local instance ideleValuationCharacterDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
theorem ideleValuationCharacter_finitePlace_integral
    (φ : Module.Dual (ZMod p) (FiniteValuationDefectModP K p))
    (v : HeightOneSpectrum (𝓞 K)) (a : (v.adicCompletion K)ˣ)
    (ha : a ∈ (v.adicCompletionIntegers K).units) :
    ideleValuationCharacter K p φ (finitePlaceIdele 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.