Module

HilbertClassFieldUnramifiedMaximality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldUnramifiedMaximality

11 declarations indexed from sourceView source ↗

Module documentation

Unramifiedness and maximality of Hilbert class fields

The selected big and small Hilbert class fields have the prescribed idele-class norm ranges. Exact local--global narrow finite conductor compatibility therefore turns the vanishing of their intrinsic finite conductors into actual unramifiedness at every finite prime.

Imports8

Imported by5

theorem

isUnramifiedAtFinitePlaces_of_normRange_eq_bigHilbertNormSubgroup

L44 ↗

GlobalClassFieldTheory.GlobalClassFields.isUnramifiedAtFinitePlaces_of_normRange_eq_bigHilbertNormSubgroup

Documentation

Any actual finite abelian realization of the intrinsic big-Hilbert norm subgroup is unramified at every finite prime.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem isUnramifiedAtFinitePlaces_of_normRange_eq_bigHilbertNormSubgroup
    (hnorm :
      (_root_.ideleClassNorm K L).range =
        bigHilbertClassFieldNormSubgroup (K := K)) :
    IsUnramifiedAtFinitePlaces K L

theorem

isUnramifiedAtFinitePlaces_of_normRange_eq_smallHilbertNormSubgroup

L64 ↗

GlobalClassFieldTheory.GlobalClassFields.isUnramifiedAtFinitePlaces_of_normRange_eq_smallHilbertNormSubgroup

Documentation

Any actual finite abelian realization of the intrinsic small-Hilbert norm subgroup is unramified at every finite prime.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem isUnramifiedAtFinitePlaces_of_normRange_eq_smallHilbertNormSubgroup
    (hnorm :
      (_root_.ideleClassNorm K L).range =
        smallHilbertClassFieldNormSubgroup (K := K)) :
    IsUnramifiedAtFinitePlaces K L

theorem

isUnramifiedAtInfinitePlaces_of_normRange_eq_smallHilbertNormSubgroup

L84 ↗

GlobalClassFieldTheory.GlobalClassFields.isUnramifiedAtInfinitePlaces_of_normRange_eq_smallHilbertNormSubgroup

Documentation

Any actual finite abelian realization of the intrinsic small-Hilbert norm subgroup splits every infinite place completely.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · statement

theorem isUnramifiedAtInfinitePlaces_of_normRange_eq_smallHilbertNormSubgroup
    (hnorm :
      (_root_.ideleClassNorm K L).range =
        smallHilbertClassFieldNormSubgroup (K := K)) :
    IsUnramifiedAtInfinitePlaces K L

theorem

isEverywhereUnramified_of_normRange_eq_smallHilbertNormSubgroup

L116 ↗

GlobalClassFieldTheory.GlobalClassFields.isEverywhereUnramified_of_normRange_eq_smallHilbertNormSubgroup

Documentation

Any actual finite abelian realization of the intrinsic small-Hilbert norm subgroup is everywhere unramified.

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 L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]

Lean source · full declaration

theorem isEverywhereUnramified_of_normRange_eq_smallHilbertNormSubgroup
    (hnorm :
      (_root_.ideleClassNorm K L).range =
        smallHilbertClassFieldNormSubgroup (K := K)) :
    IsEverywhereUnramified K L where
  finitePlaces :=
    isUnramifiedAtFinitePlaces_of_normRange_eq_smallHilbertNormSubgroup
      hnorm
  infinitePlaces :=
    isUnramifiedAtInfinitePlaces_of_normRange_eq_smallHilbertNormSubgroup
      hnorm

theorem

ramifiedBaseFinitePlaces_eq_empty_of_isUnramifiedAtFinitePlaces

L129 ↗

GlobalClassFieldTheory.GlobalClassFields.ramifiedBaseFinitePlaces_eq_empty_of_isUnramifiedAtFinitePlaces

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
omit [FiniteDimensional K L] [IsAbelianGalois K L] in

Lean source · statement

theorem ramifiedBaseFinitePlaces_eq_empty_of_isUnramifiedAtFinitePlaces
    (hunramified : IsUnramifiedAtFinitePlaces K L) :
    _root_.ramifiedBaseFinitePlaces (K := K) (L := L) = ∅

theorem

bigHilbertClassField_isUnramifiedAtFinitePlaces

L143 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_isUnramifiedAtFinitePlaces

Documentation

The selected big Hilbert class field is unramified at every finite prime of the original number field.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem bigHilbertClassField_isUnramifiedAtFinitePlaces :
    IsUnramifiedAtFinitePlaces K (bigHilbertClassField K)

theorem

smallHilbertClassField_isUnramifiedAtFinitePlaces

L152 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_isUnramifiedAtFinitePlaces

Documentation

The selected small Hilbert class field is unramified at every finite prime of the original number field.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassField_isUnramifiedAtFinitePlaces :
    IsUnramifiedAtFinitePlaces K (smallHilbertClassField K)

theorem

smallHilbertClassField_isUnramifiedAtInfinitePlaces

L164 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_isUnramifiedAtInfinitePlaces

Documentation

Every infinite place splits completely in the selected small Hilbert class field. Indeed, an idele supported at an infinite place is integral at every finite place, hence belongs to the intrinsic small-Hilbert norm subgroup; infinite-place local--global compatibility then identifies its component with an actual local norm.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassField_isUnramifiedAtInfinitePlaces :
    IsUnramifiedAtInfinitePlaces K (smallHilbertClassField K)

theorem

smallHilbertClassField_isEverywhereUnramified

L173 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_isEverywhereUnramified

Documentation

The selected small Hilbert class field is everywhere unramified over the original number field.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassField_isEverywhereUnramified :
    IsEverywhereUnramified K (smallHilbertClassField K)

theorem

bigHilbertClassField_ramifiedBaseFinitePlaces_eq_empty

L181 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_ramifiedBaseFinitePlaces_eq_empty

Documentation

Equivalently, the actual finite ramification set of the selected big Hilbert class field is empty.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem bigHilbertClassField_ramifiedBaseFinitePlaces_eq_empty :
    _root_.ramifiedBaseFinitePlaces
        (K := K) (L := bigHilbertClassField K) = ∅

theorem

smallHilbertClassField_ramifiedBaseFinitePlaces_eq_empty

L191 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_ramifiedBaseFinitePlaces_eq_empty

Documentation

Equivalently, the actual finite ramification set of the selected small Hilbert class field is empty.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassField_ramifiedBaseFinitePlaces_eq_empty :
    _root_.ramifiedBaseFinitePlaces
        (K := K) (L := smallHilbertClassField K) = ∅

Module documentation

Unramifiedness and maximality of Hilbert class fields

Declarations