NYLL
Module

IdealPowerRadicalAbsoluteKummerLinear.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadicalAbsoluteKummerLinear
10 declarations indexed from sourceView source ↗

Module documentation

Linear ideal-power radical Kummer characters

For a number field containing the p-th roots of unity, the ideal-power radical embeds canonically into the continuous absolute mod-p character module. Dualizing this inclusion gives the corresponding surjective restriction map on linear duals.

Imports3
Imported by4

Declarations

instance

idealPowerRadicalLinearCharacterTopology

L30 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalLinearCharacterTopology
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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p))
instance

idealPowerRadicalLinearCharacterDiscreteTopology

L33 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalLinearCharacterDiscreteTopology
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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
Lean source · statement
instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p))
def

idealPowerRadicalToAbsolutePowerClassLinearMap

L39 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalToAbsolutePowerClassLinearMap
Documentation

The inclusion of ideal-power radical classes into all absolute power classes, linearized over ZMod p.

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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
def idealPowerRadicalToAbsolutePowerClassLinearMap :
    idealPowerRadicalModP K p →ₗ[ZMod p]
      absolutePowerClassModP K p
theorem

idealPowerRadicalToAbsolutePowerClassLinearMap_apply

L71 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalToAbsolutePowerClassLinearMap_apply
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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealPowerRadicalToAbsolutePowerClassLinearMap_apply
    (x : idealPowerRadicalModP K p) :
    idealPowerRadicalToAbsolutePowerClassLinearMap K p x =
      Additive.ofMul
        (emptySupportSelmerToAbsolutePowerClass K
          (p.toPNat (Fact.out : p.Prime).pos)
          (idealNthPowerRadicalQuotientEquivEmptySelmer K
            (p.toPNat (Fact.out : p.Prime).pos) (Additive.toMul x)))
theorem

idealPowerRadicalToAbsolutePowerClassLinearMap_injective

L82 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalToAbsolutePowerClassLinearMap_injective
Documentation

The ideal-power radical inclusion into all absolute power classes is injective.

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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealPowerRadicalToAbsolutePowerClassLinearMap_injective :
    Function.Injective
      (idealPowerRadicalToAbsolutePowerClassLinearMap K p)
def

idealPowerRadicalToAbsoluteKummerLinearMap

L106 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalToAbsoluteKummerLinearMap
Documentation

The ideal-power radical as a linear subspace of continuous absolute mod-p characters.

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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
def idealPowerRadicalToAbsoluteKummerLinearMap
    (hmu : (primitiveRoots p K).Nonempty) :
    idealPowerRadicalModP K p →ₗ[ZMod p]
      absoluteContinuousZModCharacterModP K p
theorem

idealPowerRadicalToAbsoluteKummerLinearMap_apply

L114 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalToAbsoluteKummerLinearMap_apply
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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealPowerRadicalToAbsoluteKummerLinearMap_apply
    (hmu : (primitiveRoots p K).Nonempty)
    (x : idealPowerRadicalModP K p) :
    Additive.toMul (idealPowerRadicalToAbsoluteKummerLinearMap K p hmu x) =
      idealNthPowerRadicalQuotientToAbsoluteKummerCharacter K
        (p.toPNat (Fact.out : p.Prime).pos) hmu (Additive.toMul x)
theorem

idealPowerRadicalToAbsoluteKummerLinearMap_injective

L123 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalToAbsoluteKummerLinearMap_injective
Documentation

The linearized absolute Kummer map on the ideal-power radical is injective.

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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealPowerRadicalToAbsoluteKummerLinearMap_injective
    (hmu : (primitiveRoots p K).Nonempty) :
    Function.Injective
      (idealPowerRadicalToAbsoluteKummerLinearMap K p hmu)
def

absoluteKummerDualRestriction

L131 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerDualRestriction
Documentation

Restriction of linear functionals along the ideal-radical Kummer inclusion.

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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
def absoluteKummerDualRestriction
    (hmu : (primitiveRoots p K).Nonempty) :
    Module.Dual (ZMod p) (absoluteContinuousZModCharacterModP K p) →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP K p)
theorem

absoluteKummerDualRestriction_surjective

L138 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerDualRestriction_surjective
Documentation

Every functional on the ideal-power radical extends to the absolute character module.

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] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
local instance idealPowerRadicalLinearCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance idealPowerRadicalLinearCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
theorem absoluteKummerDualRestriction_surjective
    (hmu : (primitiveRoots p K).Nonempty) :
    Function.Surjective (absoluteKummerDualRestriction K p hmu)

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