Module

SmallHilbertClassFieldOverOriginalBase.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldOverOriginalBase

11 declarations indexed from sourceView source ↗

Module documentation

The small Hilbert class field over the original number field

The finite class-field construction realizes the small Hilbert class field over a canonical fixed-field copy of the input number field. The fixed-field copy is canonically ℚ-algebra equivalent to the original field. This file uses that equivalence as the actual scalar map, so the selected Hilbert class field becomes a finite abelian Galois extension of the original field itself.

This is the scalar structure used by the final extension-of-ideals map in the principal ideal theorem.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldRealization

Imported by3

instance

smallHilbertClassFieldBaseAlgebraOverOriginal

L37 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldBaseAlgebraOverOriginal

Documentation

The canonical fixed-field copy underlying the selected small Hilbert class field, 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 IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance smallHilbertClassFieldBaseAlgebraOverOriginal :
    Algebra K (smallHilbertClassFieldBase K)

def

smallHilbertClassFieldBaseEquivOverOriginal

L43 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldBaseEquivOverOriginal

Documentation

The canonical base-field identification, now regarded as an equivalence of algebras over the original field.

Source context 5 commands

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

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

Lean source · statement

def smallHilbertClassFieldBaseEquivOverOriginal :
    K ≃ₐ[K] smallHilbertClassFieldBase K

instance

smallHilbertClassFieldAlgebraOverOriginal

L52 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldAlgebraOverOriginal

Documentation

The selected small Hilbert class field, regarded as an algebra over the original number field through the canonical fixed-field copy.

Source context 5 commands

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

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

Lean source · statement

instance smallHilbertClassFieldAlgebraOverOriginal :
    Algebra K (smallHilbertClassField K)

theorem

smallHilbertClassField_algebraMap_original

L64 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_algebraMap_original

Documentation

The scalar map from the original number field into the selected small Hilbert class field is literally the canonical base equivalence followed by the fixed-field inclusion.

Source context 5 commands

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

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

Lean source · statement

theorem smallHilbertClassField_algebraMap_original
    (x : K) :
    algebraMap K (smallHilbertClassField K) x =
      algebraMap
        (smallHilbertClassFieldBase K)
        (smallHilbertClassField K)
        (smallHilbertClassFieldBaseEquiv (K := K) x)

instance

smallHilbertClassFieldBaseFiniteDimensionalOverOriginal

L75 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldBaseFiniteDimensionalOverOriginal

Documentation

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

Source context 5 commands

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

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

Lean source · statement

instance
    smallHilbertClassFieldBaseFiniteDimensionalOverOriginal :
    FiniteDimensional K (smallHilbertClassFieldBase K)

instance

smallHilbertClassFieldScalarTowerOverOriginal

L84 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldScalarTowerOverOriginal

Documentation

The original field, its canonical fixed-field copy, and the selected small Hilbert class field form the literal scalar tower used by extension of ideals.

Source context 5 commands

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

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

Lean source · statement

instance smallHilbertClassFieldScalarTowerOverOriginal :
    IsScalarTower K
      (smallHilbertClassFieldBase K)
      (smallHilbertClassField K)

instance

smallHilbertClassFieldFiniteDimensionalOverOriginal

L92 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldFiniteDimensionalOverOriginal

Documentation

The selected small 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 IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance
    smallHilbertClassFieldFiniteDimensionalOverOriginal :
    FiniteDimensional K (smallHilbertClassField K)

theorem

smallHilbertClassFieldBase_finrank_over_original

L102 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldBase_finrank_over_original

Documentation

The canonical fixed-field copy has relative degree one over the original number field.

Source context 5 commands

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

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

Lean source · statement

theorem smallHilbertClassFieldBase_finrank_over_original :
    Module.finrank K (smallHilbertClassFieldBase K) = 1

theorem

smallHilbertClassField_finrank_over_original_eq_classNumber

L110 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_finrank_over_original_eq_classNumber

Documentation

The degree of the selected small Hilbert class field over the original number field is its ordinary class number.

Source context 5 commands

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

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

Lean source · statement

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

instance

smallHilbertClassFieldIsGaloisOverOriginal

L131 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldIsGaloisOverOriginal

Documentation

The selected small Hilbert class field is Galois over the original number field, not only over its canonically equivalent fixed-field copy.

Source context 5 commands

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

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

Lean source · statement

instance smallHilbertClassFieldIsGaloisOverOriginal :
    IsGalois K (smallHilbertClassField K)

instance

smallHilbertClassFieldIsAbelianGaloisOverOriginal

L170 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldIsAbelianGaloisOverOriginal

Documentation

The selected small 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 IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

instance
    smallHilbertClassFieldIsAbelianGaloisOverOriginal :
    IsAbelianGalois K (smallHilbertClassField K)

Module documentation

The small Hilbert class field over the original number field

Declarations