NYLL
Module

FinitePlaceH1CharacterLocalization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FinitePlaceH1CharacterLocalization
11 declarations indexed from sourceView source ↗

Module documentation

Finite-place restriction of absolute mod-p characters

Continuous mod-p characters of the absolute Galois group restrict to the absolute decomposition subgroup at every finite place. This file linearizes each restriction and assembles all of them into a dependent product.

Imports4
Imported by2

Declarations

instance

finitePlaceH1CharacterTopology

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

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p))
instance

finitePlaceH1CharacterDiscreteTopology

L34 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1CharacterDiscreteTopology
Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
Lean source · statement
instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p))
theorem

finitePlaceDecompositionContinuousZModCharacter_pow_eq_one

L39 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionContinuousZModCharacter_pow_eq_one
Documentation

Every mod-p character of a finite-place decomposition subgroup has exponent dividing p.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
theorem finitePlaceDecompositionContinuousZModCharacter_pow_eq_one
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : finitePlaceAbsoluteDecompositionGroup F v →ₜ*
      Multiplicative (ZMod p)) :
    chi ^ p = 1
def

finitePlaceDecompositionContinuousZModCharacterModP

L53 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionContinuousZModCharacterModP
Documentation

Continuous mod-p characters of the absolute decomposition subgroup at v, with their canonical ZMod p-module structure.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
def finitePlaceDecompositionContinuousZModCharacterModP
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ModuleCat (ZMod p)
def

finitePlaceH1CharacterRestrictionAddHom

L68 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1CharacterRestrictionAddHom
Documentation

Restriction of absolute characters to the decomposition subgroup, as an additive map.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · full declaration
def finitePlaceH1CharacterRestrictionAddHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Additive
        (Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p)) →+
      Additive
        (finitePlaceAbsoluteDecompositionGroup F v →ₜ*
          Multiplicative (ZMod p)) where
  toFun chi := Additive.ofMul <|
    (Additive.toMul chi).comp (finitePlaceAbsoluteDecompositionInclusion F v)
  map_zero' := by
    apply Additive.toMul.injective
    ext sigma
    rfl
  map_add' chi psi := by
    apply Additive.toMul.injective
    ext sigma
    rfl
def

finitePlaceH1CharacterRestriction

L87 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1CharacterRestriction
Documentation

Restriction of absolute continuous mod-p characters to the decomposition subgroup at v.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
def finitePlaceH1CharacterRestriction
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      finitePlaceDecompositionContinuousZModCharacterModP F p v
theorem

finitePlaceH1CharacterRestriction_apply

L112 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1CharacterRestriction_apply
Documentation

Restriction is evaluation after the continuous decomposition-group inclusion.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · full declaration
theorem finitePlaceH1CharacterRestriction_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : absoluteContinuousZModCharacterModP F p)
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    (Additive.toMul
        (show Additive
            (finitePlaceAbsoluteDecompositionGroup F v →ₜ*
              Multiplicative (ZMod p))
          from finitePlaceH1CharacterRestriction F p v chi)) sigma =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
          from chi)) (finitePlaceAbsoluteDecompositionInclusion F v sigma) :=
  rfl
abbrev

FinitePlaceH1CharacterLocalizationTarget

L128 ↗
ClassFieldTower.Martinet.Shafarevich.FinitePlaceH1CharacterLocalizationTarget
Documentation

The dependent product of finite-place decomposition-character modules.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
abbrev FinitePlaceH1CharacterLocalizationTarget
def

finitePlaceH1CharacterRestrictionFamily

L133 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1CharacterRestrictionFamily
Documentation

Simultaneous restriction of an absolute mod-p character at every finite place.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
def finitePlaceH1CharacterRestrictionFamily :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      FinitePlaceH1CharacterLocalizationTarget F p
theorem

finitePlaceH1CharacterRestrictionFamily_apply

L140 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1CharacterRestrictionFamily_apply
Documentation

Each component of simultaneous restriction is the corresponding finite-place map.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
theorem finitePlaceH1CharacterRestrictionFamily_apply
    (chi : absoluteContinuousZModCharacterModP F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceH1CharacterRestrictionFamily F p chi v =
      finitePlaceH1CharacterRestriction F p v chi
theorem

finitePlaceH1CharacterRestrictionFamily_apply_apply

L149 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1CharacterRestrictionFamily_apply_apply
Documentation

Evaluation of a component is ordinary character restriction.

Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1CharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1CharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · full declaration
theorem finitePlaceH1CharacterRestrictionFamily_apply_apply
    (chi : absoluteContinuousZModCharacterModP F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    (Additive.toMul
        (show Additive
            (finitePlaceAbsoluteDecompositionGroup F v →ₜ*
              Multiplicative (ZMod p))
          from finitePlaceH1CharacterRestrictionFamily F p chi v)) sigma =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
          from chi)) (finitePlaceAbsoluteDecompositionInclusion F v sigma) :=
  rfl

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