Module

HilbertClassFieldRealization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldRealization

20 declarations indexed from sourceView source ↗

Module documentation

Actual realizations of the Hilbert class fields

The big and small Hilbert norm subgroups are closed and have finite index. The finite-index class-field construction therefore supplies genuine finite abelian subextensions of the rational separable closure. This file fixes those subextensions once and for all, names their actual relative fixed fields, and identifies their determinant-norm ranges.

The resulting degrees are the orders of the corresponding reciprocity quotients: the narrow class number for the big Hilbert class field and the ordinary class number for the small Hilbert class field.

Imports12

Imported by5

instance

bigHilbertClassFieldNormSubgroupFiniteIndex

L52 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroupFiniteIndex

Documentation

The big-Hilbert congruence subgroup has finite index, registered at the realization layer where the closed finite-index construction uses it.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance bigHilbertClassFieldNormSubgroupFiniteIndex :
    (bigHilbertClassFieldNormSubgroup (K := K)).FiniteIndex

abbrev

bigHilbertClassFieldNormAmbient

L59 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormAmbient

Documentation

The concrete finite Galois norm neighbourhood used to realize the big Hilbert class field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev bigHilbertClassFieldNormAmbient (K : Type)
    [Field K] [NumberField K] : Type

abbrev

smallHilbertClassFieldNormAmbient

L68 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormAmbient

Documentation

The concrete finite Galois norm neighbourhood used to realize the small Hilbert class field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertClassFieldNormAmbient (K : Type)
    [Field K] [NumberField K] : Type

abbrev

bigHilbertClassFieldBaseSubgroup

L77 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBaseSubgroup

Documentation

The compatible abstract base subgroup for the actual big Hilbert class-field realization.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev bigHilbertClassFieldBaseSubgroup (K : Type)
    [Field K] [NumberField K]

abbrev

bigHilbertClassFieldSubextension

L86 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldSubextension

Documentation

The finite abelian subextension selected by the big-Hilbert norm subgroup. This is the actual class-field witness, rather than merely an existence proposition.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev bigHilbertClassFieldSubextension (K : Type)
    [Field K] [NumberField K] :
    FiniteAbelianSubextension
      (bigHilbertClassFieldBaseSubgroup K)

abbrev

bigHilbertClassFieldBase

L96 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBase

Documentation

The compatible actual copy of the original number field occurring as the base fixed field in the big-Hilbert realization.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev bigHilbertClassFieldBase (K : Type)
    [Field K] [NumberField K] : Type

abbrev

bigHilbertClassField

L104 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField

Documentation

The actual big Hilbert class field selected inside the rational separable closure.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev bigHilbertClassField (K : Type)
    [Field K] [NumberField K] : Type

abbrev

bigHilbertClassFieldBaseEquiv

L112 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBaseEquiv

Documentation

The canonical equivalence from K to the actual base fixed field used by the selected big Hilbert class field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev bigHilbertClassFieldBaseEquiv :
    K ≃ₐ[ℚ] bigHilbertClassFieldBase K

def

bigHilbertClassFieldTransportedNormSubgroup

L120 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldTransportedNormSubgroup

Documentation

The big-Hilbert norm subgroup transported to the actual base fixed field of the selected realization.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def bigHilbertClassFieldTransportedNormSubgroup :
    Subgroup (IdeleClassGroup (bigHilbertClassFieldBase K))

theorem

bigHilbertClassField_ideleClassNorm_range

L128 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_ideleClassNorm_range

Documentation

The determinant-norm range of the actual big Hilbert class field is exactly the transported big-Hilbert norm subgroup.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem bigHilbertClassField_ideleClassNorm_range :
    (_root_.ideleClassNorm
      (bigHilbertClassFieldBase K)
      (bigHilbertClassField K)).range =
      bigHilbertClassFieldTransportedNormSubgroup (K := K)

theorem

closedFiniteIndexClassField_finrank_over_base_eq_index

L140 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField_finrank_over_base_eq_index

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem
    closedFiniteIndexClassField_finrank_over_base_eq_index
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Module.finrank
        (closedFiniteIndexClassFieldBase
          (K := K) H hclosed)
        (closedFiniteIndexClassField
          (K := K) H hclosed) =
      H.index

theorem

bigHilbertClassField_finrank_eq_narrowClassGroup_card

L182 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_finrank_eq_narrowClassGroup_card

Documentation

The degree of the actual big Hilbert class field is the narrow class number.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem bigHilbertClassField_finrank_eq_narrowClassGroup_card :
    Module.finrank
        (bigHilbertClassFieldBase K)
        (bigHilbertClassField K) =
      Nat.card (RayClass.NarrowClassGroup K)

abbrev

smallHilbertClassFieldBaseSubgroup

L208 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldBaseSubgroup

Documentation

The compatible abstract base subgroup for the actual small Hilbert class-field realization.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertClassFieldBaseSubgroup (K : Type)
    [Field K] [NumberField K]

abbrev

smallHilbertClassFieldSubextension

L216 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldSubextension

Documentation

The finite abelian subextension selected by the small-Hilbert norm subgroup. This named witness is the input used by principalization.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertClassFieldSubextension (K : Type)
    [Field K] [NumberField K] :
    FiniteAbelianSubextension
      (smallHilbertClassFieldBaseSubgroup K)

abbrev

smallHilbertClassFieldBase

L226 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldBase

Documentation

The compatible actual copy of the original number field occurring as the base fixed field in the small-Hilbert realization.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertClassFieldBase (K : Type)
    [Field K] [NumberField K] : Type

abbrev

smallHilbertClassField

L234 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField

Documentation

The actual small Hilbert class field selected inside the rational separable closure.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertClassField (K : Type)
    [Field K] [NumberField K] : Type

abbrev

smallHilbertClassFieldBaseEquiv

L242 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldBaseEquiv

Documentation

The canonical equivalence from K to the actual base fixed field used by the selected small Hilbert class field.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

abbrev smallHilbertClassFieldBaseEquiv :
    K ≃ₐ[ℚ] smallHilbertClassFieldBase K

def

smallHilbertClassFieldTransportedNormSubgroup

L250 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldTransportedNormSubgroup

Documentation

The small-Hilbert norm subgroup transported to the actual base fixed field of the selected realization.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def smallHilbertClassFieldTransportedNormSubgroup :
    Subgroup (IdeleClassGroup (smallHilbertClassFieldBase K))

theorem

smallHilbertClassField_ideleClassNorm_range

L258 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_ideleClassNorm_range

Documentation

The determinant-norm range of the actual small Hilbert class field is exactly the transported small-Hilbert norm subgroup.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassField_ideleClassNorm_range :
    (_root_.ideleClassNorm
      (smallHilbertClassFieldBase K)
      (smallHilbertClassField K)).range =
      smallHilbertClassFieldTransportedNormSubgroup (K := K)

theorem

smallHilbertClassField_finrank_eq_classNumber

L272 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_finrank_eq_classNumber

Documentation

The degree of the actual small Hilbert class field is the ordinary class number.

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open NumberField
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassField_finrank_eq_classNumber :
    Module.finrank
        (smallHilbertClassFieldBase K)
        (smallHilbertClassField K) =
      NumberField.classNumber K

Module documentation

Actual realizations of the Hilbert class fields

Declarations