The arithmetic obstruction space used in the Shafarevich relation-rank argument has two finite pieces: an S-unit Kummer quotient and the elementary ideal class quotient. This file packages those pieces as one finite-dimensional ZMod p-module without installing noncanonical global module instances.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]def pPositive : ℕ+The Kummer and ideal-class parameter space attached to a finite set of finite places.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]def kummerClassParameter
(S : Finset (HeightOneSpectrum (𝓞 F))) : ModuleCat (ZMod p)The Kummer/class-group parameter is finite-dimensional over ZMod p.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open KummerTheory
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]theorem kummerClassParameter_finiteDimensional
(S : Finset (HeightOneSpectrum (𝓞 F))) :
FiniteDimensional (ZMod p) (kummerClassParameter F p S)