Module

SmallHilbertNormCharacterization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertNormCharacterization

18 declarations indexed from sourceView source ↗

Module documentation

Small Hilbert norm subgroups and everywhere-unramified extensions

For a finite Galois extension which is unramified at both finite and infinite places, every idele integral at all finite places is an actual relative-idele norm. It follows that the actual idele-class norm range contains the small-Hilbert norm subgroup.

This realizes the maximality of the small Hilbert class field on the norm-subgroup side. The resulting quotient transition gives a canonical surjection from the ordinary class group, its exact kernel factorization, and the divisibility of the extension norm quotient order by the class number.

Imports4

Imported by4

instance

smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative

L45 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative

Documentation

Keep norm-range quotient normality out of exported declaration types.

Source context 6 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)

theorem

infiniteTensorNormSubgroup_eq_top_of_isUnramifiedAtInfinitePlaces

L54 ↗

GlobalClassFieldTheory.GlobalClassFields.infiniteTensorNormSubgroup_eq_top_of_isUnramifiedAtInfinitePlaces

Documentation

At an extension unramified at all infinite places, the determinant norm image of every infinite tensor factor is the whole local multiplicative group.

Source context 8 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [FiniteDimensional K L] in

Lean source · statement

theorem
    infiniteTensorNormSubgroup_eq_top_of_isUnramifiedAtInfinitePlaces
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (v : InfinitePlace K) :
    _root_.infiniteTensorNormSubgroup
        (K := K) (L := L) v = ⊤

theorem

chosenFinitePlaceIsUnramified_of_no_ramifiedFinitePlaces

L89 ↗

GlobalClassFieldTheory.GlobalClassFields.chosenFinitePlaceIsUnramified_of_no_ramifiedFinitePlaces

Documentation

If the finite ramification support is empty, the chosen completion above every finite base place is unramified.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem chosenFinitePlaceIsUnramified_of_no_ramifiedFinitePlaces
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (v : HeightOneSpectrum (𝓞 K)) :
    _root_.ChosenFinitePlaceIsUnramified
      (K := K) (L := L) v

theorem

integralAtFinitePlaces_le_relativeIdeleNorm_range_of_everywhereUnramified

L118 ↗

GlobalClassFieldTheory.GlobalClassFields.integralAtFinitePlaces_le_relativeIdeleNorm_range_of_everywhereUnramified

Documentation

In an extension unramified at every finite and infinite place, every idele integral at all finite places is an actual relative-idele norm.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    integralAtFinitePlaces_le_relativeIdeleNorm_range_of_everywhereUnramified
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    IdeleGroup.integralAtFinitePlaces (K := K) ≤
      (RelativeIdeleGroup.norm K L).range

theorem

integralIdeleClass_mem_ideleClassNorm_range_of_everywhereUnramified

L147 ↗

GlobalClassFieldTheory.GlobalClassFields.integralIdeleClass_mem_ideleClassNorm_range_of_everywhereUnramified

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem integralIdeleClass_mem_ideleClassNorm_range_of_everywhereUnramified
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    {a : IdeleGroup K}
    (ha : a ∈ IdeleGroup.integralAtFinitePlaces (K := K)) :
    QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K) a ∈
      (_root_.ideleClassNorm K L).range

theorem

principalIdeleClass_mem_ideleClassNorm_range

L177 ↗

GlobalClassFieldTheory.GlobalClassFields.principalIdeleClass_mem_ideleClassNorm_range

Source context 8 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem principalIdeleClass_mem_ideleClassNorm_range
    {a : IdeleGroup K}
    (ha : a ∈ IdeleGroup.principalSubgroup K) :
    QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K) a ∈
      (_root_.ideleClassNorm K L).range

theorem

smallHilbertClassFieldNormSubgroup_le_ideleClassNorm_range_of_everywhereUnramified

L192 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup_le_ideleClassNorm_range_of_everywhereUnramified

Documentation

The norm subgroup of an everywhere-unramified finite Galois extension contains the small-Hilbert norm subgroup.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    smallHilbertClassFieldNormSubgroup_le_ideleClassNorm_range_of_everywhereUnramified
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    smallHilbertClassFieldNormSubgroup (K := K) ≤
      (_root_.ideleClassNorm K L).range

def

smallHilbertClassFieldQuotientToIdeleClassNormQuotient

L215 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientToIdeleClassNormQuotient

Documentation

The canonical transition from the small-Hilbert reciprocity quotient to the actual norm quotient of an everywhere-unramified extension.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def smallHilbertClassFieldQuotientToIdeleClassNormQuotient
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    (IdeleClassGroup K ⧸
        smallHilbertClassFieldNormSubgroup (K := K)) →*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)

theorem

smallHilbertClassFieldQuotientToIdeleClassNormQuotient_mk

L235 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientToIdeleClassNormQuotient_mk

Documentation

The small-Hilbert quotient transition sends an idele class to the same class modulo the actual norm subgroup.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem smallHilbertClassFieldQuotientToIdeleClassNormQuotient_mk
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (x : IdeleClassGroup K) :
    smallHilbertClassFieldQuotientToIdeleClassNormQuotient
        (K := K) (L := L) hunramifiedFinite
        (QuotientGroup.mk'
          (smallHilbertClassFieldNormSubgroup (K := K)) x) =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K L).range) x

theorem

smallHilbertClassFieldQuotientToIdeleClassNormQuotient_surjective

L251 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientToIdeleClassNormQuotient_surjective

Documentation

The transition from the small-Hilbert quotient to an everywhere-unramified actual norm quotient is surjective.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    smallHilbertClassFieldQuotientToIdeleClassNormQuotient_surjective
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Function.Surjective
      (smallHilbertClassFieldQuotientToIdeleClassNormQuotient
        (K := K) (L := L) hunramifiedFinite)

theorem

smallHilbertClassFieldQuotientToIdeleClassNormQuotient_ker

L271 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientToIdeleClassNormQuotient_ker

Documentation

The kernel of the small-Hilbert quotient transition is the image of the actual norm subgroup modulo the small-Hilbert norm subgroup.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    smallHilbertClassFieldQuotientToIdeleClassNormQuotient_ker
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    MonoidHom.ker
        (smallHilbertClassFieldQuotientToIdeleClassNormQuotient
          (K := K) (L := L) hunramifiedFinite) =
      Subgroup.map
        (QuotientGroup.mk'
          (smallHilbertClassFieldNormSubgroup (K := K)))
        ((_root_.ideleClassNorm K L).range)

def

smallHilbertNormImageQuotientEquivIdeleClassNormQuotient

L300 ↗

GlobalClassFieldTheory.GlobalClassFields.smallHilbertNormImageQuotientEquivIdeleClassNormQuotient

Documentation

Quotienting the small-Hilbert reciprocity quotient by the image of the actual norm subgroup recovers the actual norm quotient.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def smallHilbertNormImageQuotientEquivIdeleClassNormQuotient
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    ((IdeleClassGroup K ⧸
          smallHilbertClassFieldNormSubgroup (K := K)) ⧸
        Subgroup.map
          (QuotientGroup.mk'
            (smallHilbertClassFieldNormSubgroup (K := K)))
          ((_root_.ideleClassNorm K L).range)) ≃*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)

def

classGroupToIdeleClassNormQuotient

L324 ↗

GlobalClassFieldTheory.GlobalClassFields.classGroupToIdeleClassNormQuotient

Documentation

The ordinary class group maps canonically onto the actual norm quotient of every everywhere-unramified finite Galois extension.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def classGroupToIdeleClassNormQuotient
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    ClassGroup (𝓞 K) →*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)

theorem

classGroupToIdeleClassNormQuotient_surjective

L339 ↗

GlobalClassFieldTheory.GlobalClassFields.classGroupToIdeleClassNormQuotient_surjective

Documentation

The canonical map from the ordinary class group to the actual norm quotient of an everywhere-unramified extension is surjective.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem classGroupToIdeleClassNormQuotient_surjective
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Function.Surjective
      (classGroupToIdeleClassNormQuotient
        (K := K) (L := L) hunramifiedFinite)

theorem

ideleClassNormQuotient_card_dvd_classNumber_of_everywhereUnramified

L354 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotient_card_dvd_classNumber_of_everywhereUnramified

Documentation

The actual norm quotient of an everywhere-unramified finite Galois extension has order dividing the class number.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    ideleClassNormQuotient_card_dvd_classNumber_of_everywhereUnramified
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Nat.card
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) ∣
      NumberField.classNumber K

theorem

classNumber_eq_unramifiedNormKernel_card_mul_normQuotient_card

L382 ↗

GlobalClassFieldTheory.GlobalClassFields.classNumber_eq_unramifiedNormKernel_card_mul_normQuotient_card

Documentation

The class number factors as the kernel order of the canonical class group map times the order of an everywhere-unramified actual norm quotient.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    classNumber_eq_unramifiedNormKernel_card_mul_normQuotient_card
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    NumberField.classNumber K =
      Nat.card
          (MonoidHom.ker
            (classGroupToIdeleClassNormQuotient
              (K := K) (L := L) hunramifiedFinite)) *
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range)

theorem

cyclicEverywhereUnramifiedExtensionDegree_dvd_classNumber

L421 ↗

GlobalClassFieldTheory.GlobalClassFields.cyclicEverywhereUnramifiedExtensionDegree_dvd_classNumber

Documentation

The degree of every finite cyclic extension unramified at all finite and infinite places divides the class number.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem cyclicEverywhereUnramifiedExtensionDegree_dvd_classNumber
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    [IsCyclic (L ≃ₐ[K] L)]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Module.finrank K L ∣
      NumberField.classNumber K

theorem

classNumber_eq_unramifiedCyclicNormKernel_card_mul_extensionDegree

L438 ↗

GlobalClassFieldTheory.GlobalClassFields.classNumber_eq_unramifiedCyclicNormKernel_card_mul_extensionDegree

Documentation

For a finite cyclic extension unramified at all finite and infinite places, the class number is the kernel order of the canonical class group reciprocity map times the extension degree.

Source context 7 commands

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

open scoped IsMulCommutative NumberField NumberField.LiesOver
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField IsDedekindDomain
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    smallHilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    classNumber_eq_unramifiedCyclicNormKernel_card_mul_extensionDegree
    [_root_.IsUnramifiedAtInfinitePlaces K L]
    [IsCyclic (L ≃ₐ[K] L)]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    NumberField.classNumber K =
      Nat.card
          (MonoidHom.ker
            (classGroupToIdeleClassNormQuotient
              (K := K) (L := L) hunramifiedFinite)) *
        Module.finrank K L

Module documentation

Small Hilbert norm subgroups and everywhere-unramified extensions

Declarations