Module

IdealRadicalCyclotomicModule.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealRadicalCyclotomicModule

7 declarations indexed from sourceView source ↗

Module documentation

The cyclotomic ideal radical as a `ZMod p`-module

The ideal radical over F maps onto the restricted radical generated after adjoining a primitive p-th root of unity. This file makes that quotient and the quotient map linear, then dualizes the surjection to a canonical injection into the dual of the original ideal radical.

All module structures are kept inside explicit definitions; no noncanonical global instance is installed.

Imports2

Imported by3

def

idealRadicalCyclotomicModPModule

L36 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicModPModule

Documentation

The canonical ZMod p-module structure on the cyclotomic restricted ideal-radical quotient.

Source context 6 commands

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

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

Lean source · statement

def idealRadicalCyclotomicModPModule :
    Module (ZMod p)
      (Additive
        (RestrictedRadicalQuotient (p.toPNat (Fact.out : p.Prime).pos)
          (idealRadicalCyclotomicKummerSubgroup F p Fact.out)))

def

idealRadicalCyclotomicModP

L47 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicModP

Documentation

The cyclotomic restricted ideal radical as a ZMod p-module object.

Source context 6 commands

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

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

Lean source · statement

def idealRadicalCyclotomicModP : ModuleCat (ZMod p)

def

idealRadicalQuotientToCyclotomicLinearMap

L59 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalQuotientToCyclotomicLinearMap

Documentation

The base-change map on ideal radicals, viewed linearly over ZMod p.

Source context 6 commands

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

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

Lean source · statement

def idealRadicalQuotientToCyclotomicLinearMap :
    idealPowerRadicalModP F p →ₗ[ZMod p]
      idealRadicalCyclotomicModP F p

theorem

idealRadicalQuotientToCyclotomicLinearMap_surjective

L75 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalQuotientToCyclotomicLinearMap_surjective

Documentation

The linearized base-change map is onto.

Source context 6 commands

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

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

Lean source · statement

theorem idealRadicalQuotientToCyclotomicLinearMap_surjective :
    Function.Surjective
      (idealRadicalQuotientToCyclotomicLinearMap F p)

def

idealRadicalCyclotomicDualInjection

L89 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicDualInjection

Documentation

Dualizing the cyclotomic quotient map gives a canonical linear map into the dual of the base-field ideal radical.

Source context 6 commands

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

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

Lean source · statement

def idealRadicalCyclotomicDualInjection :
    Module.Dual (ZMod p) (idealRadicalCyclotomicModP F p) →ₗ[ZMod p]
      Module.Dual (ZMod p) (idealPowerRadicalModP F p)

theorem

idealRadicalCyclotomicDualInjection_injective

L96 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicDualInjection_injective

Documentation

The dualized map is injective because the ideal-radical base-change map is surjective.

Source context 6 commands

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

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

Lean source · statement

theorem idealRadicalCyclotomicDualInjection_injective :
    Function.Injective (idealRadicalCyclotomicDualInjection F p)

theorem

idealRadicalCyclotomicModP_finiteDimensional

L102 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicModP_finiteDimensional

Documentation

The cyclotomic restricted ideal radical is finite-dimensional.

Source context 6 commands

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

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

Lean source · statement

theorem idealRadicalCyclotomicModP_finiteDimensional :
    FiniteDimensional (ZMod p) (idealRadicalCyclotomicModP F p)

Module documentation

The cyclotomic ideal radical as a ZMod p-module

Declarations

idealRadicalCyclotomicModPModule

idealRadicalCyclotomicModP

idealRadicalQuotientToCyclotomicLinearMap

idealRadicalQuotientToCyclotomicLinearMap_surjective

idealRadicalCyclotomicDualInjection

idealRadicalCyclotomicDualInjection_injective

idealRadicalCyclotomicModP_finiteDimensional

The cyclotomic ideal radical as a `ZMod p`-module