NYLL
Module

IdealPowerRadicalAbsoluteKummer.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadicalAbsoluteKummer
16 declarations indexed from sourceView source ↗

Module documentation

Ideal-power radical classes as absolute Kummer characters

For a number field containing a primitive n-th root of unity, this file embeds the empty-support Selmer group, and hence the ideal-power radical quotient, into the continuous mod-n characters of the absolute Galois group. The image subgroup records exactly the Kummer characters satisfying the empty finite-valuation condition.

Imports2
Imported by2

Declarations

instance

idealRadicalCharacterTopology

L30 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalCharacterTopology
Source context 5 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]
Lean source · statement
instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n))
instance

idealRadicalCharacterDiscreteTopology

L33 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalCharacterDiscreteTopology
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
Lean source · statement
instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n))
def

emptySupportSelmerToAbsolutePowerClass

L39 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportSelmerToAbsolutePowerClass
Documentation

The inclusion of the empty-support Selmer group into the full group of power classes.

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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · full declaration
def emptySupportSelmerToAbsolutePowerClass (n : ℕ+) :
    EmptySupportSelmerGroup K n →*
      Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range where
  toFun x := x.1
  map_one' := rfl
  map_mul' _ _ := rfl
theorem

emptySupportSelmerToAbsolutePowerClass_injective

L46 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportSelmerToAbsolutePowerClass_injective
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem emptySupportSelmerToAbsolutePowerClass_injective (n : ℕ+) :
    Function.Injective (emptySupportSelmerToAbsolutePowerClass K n)
def

emptySupportSelmerToAbsoluteKummerCharacter

L51 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportSelmerToAbsoluteKummerCharacter
Documentation

Empty-support Selmer classes as continuous absolute Kummer characters.

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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
def emptySupportSelmerToAbsoluteKummerCharacter
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    EmptySupportSelmerGroup K n →*
      (Field.absoluteGaloisGroup K →ₜ*
        Multiplicative (ZMod (n : ℕ)))
theorem

emptySupportSelmerToAbsoluteKummerCharacter_apply

L60 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportSelmerToAbsoluteKummerCharacter_apply
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem emptySupportSelmerToAbsoluteKummerCharacter_apply
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (x : EmptySupportSelmerGroup K n) :
    emptySupportSelmerToAbsoluteKummerCharacter K n hmu x =
      absoluteKummerContinuousZModCharacterEquiv K n hmu x.1
theorem

emptySupportSelmerToAbsoluteKummerCharacter_injective

L67 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportSelmerToAbsoluteKummerCharacter_injective
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem emptySupportSelmerToAbsoluteKummerCharacter_injective
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Function.Injective
      (emptySupportSelmerToAbsoluteKummerCharacter K n hmu)
def

idealNthPowerRadicalQuotientToAbsoluteKummerCharacter

L77 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToAbsoluteKummerCharacter
Documentation

Ideal-power radical classes as continuous absolute Kummer characters.

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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
def idealNthPowerRadicalQuotientToAbsoluteKummerCharacter
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    IdealNthPowerRadicalQuotient K n →*
      (Field.absoluteGaloisGroup K →ₜ*
        Multiplicative (ZMod (n : ℕ)))
theorem

idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_apply

L86 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_apply
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_apply
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (x : IdealNthPowerRadicalQuotient K n) :
    idealNthPowerRadicalQuotientToAbsoluteKummerCharacter K n hmu x =
      emptySupportSelmerToAbsoluteKummerCharacter K n hmu
        (idealNthPowerRadicalQuotientEquivEmptySelmer K n x)
theorem

idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_mk

L95 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_mk
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_mk
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : (idealNthPowerRadicalKummerSubgroup K n).1) :
    idealNthPowerRadicalQuotientToAbsoluteKummerCharacter K n hmu
        (restrictedRadicalQuotientMk n
          (idealNthPowerRadicalKummerSubgroup K n) a) =
      absoluteKummerContinuousZModCharacterEquiv K n hmu
        (QuotientGroup.mk'
          (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range a.1)
theorem

idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_injective

L114 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_injective
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealNthPowerRadicalQuotientToAbsoluteKummerCharacter_injective
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Function.Injective
      (idealNthPowerRadicalQuotientToAbsoluteKummerCharacter K n hmu)
def

idealPowerRadicalAbsoluteKummerCharacterSubgroup

L125 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalAbsoluteKummerCharacterSubgroup
Documentation

The subgroup of absolute Kummer characters cut out by the empty-support Selmer condition.

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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
def idealPowerRadicalAbsoluteKummerCharacterSubgroup
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Subgroup
      (Field.absoluteGaloisGroup K →ₜ*
        Multiplicative (ZMod (n : ℕ)))
def

emptySupportSelmerEquivAbsoluteKummerCharacterSubgroup

L134 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportSelmerEquivAbsoluteKummerCharacterSubgroup
Documentation

The empty-support Selmer group is equivalent to its subgroup of absolute Kummer characters.

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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
def emptySupportSelmerEquivAbsoluteKummerCharacterSubgroup
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    EmptySupportSelmerGroup K n ≃*
      idealPowerRadicalAbsoluteKummerCharacterSubgroup K n hmu
theorem

emptySupportSelmerEquivAbsoluteKummerCharacterSubgroup_apply_coe

L142 ↗
ClassFieldTower.Martinet.Shafarevich.emptySupportSelmerEquivAbsoluteKummerCharacterSubgroup_apply_coe
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem emptySupportSelmerEquivAbsoluteKummerCharacterSubgroup_apply_coe
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (x : EmptySupportSelmerGroup K n) :
    (emptySupportSelmerEquivAbsoluteKummerCharacterSubgroup K n hmu x :
        Field.absoluteGaloisGroup K →ₜ*
          Multiplicative (ZMod (n : ℕ))) =
      emptySupportSelmerToAbsoluteKummerCharacter K n hmu x
def

idealNthPowerRadicalQuotientEquivAbsoluteKummerCharacterSubgroup

L153 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientEquivAbsoluteKummerCharacterSubgroup
Documentation

The ideal-power radical quotient is equivalent to the same subgroup of absolute Kummer characters.

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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
def idealNthPowerRadicalQuotientEquivAbsoluteKummerCharacterSubgroup
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    IdealNthPowerRadicalQuotient K n ≃*
      idealPowerRadicalAbsoluteKummerCharacterSubgroup K n hmu
theorem

idealNthPowerRadicalQuotientEquivAbsoluteKummerCharacterSubgroup_apply_coe

L161 ↗
ClassFieldTower.Martinet.Shafarevich.idealNthPowerRadicalQuotientEquivAbsoluteKummerCharacterSubgroup_apply_coe
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]
local instance idealRadicalCharacterTopology (n : ℕ) :
    TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance idealRadicalCharacterDiscreteTopology (n : ℕ) :
    DiscreteTopology (Multiplicative (ZMod n)) :=
  discreteTopology_bot _
Lean source · statement
theorem idealNthPowerRadicalQuotientEquivAbsoluteKummerCharacterSubgroup_apply_coe
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (x : IdealNthPowerRadicalQuotient K n) :
    (idealNthPowerRadicalQuotientEquivAbsoluteKummerCharacterSubgroup
        K n hmu x :
      Field.absoluteGaloisGroup K →ₜ*
        Multiplicative (ZMod (n : ℕ))) =
      idealNthPowerRadicalQuotientToAbsoluteKummerCharacter K n hmu x

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