Module

BigHilbertClassField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.BigHilbertClassField

8 declarations indexed from sourceView source ↗

Module documentation

The big Hilbert class field

The big Hilbert class field is the ray class field of modulus one (the zero finite modulus in the exponent-valued representation). This file identifies its defining norm quotient with the narrow class group. The maximal-unramified field statement follows from this input together with the narrow finite conductor/ramification criterion.

Imports2

Imported by5

def

bigHilbertClassFieldNormSubgroup

L34 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup

Documentation

The norm subgroup defining the big Hilbert class field.

Source context 6 commands

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

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

Lean source · statement

def bigHilbertClassFieldNormSubgroup :
    Subgroup (IdeleClassGroup K)

instance

bigHilbertClassFieldNormSubgroup_normal

L39 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup_normal

Source context 6 commands

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

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

Lean source · statement

instance bigHilbertClassFieldNormSubgroup_normal :
    (bigHilbertClassFieldNormSubgroup (K := K)).Normal

theorem

bigHilbertClassFieldNormSubgroup_isClosed

L46 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup_isClosed

Documentation

The norm subgroup defining the big Hilbert class field is closed.

Source context 6 commands

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

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

Lean source · statement

theorem bigHilbertClassFieldNormSubgroup_isClosed :
    IsClosed
      ((bigHilbertClassFieldNormSubgroup (K := K) :
        Subgroup (IdeleClassGroup K)) :
        Set (IdeleClassGroup K))

def

bigHilbertClassFieldQuotientEquivNarrowClassGroup

L57 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientEquivNarrowClassGroup

Documentation

The reciprocity quotient for the big Hilbert class field is the narrow ideal class group.

Source context 6 commands

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

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

Lean source · statement

def bigHilbertClassFieldQuotientEquivNarrowClassGroup :
    IdeleClassGroup K ⧸
        bigHilbertClassFieldNormSubgroup (K := K) ≃*
      RayClass.NarrowClassGroup K

theorem

bigHilbertClassFieldNormSubgroup_isDefiningModulus

L65 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup_isDefiningModulus

Documentation

The narrow modulus with zero finite part is a defining modulus for the big-Hilbert norm subgroup.

Source context 6 commands

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

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

Lean source · statement

theorem bigHilbertClassFieldNormSubgroup_isDefiningModulus :
    IsDefiningModulus
      (bigHilbertClassFieldNormSubgroup (K := K))
      (RayClass.Modulus.narrowOfFinite
        (0 : RayClass.FiniteModulus K))

def

bigHilbertClassFieldConductorialSubgroup

L74 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldConductorialSubgroup

Documentation

The conductorial subgroup supplied by the intrinsic big-Hilbert norm subgroup and its narrow zero-finite defining modulus.

Source context 6 commands

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

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

Lean source · statement

def bigHilbertClassFieldConductorialSubgroup :
    ConductorialSubgroup K

theorem

bigHilbertClassFieldNormSubgroup_le_iff_narrowFiniteConductor_eq_zero

L82 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup_le_iff_narrowFiniteConductor_eq_zero

Documentation

Among conductorial idèle-class subgroups, containing the big-Hilbert norm subgroup is equivalent to having narrow finite conductor zero.

Source context 6 commands

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

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

Lean source · statement

theorem
    bigHilbertClassFieldNormSubgroup_le_iff_narrowFiniteConductor_eq_zero
    (H : ConductorialSubgroup K) :
    bigHilbertClassFieldNormSubgroup (K := K) ≤ H.1 ↔
      H.narrowFiniteConductor = 0

theorem

bigHilbertClassField_narrowFiniteConductor

L106 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_narrowFiniteConductor

Documentation

The narrow finite conductor of the big-Hilbert norm subgroup is zero.

Source context 6 commands

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

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

Lean source · statement

theorem bigHilbertClassField_narrowFiniteConductor :
    (bigHilbertClassFieldConductorialSubgroup
      (K := K)).narrowFiniteConductor = 0

Module documentation

The big Hilbert class field

Declarations