Module

HilbertNormCharacterization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertNormCharacterization

14 declarations indexed from sourceView source ↗

Module documentation

Hilbert norm subgroups and unramified extensions

For a finite Galois extension with no ramified finite prime, the actual idele-class narrow finite conductor is zero. Consequently its norm subgroup contains the big-Hilbert norm subgroup. This is the norm-subgroup form of the maximality of the big Hilbert class field.

The inclusion yields a canonical surjection from the narrow class group onto the actual norm quotient, together with the exact kernel factorization and the resulting divisibility of orders.

Imports3

Imported by3

instance

hilbertNormCharacterization_ideleClassGroupIsMulCommutative

L42 ↗

GlobalClassFieldTheory.GlobalClassFields.hilbertNormCharacterization_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
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] [IsGalois K L]

Lean source · statement

instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)

theorem

ideleClassNorm_narrowFiniteConductor_eq_zero_of_no_ramifiedFinitePlaces

L49 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_eq_zero_of_no_ramifiedFinitePlaces

Documentation

If no finite prime of the base ramifies in the extension, then the narrow finite conductor of the actual idele-class norm subgroup is zero.

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem ideleClassNorm_narrowFiniteConductor_eq_zero_of_no_ramifiedFinitePlaces
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    ideleClassNormNarrowFiniteConductor (K := K) (L := L) = 0

theorem

bigHilbertClassFieldNormSubgroup_le_ideleClassNorm_range_of_no_ramifiedFinitePlaces

L66 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup_le_ideleClassNorm_range_of_no_ramifiedFinitePlaces

Documentation

The norm subgroup of every finite Galois extension unramified at all finite primes contains the big-Hilbert norm subgroup.

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    bigHilbertClassFieldNormSubgroup_le_ideleClassNorm_range_of_no_ramifiedFinitePlaces
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    bigHilbertClassFieldNormSubgroup (K := K) ≤
      (_root_.ideleClassNorm K L).range

def

bigHilbertClassFieldQuotientToIdeleClassNormQuotient

L83 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToIdeleClassNormQuotient

Documentation

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

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def bigHilbertClassFieldQuotientToIdeleClassNormQuotient
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    (IdeleClassGroup K ⧸
        bigHilbertClassFieldNormSubgroup (K := K)) →*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)

theorem

bigHilbertClassFieldQuotientToIdeleClassNormQuotient_mk

L102 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToIdeleClassNormQuotient_mk

Documentation

The big-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
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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem bigHilbertClassFieldQuotientToIdeleClassNormQuotient_mk
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅)
    (x : IdeleClassGroup K) :
    bigHilbertClassFieldQuotientToIdeleClassNormQuotient
        (K := K) (L := L) hunramified
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K)) x) =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K L).range) x

theorem

bigHilbertClassFieldQuotientToIdeleClassNormQuotient_surjective

L117 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToIdeleClassNormQuotient_surjective

Documentation

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

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    bigHilbertClassFieldQuotientToIdeleClassNormQuotient_surjective
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Function.Surjective
      (bigHilbertClassFieldQuotientToIdeleClassNormQuotient
        (K := K) (L := L) hunramified)

theorem

bigHilbertClassFieldQuotientToIdeleClassNormQuotient_ker

L136 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToIdeleClassNormQuotient_ker

Documentation

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

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    bigHilbertClassFieldQuotientToIdeleClassNormQuotient_ker
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    MonoidHom.ker
        (bigHilbertClassFieldQuotientToIdeleClassNormQuotient
          (K := K) (L := L) hunramified) =
      Subgroup.map
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K)))
        ((_root_.ideleClassNorm K L).range)

def

bigHilbertNormImageQuotientEquivIdeleClassNormQuotient

L165 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertNormImageQuotientEquivIdeleClassNormQuotient

Documentation

For an everywhere finite-unramified extension, quotienting the big-Hilbert reciprocity quotient by the image of its 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
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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def bigHilbertNormImageQuotientEquivIdeleClassNormQuotient
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    ((IdeleClassGroup K ⧸
          bigHilbertClassFieldNormSubgroup (K := K)) ⧸
        Subgroup.map
          (QuotientGroup.mk'
            (bigHilbertClassFieldNormSubgroup (K := K)))
          ((_root_.ideleClassNorm K L).range)) ≃*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)

def

narrowClassGroupToIdeleClassNormQuotient

L188 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowClassGroupToIdeleClassNormQuotient

Documentation

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

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def narrowClassGroupToIdeleClassNormQuotient
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    RayClass.NarrowClassGroup K →*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range)

theorem

narrowClassGroupToIdeleClassNormQuotient_surjective

L202 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowClassGroupToIdeleClassNormQuotient_surjective

Documentation

The canonical map from the narrow class group to an everywhere finite-unramified actual norm quotient is surjective.

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem narrowClassGroupToIdeleClassNormQuotient_surjective
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Function.Surjective
      (narrowClassGroupToIdeleClassNormQuotient
        (K := K) (L := L) hunramified)

theorem

ideleClassNormQuotient_card_dvd_narrowClassGroup_card_of_no_ramifiedFinitePlaces

L216 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotient_card_dvd_narrowClassGroup_card_of_no_ramifiedFinitePlaces

Documentation

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

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    ideleClassNormQuotient_card_dvd_narrowClassGroup_card_of_no_ramifiedFinitePlaces
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Nat.card
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) ∣
      Nat.card (RayClass.NarrowClassGroup K)

theorem

narrowClassGroup_card_eq_unramifiedNormKernel_card_mul_normQuotient_card

L244 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowClassGroup_card_eq_unramifiedNormKernel_card_mul_normQuotient_card

Documentation

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

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    narrowClassGroup_card_eq_unramifiedNormKernel_card_mul_normQuotient_card
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Nat.card (RayClass.NarrowClassGroup K) =
      Nat.card
          (MonoidHom.ker
            (narrowClassGroupToIdeleClassNormQuotient
              (K := K) (L := L) hunramified)) *
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K L).range)

theorem

cyclicExtensionDegree_dvd_narrowClassGroup_card_of_no_ramifiedFinitePlaces

L279 ↗

GlobalClassFieldTheory.GlobalClassFields.cyclicExtensionDegree_dvd_narrowClassGroup_card_of_no_ramifiedFinitePlaces

Documentation

The degree of every finite cyclic extension unramified at all finite places divides the order of the narrow class group.

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    cyclicExtensionDegree_dvd_narrowClassGroup_card_of_no_ramifiedFinitePlaces
    [IsCyclic (L ≃ₐ[K] L)]
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Module.finrank K L ∣
      Nat.card (RayClass.NarrowClassGroup K)

theorem

narrowClassGroup_card_eq_unramifiedCyclicNormKernel_card_mul_extensionDegree

L296 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowClassGroup_card_eq_unramifiedCyclicNormKernel_card_mul_extensionDegree

Documentation

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

Source context 7 commands

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

open scoped IsMulCommutative 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] [IsGalois K L]
/-- Keep norm-range quotient normality out of exported declaration types. -/
local instance
    hilbertNormCharacterization_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

theorem
    narrowClassGroup_card_eq_unramifiedCyclicNormKernel_card_mul_extensionDegree
    [IsCyclic (L ≃ₐ[K] L)]
    (hunramified :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Nat.card (RayClass.NarrowClassGroup K) =
      Nat.card
          (MonoidHom.ker
            (narrowClassGroupToIdeleClassNormQuotient
              (K := K) (L := L) hunramified)) *
        Module.finrank K L

Module documentation

Hilbert norm subgroups and unramified extensions

Declarations