Module

AbsoluteKummerH1Linear.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.AbsoluteKummerH1Linear

7 declarations indexed from sourceView source ↗

Module documentation

Linear absolute Kummer characters

For a prime p, the absolute Kummer equivalence is linear after giving both power classes and continuous mod-p characters their canonical exponent-p ZMod p-module structures.

Imports2

Imported by9

instance

absoluteKummerLinearCharacterTopology

L28 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerLinearCharacterTopology

Source context 6 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

instance absoluteKummerLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p))

instance

absoluteKummerLinearCharacterDiscreteTopology

L30 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerLinearCharacterDiscreteTopology

Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
local instance absoluteKummerLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥

Lean source · statement

instance absoluteKummerLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p))

theorem

absolutePowerClassQuotient_pow_eq_one

L36 ↗

ClassFieldTower.Martinet.Shafarevich.absolutePowerClassQuotient_pow_eq_one

Documentation

Every absolute power class modulo p-th powers has exponent dividing p.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
local instance absoluteKummerLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance absoluteKummerLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
omit [Fact p.Prime] in

Lean source · statement

theorem absolutePowerClassQuotient_pow_eq_one
    (x : Kˣ ⧸ (powMonoidHom p : Kˣ →* Kˣ).range) :
    x ^ p = 1

theorem

absoluteContinuousZModCharacter_pow_eq_one

L45 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteContinuousZModCharacter_pow_eq_one

Documentation

Every continuous absolute mod-p character has exponent dividing p.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
local instance absoluteKummerLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance absoluteKummerLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
omit [Fact p.Prime] in

Lean source · statement

theorem absoluteContinuousZModCharacter_pow_eq_one
    (x : Field.absoluteGaloisGroup K →ₜ* Multiplicative (ZMod p)) :
    x ^ p = 1

def

absolutePowerClassModP

L57 ↗

ClassFieldTower.Martinet.Shafarevich.absolutePowerClassModP

Documentation

The power-class group as its canonical ZMod p-module object.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
local instance absoluteKummerLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance absoluteKummerLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _

Lean source · statement

def absolutePowerClassModP : ModuleCat (ZMod p)

def

absoluteContinuousZModCharacterModP

L66 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteContinuousZModCharacterModP

Documentation

Continuous absolute mod-p characters as their canonical ZMod p-module object.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
local instance absoluteKummerLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance absoluteKummerLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _

Lean source · statement

def absoluteContinuousZModCharacterModP : ModuleCat (ZMod p)

def

absoluteKummerContinuousZModCharacterLinearEquiv

L77 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerContinuousZModCharacterLinearEquiv

Documentation

The absolute Kummer equivalence, upgraded to a ZMod p-linear equivalence.

Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
variable (p : ℕ) [Fact p.Prime]
local instance absoluteKummerLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance absoluteKummerLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _

Lean source · statement

def absoluteKummerContinuousZModCharacterLinearEquiv
    [CharZero K]
    (hmu : (primitiveRoots p K).Nonempty) :
    absolutePowerClassModP K p ≃ₗ[ZMod p]
      absoluteContinuousZModCharacterModP K p

Module documentation

Linear absolute Kummer characters

Declarations

absoluteKummerLinearCharacterTopology

absoluteKummerLinearCharacterDiscreteTopology

absolutePowerClassQuotient_pow_eq_one

absoluteContinuousZModCharacter_pow_eq_one

absolutePowerClassModP

absoluteContinuousZModCharacterModP

absoluteKummerContinuousZModCharacterLinearEquiv