NYLL
Module

IdealRadicalGoverningFieldLinearDuality.lean

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

Module documentation

Linear Kummer duality for the ideal-radical governing field

The Kummer character isomorphism for the governing extension is linearized over ZMod p. Thus every governing automorphism gives a functional on the cyclotomic restricted ideal radical, and the resulting linear map is faithful.

Imports3
Imported by2

Declarations

instance

idealRadicalGoverningFieldZModAddCommGroup

L30 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldZModAddCommGroup
Source context 6 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p)
instance

(anonymous instance)

L33 ↗
Source context 7 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out)
abbrev

IdealRadicalGoverningGalois

L39 ↗
ClassFieldTower.Martinet.Shafarevich.IdealRadicalGoverningGalois
Documentation

The Galois group of the ideal-radical governing extension.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
abbrev IdealRadicalGoverningGalois
abbrev

IdealRadicalCyclotomicRestrictedQuotient

L44 ↗
ClassFieldTower.Martinet.Shafarevich.IdealRadicalCyclotomicRestrictedQuotient
Documentation

The restricted radical paired with the ideal-radical governing group.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
abbrev IdealRadicalCyclotomicRestrictedQuotient
theorem

idealRadicalGoverningField_primitiveRoots_nonempty

L48 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningField_primitiveRoots_nonempty
Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem idealRadicalGoverningField_primitiveRoots_nonempty :
    (primitiveRoots p (IdealRadicalGoverningField F p Fact.out)).Nonempty
def

idealRadicalGoverningFieldPairingZMod

L61 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldPairingZMod
Documentation

The governing-field Kummer pairing with its root-of-unity values written in ZMod p.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def idealRadicalGoverningFieldPairingZMod :
    IdealRadicalGoverningGalois F p →*
      (IdealRadicalCyclotomicRestrictedQuotient F p →*
        Multiplicative (ZMod p))
def

idealRadicalGoverningGaloisModPModule

L91 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningGaloisModPModule
Documentation

The exponent-p governing Galois group as a ZMod p-module.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def idealRadicalGoverningGaloisModPModule :
    Module (ZMod p) (Additive (IdealRadicalGoverningGalois F p))
def

idealRadicalGoverningGaloisModP

L97 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningGaloisModP
Documentation

The exponent-p governing Galois group as a module object.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def idealRadicalGoverningGaloisModP : ModuleCat (ZMod p)
def

idealRadicalGoverningFieldLinearFunctional

L104 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldLinearFunctional
Documentation

Evaluation of a governing automorphism on the restricted radical, in ZMod p coordinates.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def idealRadicalGoverningFieldLinearFunctional
    (sigma : idealRadicalGoverningGaloisModP (F := F) p) :
    Module.Dual (ZMod p) (idealRadicalCyclotomicModP F p)
def

idealRadicalGoverningFieldLinearDuality

L115 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldLinearDuality
Documentation

Kummer character duality, linearized over ZMod p.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
def idealRadicalGoverningFieldLinearDuality :
    idealRadicalGoverningGaloisModP (F := F) p →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealRadicalCyclotomicModP F p)
theorem

idealRadicalGoverningFieldLinearDuality_apply

L151 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldLinearDuality_apply
Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem idealRadicalGoverningFieldLinearDuality_apply
    (sigma : idealRadicalGoverningGaloisModP (F := F) p)
    (q : idealRadicalCyclotomicModP F p) :
    idealRadicalGoverningFieldLinearDuality F p sigma q =
      (idealRadicalGoverningFieldPairingZMod F p
        (Additive.toMul sigma) (Additive.toMul q)).toAdd
theorem

idealRadicalGoverningFieldPairingZMod_injective

L161 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldPairingZMod_injective
Documentation

Root coordinates preserve the faithfulness of governing-field Kummer character duality.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem idealRadicalGoverningFieldPairingZMod_injective :
    Function.Injective (idealRadicalGoverningFieldPairingZMod F p)
theorem

idealRadicalGoverningFieldLinearDuality_injective

L179 ↗
ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldLinearDuality_injective
Documentation

The linearized governing-field character map is injective.

Source context 8 commands

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

open scoped NumberField IsMulCommutative
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField KummerTheory
noncomputable section
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance idealRadicalGoverningFieldZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance : IsAbelianGalois
    (IdealRadicalCyclotomicBase F p Fact.out)
    (IdealRadicalGoverningField F p Fact.out) :=
  idealRadicalGoverningField_isAbelianGalois F p Fact.out
Lean source · statement
theorem idealRadicalGoverningFieldLinearDuality_injective :
    Function.Injective (idealRadicalGoverningFieldLinearDuality F p)

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