Module

HilbertClassFieldMaximality.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldMaximality

16 declarations indexed from sourceView source ↗

Module documentation

Maximality criteria for Hilbert class fields

An unramified cyclic extension reaches the big or small Hilbert norm subgroup exactly when its degree reaches the corresponding narrow or ordinary class number. Thus a maximal-degree unramified cyclic extension has the canonical Hilbert reciprocity quotient.

Imports2

Imported by2

theorem

hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative

L30 ↗

GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField

Lean source · statement

theorem hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

instance

narrowClassGroup_finite

L44 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowClassGroup_finite

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

instance narrowClassGroup_finite :
    Finite (RayClass.NarrowClassGroup K)

instance

bigHilbertNormQuotient_finite

L53 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertNormQuotient_finite

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

instance bigHilbertNormQuotient_finite :
    Finite
      (IdeleClassGroup K ⧸
        bigHilbertClassFieldNormSubgroup (K := K))

instance

bigHilbertNormSubgroup_finiteIndex

L62 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertNormSubgroup_finiteIndex

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

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

theorem

ideleClassNorm_range_eq_bigHilbertClassFieldNormSubgroup_iff_finrank_eq_narrowClassGroup_card

L70 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_eq_bigHilbertClassFieldNormSubgroup_iff_finrank_eq_narrowClassGroup_card

Documentation

A cyclic extension unramified at all finite places has the big Hilbert norm subgroup exactly when its degree is the order of the narrow class group.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    ideleClassNorm_range_eq_bigHilbertClassFieldNormSubgroup_iff_finrank_eq_narrowClassGroup_card
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    (_root_.ideleClassNorm K L).range =
        bigHilbertClassFieldNormSubgroup (K := K) ↔
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K)

theorem

narrowClassGroupToIdeleClassNormQuotient_injective_iff_finrank_eq_narrowClassGroup_card

L146 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowClassGroupToIdeleClassNormQuotient_injective_iff_finrank_eq_narrowClassGroup_card

Documentation

The canonical narrow-class reciprocity map for a finite-unramified cyclic extension is injective exactly at maximal possible degree.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    narrowClassGroupToIdeleClassNormQuotient_injective_iff_finrank_eq_narrowClassGroup_card
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Function.Injective
        (narrowClassGroupToIdeleClassNormQuotient
          (K := K) (L := L) hunramified) ↔
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K)

def

maximalFiniteUnramifiedCyclicNormQuotientEquivNarrowClassGroup

L196 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalFiniteUnramifiedCyclicNormQuotientEquivNarrowClassGroup

Documentation

At maximal narrow-class degree, the actual norm quotient of an unramified cyclic extension is canonically the narrow class group.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

def maximalFiniteUnramifiedCyclicNormQuotientEquivNarrowClassGroup
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K)) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      RayClass.NarrowClassGroup K

theorem

ideleClassNorm_range_eq_smallHilbertClassFieldNormSubgroup_iff_finrank_eq_classNumber

L216 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_eq_smallHilbertClassFieldNormSubgroup_iff_finrank_eq_classNumber

Documentation

A cyclic extension unramified at every finite and infinite place has the small Hilbert norm subgroup exactly when its degree is the ordinary class number.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    ideleClassNorm_range_eq_smallHilbertClassFieldNormSubgroup_iff_finrank_eq_classNumber
    [IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    (_root_.ideleClassNorm K L).range =
        smallHilbertClassFieldNormSubgroup (K := K) ↔
      Module.finrank K L =
        NumberField.classNumber K

theorem

classGroupToIdeleClassNormQuotient_injective_iff_finrank_eq_classNumber

L292 ↗

GlobalClassFieldTheory.GlobalClassFields.classGroupToIdeleClassNormQuotient_injective_iff_finrank_eq_classNumber

Documentation

The canonical ordinary class-group reciprocity map for an everywhere-unramified cyclic extension is injective exactly at maximal possible degree.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem
    classGroupToIdeleClassNormQuotient_injective_iff_finrank_eq_classNumber
    [IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Function.Injective
        (classGroupToIdeleClassNormQuotient
          (K := K) (L := L) hunramifiedFinite) ↔
      Module.finrank K L =
        NumberField.classNumber K

def

maximalEverywhereUnramifiedCyclicNormQuotientEquivClassGroup

L358 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicNormQuotientEquivClassGroup

Documentation

At maximal ordinary-class degree, the actual norm quotient of an everywhere-unramified cyclic extension is canonically the ordinary ideal class group.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

def maximalEverywhereUnramifiedCyclicNormQuotientEquivClassGroup
    [IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hdegree :
      Module.finrank K L =
        NumberField.classNumber K) :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) ≃*
      ClassGroup (𝓞 K)

theorem

maximalFiniteUnramifiedCyclicNormRanges_eq

L378 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalFiniteUnramifiedCyclicNormRanges_eq

Documentation

Any two finite-unramified cyclic extensions attaining the narrow class number determine the same idèle-class norm subgroup. This is uniqueness of the big Hilbert class field at the norm-subgroup level.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem maximalFiniteUnramifiedCyclicNormRanges_eq
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    [IsCyclic (M ≃ₐ[K] M)]
    (hLunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hMunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := M) = ∅)
    (hLdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (hMdegree :
      Module.finrank K M =
        Nat.card (RayClass.NarrowClassGroup K)) :
    (_root_.ideleClassNorm K L).range =
      (_root_.ideleClassNorm K M).range

theorem

maximalEverywhereUnramifiedCyclicNormRanges_eq

L411 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicNormRanges_eq

Documentation

Any two everywhere-unramified cyclic extensions attaining the ordinary class number determine the same idèle-class norm subgroup. This is uniqueness of the small Hilbert class field at the norm-subgroup level.

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
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]

Lean source · statement

theorem maximalEverywhereUnramifiedCyclicNormRanges_eq
    {M : Type}
    [Field M] [NumberField M] [Algebra K M]
    [FiniteDimensional K M] [IsGalois K M]
    [IsCyclic (M ≃ₐ[K] M)]
    [IsUnramifiedAtInfinitePlaces K L]
    [IsUnramifiedAtInfinitePlaces K M]
    (hLunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (hMunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := M) = ∅)
    (hLdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (hMdegree :
      Module.finrank K M =
        NumberField.classNumber K) :
    (_root_.ideleClassNorm K L).range =
      (_root_.ideleClassNorm K M).range

theorem

maximalFiniteUnramifiedCyclicExtension_relativeDegree_eq_one

L445 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalFiniteUnramifiedCyclicExtension_relativeDegree_eq_one

Documentation

A finite-unramified cyclic extension whose degree is the narrow class number has no proper nested finite-unramified cyclic overextension over the same base field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [IsCyclic (L ≃ₐ[K] L)] in

Lean source · statement

theorem
    maximalFiniteUnramifiedCyclicExtension_relativeDegree_eq_one
    {M : Type}
    [Field M] [NumberField M]
    [Algebra L M] [Algebra K M] [IsScalarTower K L M]
    [FiniteDimensional L M] [FiniteDimensional K M]
    [IsGalois K M] [IsCyclic (M ≃ₐ[K] M)]
    (hLdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (hMunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := M) = ∅) :
    Module.finrank L M = 1

theorem

maximalEverywhereUnramifiedCyclicExtension_relativeDegree_eq_one

L482 ↗

GlobalClassFieldTheory.GlobalClassFields.maximalEverywhereUnramifiedCyclicExtension_relativeDegree_eq_one

Documentation

An everywhere-unramified cyclic extension whose degree is the ordinary class number has no proper nested everywhere-unramified cyclic overextension over the same base field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [IsCyclic (L ≃ₐ[K] L)] in

Lean source · statement

theorem
    maximalEverywhereUnramifiedCyclicExtension_relativeDegree_eq_one
    {M : Type}
    [Field M] [NumberField M]
    [Algebra L M] [Algebra K M] [IsScalarTower K L M]
    [FiniteDimensional L M] [FiniteDimensional K M]
    [IsGalois K M] [IsCyclic (M ≃ₐ[K] M)]
    [IsUnramifiedAtInfinitePlaces K M]
    (hLdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (hMunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := M) = ∅) :
    Module.finrank L M = 1

theorem

properCyclicOverextension_of_maximalFiniteUnramifiedExtension_has_ramifiedFinitePlace

L519 ↗

GlobalClassFieldTheory.GlobalClassFields.properCyclicOverextension_of_maximalFiniteUnramifiedExtension_has_ramifiedFinitePlace

Documentation

A proper cyclic overextension of a narrow-class-degree extension must ramify at some finite place of the base field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [IsCyclic (L ≃ₐ[K] L)] in

Lean source · statement

theorem
    properCyclicOverextension_of_maximalFiniteUnramifiedExtension_has_ramifiedFinitePlace
    {M : Type}
    [Field M] [NumberField M]
    [Algebra L M] [Algebra K M] [IsScalarTower K L M]
    [FiniteDimensional L M] [FiniteDimensional K M]
    [IsGalois K M] [IsCyclic (M ≃ₐ[K] M)]
    (hLdegree :
      Module.finrank K L =
        Nat.card (RayClass.NarrowClassGroup K))
    (hrelativeDegree :
      Module.finrank L M ≠ 1) :
    _root_.ramifiedBaseFinitePlaces
        (K := K) (L := M) ≠ ∅

theorem

properCyclicOverextension_of_maximalEverywhereUnramifiedExtension_has_ramifiedFinitePlace

L544 ↗

GlobalClassFieldTheory.GlobalClassFields.properCyclicOverextension_of_maximalEverywhereUnramifiedExtension_has_ramifiedFinitePlace

Documentation

A proper cyclic overextension which is unramified at every infinite place and lies above an ordinary-class-degree extension must ramify at some finite place of the base field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] hilbertClassFieldMaximalityIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [IsCyclic (L ≃ₐ[K] L)] in

Lean source · statement

theorem
    properCyclicOverextension_of_maximalEverywhereUnramifiedExtension_has_ramifiedFinitePlace
    {M : Type}
    [Field M] [NumberField M]
    [Algebra L M] [Algebra K M] [IsScalarTower K L M]
    [FiniteDimensional L M] [FiniteDimensional K M]
    [IsGalois K M] [IsCyclic (M ≃ₐ[K] M)]
    [IsUnramifiedAtInfinitePlaces K M]
    (hLdegree :
      Module.finrank K L =
        NumberField.classNumber K)
    (hrelativeDegree :
      Module.finrank L M ≠ 1) :
    _root_.ramifiedBaseFinitePlaces
        (K := K) (L := M) ≠ ∅

Module documentation

Maximality criteria for Hilbert class fields

Declarations