Module

HilbertElementaryLayerInMaximal.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.HilbertElementaryLayerInMaximal

9 declarations indexed from sourceView source ↗

Module documentation

The elementary Hilbert layer inside the maximal unramified pro-p extension

This file places the realized elementary Hilbert class-field layer inside the maximal everywhere-unramified pro-p extension. It identifies the resulting intermediate field with the abstract Hilbert layer and transports its finite, abelian Galois, exponent, and rank data.

Imports2

Imported by2

theorem

hilbertElementaryLayerInAlgebraicClosure_le_maximal

L31 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInAlgebraicClosure_le_maximal

Documentation

The realized elementary Hilbert layer is contained in the maximal everywhere-unramified pro-p extension.

Source context 5 commands

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

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

Lean source · statement

theorem hilbertElementaryLayerInAlgebraicClosure_le_maximal
    (p : ℕ) [Fact p.Prime] :
    hilbertElementaryLayerInAlgebraicClosure K p ≤
      maximalEverywhereUnramifiedProP K p

def

hilbertElementaryLayerInMaximal

L66 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInMaximal

Documentation

The elementary Hilbert layer, viewed inside the maximal extension.

Source context 5 commands

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

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

Lean source · statement

def hilbertElementaryLayerInMaximal
    (p : ℕ) [Fact p.Prime] :
    IntermediateField K (maximalEverywhereUnramifiedProP K p)

def

hilbertElementaryLayerEquivInMaximal

L74 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerEquivInMaximal

Documentation

The abstract Hilbert layer is equivalent to its copy inside the maximal extension.

Source context 5 commands

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

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

Lean source · statement

def hilbertElementaryLayerEquivInMaximal
    (p : ℕ) [Fact p.Prime] :
    hilbertElementaryLayer K p ≃ₐ[K]
      hilbertElementaryLayerInMaximal K p

instance

instFiniteDimensional

L92 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInMaximal.instFiniteDimensional

Documentation

Finite-dimensionality transported to the copy in the maximal extension.

Source context 5 commands

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

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

Lean source · statement

instance hilbertElementaryLayerInMaximal.instFiniteDimensional
    (p : ℕ) [Fact p.Prime] :
    FiniteDimensional K (hilbertElementaryLayerInMaximal K p)

instance

instIsGalois

L98 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInMaximal.instIsGalois

Documentation

Galoisness transported to the copy in the maximal extension.

Source context 5 commands

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

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

Lean source · statement

instance hilbertElementaryLayerInMaximal.instIsGalois
    (p : ℕ) [Fact p.Prime] :
    IsGalois K (hilbertElementaryLayerInMaximal K p)

theorem

hilbertElementaryLayerInMaximal_isAbelianGalois

L104 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInMaximal_isAbelianGalois

Documentation

The copy in the maximal extension is an abelian Galois extension.

Source context 5 commands

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

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

Lean source · statement

theorem hilbertElementaryLayerInMaximal_isAbelianGalois
    (p : ℕ) [Fact p.Prime] :
    IsAbelianGalois K (hilbertElementaryLayerInMaximal K p)

instance

instIsAbelianGalois

L115 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInMaximal.instIsAbelianGalois

Documentation

The canonical abelian Galois instance for the copy in the maximal extension.

Source context 5 commands

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

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

Lean source · statement

instance hilbertElementaryLayerInMaximal.instIsAbelianGalois
    (p : ℕ) [Fact p.Prime] :
    IsAbelianGalois K (hilbertElementaryLayerInMaximal K p)

theorem

hilbertElementaryLayerInMaximal_galois_pow_eq_one

L121 ↗

ClassFieldTower.Martinet.hilbertElementaryLayerInMaximal_galois_pow_eq_one

Documentation

The Galois group of the copy has exponent dividing p.

Source context 5 commands

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

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

Lean source · statement

theorem hilbertElementaryLayerInMaximal_galois_pow_eq_one
    (p : ℕ) [Fact p.Prime]
    (τ : Gal((hilbertElementaryLayerInMaximal K p)/K)) :
    τ ^ p = 1

theorem

finrank_hilbertElementaryLayerInMaximal_galois_eq_pClassRank

L140 ↗

ClassFieldTower.Martinet.finrank_hilbertElementaryLayerInMaximal_galois_eq_pClassRank

Documentation

The Galois rank of the copy is the ordinary p-class rank.

Source context 5 commands

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

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

Lean source · full declaration

theorem finrank_hilbertElementaryLayerInMaximal_galois_eq_pClassRank
    (p : ℕ) [Fact p.Prime] :
    letI : Module (ZMod p)
        (Additive Gal((hilbertElementaryLayerInMaximal K p) / K)) :=
      AddCommGroup.zmodModule (fun x => by
        change (Additive.toMul x) ^ p = 1
        exact hilbertElementaryLayerInMaximal_galois_pow_eq_one
          K p (Additive.toMul x))
    Module.finrank (ZMod p)
        (Additive Gal((hilbertElementaryLayerInMaximal K p) / K)) =
      pClassRank K p := by
  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 : Module (ZMod p)
      (Additive Gal((hilbertElementaryLayerInMaximal K p) / K)) :=
    AddCommGroup.zmodModule (fun x => by
      change (Additive.toMul x) ^ p = 1
      exact hilbertElementaryLayerInMaximal_galois_pow_eq_one
        K p (Additive.toMul x))
  let e : Additive Gal((hilbertElementaryLayer K p) / K) ≃+
      Additive Gal((hilbertElementaryLayerInMaximal K p) / K) :=
    (AlgEquiv.autCongr
      (hilbertElementaryLayerEquivInMaximal K p)).toAdditive
  let eLin : Additive Gal((hilbertElementaryLayer K p) / K) ≃ₗ[ZMod p]
      Additive Gal((hilbertElementaryLayerInMaximal K p) / K) :=
    LinearEquiv.ofBijective (e.toAddMonoidHom.toZModLinearMap p) e.bijective
  calc
    Module.finrank (ZMod p)
        (Additive Gal((hilbertElementaryLayerInMaximal K p) / K)) =
        Module.finrank (ZMod p)
          (Additive Gal((hilbertElementaryLayer K p) / K)) :=
      eLin.symm.finrank_eq
    _ = pClassRank K p :=
      finrank_hilbertElementaryGalois_eq_pClassRank K p

Module documentation

The elementary Hilbert layer inside the maximal unramified pro-p extension

Declarations