Module

PClassGroup.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.PClassGroup

6 declarations indexed from sourceView source ↗

Module documentation

The elementary `p`-class quotient

This file defines the ordinary ideal class group modulo pth powers and its canonical dimension over ZMod p when p is prime.

Imports2

Nyll.ProCGroups.ProP.FrattiniPowers
Mathlib.NumberTheory.NumberField.ClassNumber

Imported by4

def

pClassPowerSubgroup

L28 ↗

ClassFieldTower.Martinet.pClassPowerSubgroup

Documentation

The subgroup of pth powers in the ordinary ideal class group.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

def pClassPowerSubgroup (p : ℕ) : Subgroup (ClassGroup (𝓞 K))

instance

pClassPowerSubgroup_normal

L31 ↗

ClassFieldTower.Martinet.pClassPowerSubgroup_normal

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance pClassPowerSubgroup_normal (p : ℕ) :
    (pClassPowerSubgroup K p).Normal

abbrev

PClassGroup

L35 ↗

ClassFieldTower.Martinet.PClassGroup

Documentation

The ordinary ideal class group modulo pth powers.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type*) [Field K] [NumberField K]
local instance pClassPowerSubgroup_normal (p : ℕ) :
    (pClassPowerSubgroup K p).Normal := inferInstance

Lean source · statement

abbrev PClassGroup (p : ℕ)

theorem

pClassGroup_pow_eq_one

L40 ↗

ClassFieldTower.Martinet.pClassGroup_pow_eq_one

Documentation

Every element of the p-class quotient has exponent dividing p.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type*) [Field K] [NumberField K]
local instance pClassPowerSubgroup_normal (p : ℕ) :
    (pClassPowerSubgroup K p).Normal := inferInstance
omit [NumberField K] in

Lean source · statement

theorem pClassGroup_pow_eq_one (p : ℕ) (x : PClassGroup K p) :
    x ^ p = 1

def

pClassRank

L51 ↗

ClassFieldTower.Martinet.pClassRank

Documentation

The canonical ZMod p-dimension of the ordinary ideal class group modulo pth powers.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type*) [Field K] [NumberField K]
local instance pClassPowerSubgroup_normal (p : ℕ) :
    (pClassPowerSubgroup K p).Normal := inferInstance

Lean source · statement

def pClassRank (p : ℕ) [Fact p.Prime] : ℕ

theorem

powerSubgroup_map_mulEquiv

L60 ↗

ClassFieldTower.Martinet.powerSubgroup_map_mulEquiv

Documentation

A multiplicative equivalence carries the power subgroup onto the power subgroup.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type*) [Field K] [NumberField K]
local instance pClassPowerSubgroup_normal (p : ℕ) :
    (pClassPowerSubgroup K p).Normal := inferInstance

Lean source · statement

theorem powerSubgroup_map_mulEquiv
    {G H : Type*} [Group G] [Group H] (p : ℕ) (e : G ≃* H) :
    (powerSubgroup p G).map e.toMonoidHom = powerSubgroup p H

Module documentation

The elementary p-class quotient

Declarations

pClassPowerSubgroup

pClassPowerSubgroup_normal

PClassGroup

pClassGroup_pow_eq_one

pClassRank

powerSubgroup_map_mulEquiv

The elementary `p`-class quotient