NYLL
Module

IdealPowerRadicalModule.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadicalModule
7 declarations indexed from sourceView source ↗

Module documentation

The ideal-power radical as a finite ZMod p-module

For a prime p, the empty-support ideal-power radical quotient has exponent dividing p. This file packages its additive presentation as the canonical ZMod p-module, proves finite-dimensionality, and records the resulting cardinality formulas. The module structure remains explicit and is not installed as a global instance.

Imports1
Imported by6

Declarations

def

idealPowerRadicalModPModule

L34 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalModPModule
Documentation

The canonical ZMod p-module structure on the additive presentation of the empty-support ideal-power radical quotient.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def idealPowerRadicalModPModule :
    Module (ZMod p)
      (Additive (IdealNthPowerRadicalQuotient F
        (p.toPNat (Fact.out : p.Prime).pos)))
def

idealPowerRadicalModP

L45 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalModP
Documentation

The empty-support ideal-power radical as a ZMod p-module object.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def idealPowerRadicalModP : ModuleCat (ZMod p)
theorem

idealPowerRadicalModP_finiteDimensional

L55 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalModP_finiteDimensional
Documentation

The ideal-power radical module is finite-dimensional.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem idealPowerRadicalModP_finiteDimensional :
    FiniteDimensional (ZMod p) (idealPowerRadicalModP F p)
theorem

card_idealPowerRadicalModP_eq_pow_finrank

L67 ↗
ClassFieldTower.Martinet.Shafarevich.card_idealPowerRadicalModP_eq_pow_finrank
Documentation

The cardinality of the radical module is p to its dimension.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem card_idealPowerRadicalModP_eq_pow_finrank :
    Nat.card (idealPowerRadicalModP F p) =
      p ^ Module.finrank (ZMod p) (idealPowerRadicalModP F p)
theorem

card_idealPowerRadicalModP

L78 ↗
ClassFieldTower.Martinet.Shafarevich.card_idealPowerRadicalModP
Documentation

The exact unit--radical--class sequence computes the cardinality of the radical module.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
theorem card_idealPowerRadicalModP :
    Nat.card (idealPowerRadicalModP F p) =
      p ^ (NumberField.InfinitePlace.nrRealPlaces F +
          NumberField.InfinitePlace.nrComplexPlaces F - 1 +
            (if (primitiveRoots p F).Nonempty then 1 else 0)) *
        Nat.card (PClassGroup F p) := by
  change Nat.card
      (IdealNthPowerRadicalQuotient F
        (p.toPNat (Fact.out : p.Prime).pos)) = _
  exact card_idealPthPowerRadicalQuotient F p Fact.out
theorem

pow_finrank_idealPowerRadicalModP

L91 ↗
ClassFieldTower.Martinet.Shafarevich.pow_finrank_idealPowerRadicalModP
Documentation

Equivalently, the arithmetic radical cardinality is p to the module dimension.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
theorem pow_finrank_idealPowerRadicalModP :
    p ^ Module.finrank (ZMod p) (idealPowerRadicalModP F p) =
      p ^ (NumberField.InfinitePlace.nrRealPlaces F +
          NumberField.InfinitePlace.nrComplexPlaces F - 1 +
            (if (primitiveRoots p F).Nonempty then 1 else 0)) *
        Nat.card (PClassGroup F p) := by
  rw [← card_idealPowerRadicalModP_eq_pow_finrank F p]
  exact card_idealPowerRadicalModP F p
theorem

idealPowerRadicalModPDual_finiteDimensional

L101 ↗
ClassFieldTower.Martinet.Shafarevich.idealPowerRadicalModPDual_finiteDimensional
Documentation

The linear dual of the ideal-power radical module is finite-dimensional.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem idealPowerRadicalModPDual_finiteDimensional :
    FiniteDimensional (ZMod p)
      (Module.Dual (ZMod p) (idealPowerRadicalModP F p))

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