Module

HilbertElementaryLayer.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.HilbertElementaryLayer

18 declarations indexed from sourceView source ↗

Module documentation

The elementary Hilbert class-field layer

This file cuts out the exponent-p layer of the small Hilbert class field and identifies its Galois group with the ordinary class group modulo pth powers. It also realizes that layer in the canonical algebraic closure and records its maximality among finite abelian everywhere-unramified exponent-p extensions.

Imports6

Imported by2

def

hilbertPSubgroup

L37 ↗

ClassFieldTower.Martinet.hilbertPSubgroup

Documentation

The subgroup cutting out the elementary abelian p layer of the small Hilbert class field.

Source context 6 commands

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

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

Lean source · statement

def hilbertPSubgroup (p : ℕ) :
    Subgroup Gal((smallHilbertClassField K) / K)

instance

hilbertPSubgroup_normal

L41 ↗

ClassFieldTower.Martinet.hilbertPSubgroup_normal

Source context 6 commands

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

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

Lean source · statement

instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal

def

hilbertElementaryLayer

L45 ↗

ClassFieldTower.Martinet.hilbertElementaryLayer

Documentation

The elementary abelian p layer inside the small Hilbert class field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

def hilbertElementaryLayer (p : ℕ) :
    IntermediateField K (smallHilbertClassField K)

theorem

hilbertElementaryLayer_isGalois

L50 ↗

ClassFieldTower.Martinet.hilbertElementaryLayer_isGalois

Documentation

The elementary Hilbert layer is Galois over its base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

theorem hilbertElementaryLayer_isGalois (p : ℕ) :
    IsGalois K (hilbertElementaryLayer K p)

instance

instIsGalois

L55 ↗

ClassFieldTower.Martinet.hilbertElementaryLayer.instIsGalois

Documentation

The canonical Galois instance for the elementary Hilbert layer.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

instance hilbertElementaryLayer.instIsGalois (p : ℕ) :
    IsGalois K (hilbertElementaryLayer K p)

theorem

hilbertElementaryLayer_isEverywhereUnramified

L61 ↗

ClassFieldTower.Martinet.hilbertElementaryLayer_isEverywhereUnramified

Documentation

The elementary Hilbert layer is everywhere unramified over its base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

theorem hilbertElementaryLayer_isEverywhereUnramified (p : ℕ) :
    IsEverywhereUnramified K (hilbertElementaryLayer K p)

def

hilbertElementaryGaloisEquivPClassGroup

L70 ↗

ClassFieldTower.Martinet.hilbertElementaryGaloisEquivPClassGroup

Documentation

Hilbert reciprocity transports the elementary layer to the ordinary p-class quotient.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

def hilbertElementaryGaloisEquivPClassGroup (p : ℕ) :
    Gal((hilbertElementaryLayer K p) / K) ≃* PClassGroup K p

theorem

hilbertElementaryGalois_pow_eq_one

L87 ↗

ClassFieldTower.Martinet.hilbertElementaryGalois_pow_eq_one

Documentation

Every automorphism of the elementary Hilbert layer has exponent dividing p.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

theorem hilbertElementaryGalois_pow_eq_one (p : ℕ)
    (x : Gal((hilbertElementaryLayer K p)/K)) : x ^ p = 1

theorem

finrank_hilbertElementaryGalois_eq_pClassRank

L97 ↗

ClassFieldTower.Martinet.finrank_hilbertElementaryGalois_eq_pClassRank

Documentation

The Galois rank of the elementary Hilbert layer is the p-class rank.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · full declaration

theorem finrank_hilbertElementaryGalois_eq_pClassRank
    (p : ℕ) [Fact (Nat.Prime p)] :
    letI : Module (ZMod p)
        (Additive Gal((hilbertElementaryLayer K p) / K)) :=
      AddCommGroup.zmodModule (fun x => by
        change (Additive.toMul x) ^ p = 1
        exact hilbertElementaryGalois_pow_eq_one K p (Additive.toMul x))
    Module.finrank (ZMod p)
        (Additive Gal((hilbertElementaryLayer K p) / K)) = pClassRank K p := by
  let : Module (ZMod p) (Additive (PClassGroup K p)) :=
    AddCommGroup.zmodModule (fun x => by
      change (Additive.toMul x) ^ p = 1
      exact pClassGroup_pow_eq_one K p (Additive.toMul x))
  let : Module (ZMod p)
      (Additive Gal((hilbertElementaryLayer K p) / K)) :=
    AddCommGroup.zmodModule (fun x => by
      change (Additive.toMul x) ^ p = 1
      exact hilbertElementaryGalois_pow_eq_one K p (Additive.toMul x))
  let e : Additive Gal((hilbertElementaryLayer K p) / K) ≃+
      Additive (PClassGroup K p) :=
    (hilbertElementaryGaloisEquivPClassGroup K p).toAdditive
  let eLin : Additive Gal((hilbertElementaryLayer K p) / K) ≃ₗ[ZMod p]
      Additive (PClassGroup K p) :=
    LinearEquiv.ofBijective (e.toAddMonoidHom.toZModLinearMap p) e.bijective
  exact eLin.finrank_eq

def

hilbertElementaryLayerEmbedding

L125 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerEmbedding

Documentation

A chosen realization of the Hilbert elementary layer in the canonical algebraic closure.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

def hilbertElementaryLayerEmbedding (p : ℕ) :
    hilbertElementaryLayer K p →ₐ[K] AlgebraicClosure K

def

hilbertElementaryLayerInAlgebraicClosure

L130 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInAlgebraicClosure

Documentation

The realized Hilbert elementary layer in AlgebraicClosure K.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

def hilbertElementaryLayerInAlgebraicClosure (p : ℕ) :
    IntermediateField K (AlgebraicClosure K)

def

hilbertElementaryLayerEquivInAlgebraicClosure

L136 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerEquivInAlgebraicClosure

Documentation

The abstract and realized elementary Hilbert layers are equivalent over K.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

def hilbertElementaryLayerEquivInAlgebraicClosure (p : ℕ) :
    hilbertElementaryLayer K p ≃ₐ[K]
      hilbertElementaryLayerInAlgebraicClosure K p

instance

instFiniteDimensional

L143 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInAlgebraicClosure.instFiniteDimensional

Documentation

The realized elementary Hilbert layer is finite-dimensional over its base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

instance hilbertElementaryLayerInAlgebraicClosure.instFiniteDimensional
    (p : ℕ) :
    FiniteDimensional K
      (hilbertElementaryLayerInAlgebraicClosure K p)

instance

instNumberField

L150 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInAlgebraicClosure.instNumberField

Documentation

The realized elementary Hilbert layer is a number field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

instance hilbertElementaryLayerInAlgebraicClosure.instNumberField
    (p : ℕ) :
    NumberField (hilbertElementaryLayerInAlgebraicClosure K p)

instance

instIsGalois

L157 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInAlgebraicClosure.instIsGalois

Documentation

The realized elementary Hilbert layer is Galois over its base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

instance hilbertElementaryLayerInAlgebraicClosure.instIsGalois
    (p : ℕ) :
    IsGalois K (hilbertElementaryLayerInAlgebraicClosure K p)

instance

instIsAbelianGalois

L165 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInAlgebraicClosure.instIsAbelianGalois

Documentation

The realized elementary Hilbert layer is abelian Galois over its base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

instance hilbertElementaryLayerInAlgebraicClosure.instIsAbelianGalois
    (p : ℕ) :
    IsAbelianGalois K
      (hilbertElementaryLayerInAlgebraicClosure K p)

theorem

hilbertElementaryLayerInAlgebraicClosure_isEverywhereUnramified

L174 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInAlgebraicClosure_isEverywhereUnramified

Documentation

The realized elementary Hilbert layer is everywhere unramified over its base field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

theorem hilbertElementaryLayerInAlgebraicClosure_isEverywhereUnramified
    (p : ℕ) :
    IsEverywhereUnramified K
      (hilbertElementaryLayerInAlgebraicClosure K p)

theorem

finiteElementaryUnramified_le_hilbertElementaryLayer

L184 ↗

ClassFieldTower.Martinet.finiteElementaryUnramified_le_hilbertElementaryLayer

Documentation

Every finite abelian everywhere-unramified exponent-p subfield of the canonical algebraic closure lies in the realized Hilbert elementary layer.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
variable (K : Type) [Field K] [NumberField K]
local instance hilbertPSubgroup_normal (p : ℕ) :
    (hilbertPSubgroup K p).Normal := inferInstance

Lean source · statement

theorem finiteElementaryUnramified_le_hilbertElementaryLayer
    (p : ℕ)
    (L : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K L] [IsAbelianGalois K L] [NumberField L]
    (hL : IsEverywhereUnramified K L)
    (hExp : ∀ σ : Gal(L / K), σ ^ p = 1) :
    L ≤ hilbertElementaryLayerInAlgebraicClosure K p

Module documentation

The elementary Hilbert class-field layer

Declarations