Module

BigHilbertClassFieldOverOriginalBase.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassFieldOverOriginalBase

11 declarations indexed from sourceView source ↗

Module documentation

The big Hilbert class field over the original number field

The selected big Hilbert class field is constructed over a canonical fixed-field copy of the input number field. The canonical equivalence with the original field supplies the actual scalar map used here. Thus the selected field is a finite abelian Galois extension of the original number field, with degree equal to the narrow class number.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldRealization

Imported by3

instance

bigHilbertClassFieldBaseAlgebraOverOriginal

L32 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBaseAlgebraOverOriginal

Documentation

The canonical base fixed field of the big Hilbert realization, regarded as an algebra over the original number field.

Source context 5 commands

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

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

Lean source · statement

instance bigHilbertClassFieldBaseAlgebraOverOriginal :
    Algebra K (bigHilbertClassFieldBase K)

def

bigHilbertClassFieldBaseEquivOverOriginal

L38 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBaseEquivOverOriginal

Documentation

The canonical base-field identification as an equivalence of algebras over the original number field.

Source context 5 commands

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

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

Lean source · statement

def bigHilbertClassFieldBaseEquivOverOriginal :
    K ≃ₐ[K] bigHilbertClassFieldBase K

instance

bigHilbertClassFieldAlgebraOverOriginal

L47 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldAlgebraOverOriginal

Documentation

The selected big Hilbert class field as an algebra over the original number field.

Source context 5 commands

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

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

Lean source · statement

instance bigHilbertClassFieldAlgebraOverOriginal :
    Algebra K (bigHilbertClassField K)

theorem

bigHilbertClassField_algebraMap_original

L58 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_algebraMap_original

Documentation

The scalar map into the selected big Hilbert class field is the canonical base equivalence followed by fixed-field inclusion.

Source context 5 commands

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

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

Lean source · statement

theorem bigHilbertClassField_algebraMap_original
    (x : K) :
    algebraMap K (bigHilbertClassField K) x =
      algebraMap
        (bigHilbertClassFieldBase K)
        (bigHilbertClassField K)
        (bigHilbertClassFieldBaseEquiv (K := K) x)

instance

bigHilbertClassFieldBaseFiniteDimensionalOverOriginal

L69 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBaseFiniteDimensionalOverOriginal

Documentation

The canonical base fixed field has degree one over the original number field.

Source context 5 commands

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

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

Lean source · statement

instance
    bigHilbertClassFieldBaseFiniteDimensionalOverOriginal :
    FiniteDimensional K (bigHilbertClassFieldBase K)

instance

bigHilbertClassFieldScalarTowerOverOriginal

L77 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldScalarTowerOverOriginal

Documentation

The original field, its fixed-field copy, and the selected big Hilbert class field form the literal scalar tower.

Source context 5 commands

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

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

Lean source · statement

instance bigHilbertClassFieldScalarTowerOverOriginal :
    IsScalarTower K
      (bigHilbertClassFieldBase K)
      (bigHilbertClassField K)

instance

bigHilbertClassFieldFiniteDimensionalOverOriginal

L85 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldFiniteDimensionalOverOriginal

Documentation

The selected big Hilbert class field is finite-dimensional over the original number field.

Source context 5 commands

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

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

Lean source · statement

instance
    bigHilbertClassFieldFiniteDimensionalOverOriginal :
    FiniteDimensional K (bigHilbertClassField K)

theorem

bigHilbertClassFieldBase_finrank_over_original

L94 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldBase_finrank_over_original

Documentation

The canonical base fixed field has relative degree one.

Source context 5 commands

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

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

Lean source · statement

theorem bigHilbertClassFieldBase_finrank_over_original :
    Module.finrank K (bigHilbertClassFieldBase K) = 1

theorem

bigHilbertClassField_finrank_over_original_eq_narrowClassGroup_card

L102 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_finrank_over_original_eq_narrowClassGroup_card

Documentation

The degree of the selected big Hilbert class field over the original number field is the order of the narrow class group.

Source context 5 commands

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

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

Lean source · statement

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

instance

bigHilbertClassFieldIsGaloisOverOriginal

L123 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldIsGaloisOverOriginal

Documentation

The selected big Hilbert class field is Galois over the original number field.

Source context 5 commands

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

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

Lean source · statement

instance bigHilbertClassFieldIsGaloisOverOriginal :
    IsGalois K (bigHilbertClassField K)

instance

bigHilbertClassFieldIsAbelianGaloisOverOriginal

L162 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldIsAbelianGaloisOverOriginal

Documentation

The selected big Hilbert class field is an abelian Galois extension of the original number field.

Source context 5 commands

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

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

Lean source · statement

instance bigHilbertClassFieldIsAbelianGaloisOverOriginal :
    IsAbelianGalois K (bigHilbertClassField K)

Module documentation

The big Hilbert class field over the original number field

Declarations