NYLL
Module

SmallHilbertClassField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassField
19 declarations indexed from sourceView source ↗

Module documentation

The small Hilbert class field

The small Hilbert class field corresponds to the image in the idele class group of the ideles integral at every finite place. Its reciprocity quotient is canonically the ordinary ideal class group; consequently its order is the class number.

Imports4
Imported by5

Declarations

instance

smallHilbertClassFieldIdeleClassGroupIsMulCommutative

L36 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldIdeleClassGroupIsMulCommutative
Documentation

Fix the canonical commutative idèle-class structure used by the Hilbert class-field quotients in this module.

Source context 6 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

smallHilbertClassFieldNormSubgroup

L44 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup
Documentation

The norm subgroup defining the small Hilbert class field. The principal subgroup is included before passing to the idele class group so that the third-isomorphism equivalence applies literally.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def smallHilbertClassFieldNormSubgroup :
    Subgroup (IdeleClassGroup K)
def

smallHilbertClassFieldQuotientEquivClassGroup

L53 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientEquivClassGroup
Documentation

The quotient by the small-Hilbert norm subgroup is the ordinary ideal class group.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def smallHilbertClassFieldQuotientEquivClassGroup :
    IdeleClassGroup K ⧸
        smallHilbertClassFieldNormSubgroup (K := K) ≃*
      ClassGroup (𝓞 K)
theorem

smallHilbertClassFieldNormSubgroup_isOpen

L65 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup_isOpen
Documentation

The small-Hilbert norm subgroup is open.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem smallHilbertClassFieldNormSubgroup_isOpen :
    IsOpen
      ((smallHilbertClassFieldNormSubgroup (K := K) :
        Subgroup (IdeleClassGroup K)) :
        Set (IdeleClassGroup K))
theorem

smallHilbertClassFieldNormSubgroup_isClosed

L95 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup_isClosed
Documentation

The small-Hilbert norm subgroup is closed.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem smallHilbertClassFieldNormSubgroup_isClosed :
    IsClosed
      ((smallHilbertClassFieldNormSubgroup (K := K) :
        Subgroup (IdeleClassGroup K)) :
        Set (IdeleClassGroup K))
instance

smallHilbertClassFieldNormSubgroupFiniteIndex

L104 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroupFiniteIndex
Documentation

The small-Hilbert norm subgroup has finite index.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance smallHilbertClassFieldNormSubgroupFiniteIndex :
    (smallHilbertClassFieldNormSubgroup (K := K)).FiniteIndex
theorem

smallHilbertClassFieldQuotient_card_eq_classNumber

L116 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotient_card_eq_classNumber
Documentation

The order of the small-Hilbert reciprocity quotient is the class number of K.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem smallHilbertClassFieldQuotient_card_eq_classNumber :
    Nat.card
        (IdeleClassGroup K ⧸
          smallHilbertClassFieldNormSubgroup (K := K)) =
      NumberField.classNumber K
theorem

bigHilbertClassFieldNormSubgroup_le_smallHilbertClassFieldNormSubgroup

L129 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldNormSubgroup_le_smallHilbertClassFieldNormSubgroup
Documentation

The big-Hilbert norm subgroup is contained in the small-Hilbert norm subgroup. Under class-field duality this is the inclusion of the small Hilbert class field into the big Hilbert class field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    bigHilbertClassFieldNormSubgroup_le_smallHilbertClassFieldNormSubgroup :
    bigHilbertClassFieldNormSubgroup (K := K) ≤
      smallHilbertClassFieldNormSubgroup (K := K)
theorem

smallHilbertClassFieldNormSubgroup_isDefiningModulus

L144 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldNormSubgroup_isDefiningModulus
Documentation

Modulus zero is a defining modulus for the small-Hilbert norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem smallHilbertClassFieldNormSubgroup_isDefiningModulus :
    IsDefiningModulus
      (smallHilbertClassFieldNormSubgroup (K := K))
      (0 : RayClass.Modulus K)
def

smallHilbertClassFieldConductorialSubgroup

L162 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldConductorialSubgroup
Documentation

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

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def smallHilbertClassFieldConductorialSubgroup :
    ConductorialSubgroup K
def

bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient

L169 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
Documentation

The canonical quotient transition from the big-Hilbert reciprocity quotient onto the small-Hilbert reciprocity quotient.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def
    bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient :
    (IdeleClassGroup K ⧸
        bigHilbertClassFieldNormSubgroup (K := K)) →*
      (IdeleClassGroup K ⧸
        smallHilbertClassFieldNormSubgroup (K := K))
theorem

bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_mk

L192 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_mk
Documentation

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

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_mk
    (x : IdeleClassGroup K) :
    bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
        (K := K)
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K)) x) =
      QuotientGroup.mk'
        (smallHilbertClassFieldNormSubgroup (K := K)) x
theorem

bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_surjective

L204 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_surjective
Documentation

The canonical transition from the big-Hilbert quotient to the small-Hilbert quotient is surjective.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_surjective :
    Function.Surjective
      (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
        (K := K))
theorem

bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_ker

L220 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_ker
Documentation

The kernel of the canonical big-to-small Hilbert quotient transition is the image of the small-Hilbert norm subgroup modulo the big-Hilbert norm subgroup.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient_ker :
    MonoidHom.ker
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K)) =
      Subgroup.map
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K)))
        (smallHilbertClassFieldNormSubgroup (K := K))
theorem

smallHilbertClassFieldQuotient_card_dvd_bigHilbertClassFieldQuotient_card

L234 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotient_card_dvd_bigHilbertClassFieldQuotient_card
Documentation

The order of the small-Hilbert reciprocity quotient divides the order of the big-Hilbert reciprocity quotient.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem smallHilbertClassFieldQuotient_card_dvd_bigHilbertClassFieldQuotient_card :
    Nat.card
        (IdeleClassGroup K ⧸
          smallHilbertClassFieldNormSubgroup (K := K)) ∣
      Nat.card
        (IdeleClassGroup K ⧸
          bigHilbertClassFieldNormSubgroup (K := K))
theorem

classNumber_dvd_narrowClassGroup_card

L247 ↗
GlobalClassFieldTheory.GlobalClassFields.classNumber_dvd_narrowClassGroup_card
Documentation

The class number divides the order of the narrow class group.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem classNumber_dvd_narrowClassGroup_card :
    NumberField.classNumber K ∣
      Nat.card (RayClass.NarrowClassGroup K)
theorem

narrowClassGroup_card_eq_bigToSmallKernel_card_mul_classNumber

L270 ↗
GlobalClassFieldTheory.GlobalClassFields.narrowClassGroup_card_eq_bigToSmallKernel_card_mul_classNumber
Documentation

The kernel of the big-to-small Hilbert quotient transition measures the exact difference between the narrow and ordinary class numbers.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem narrowClassGroup_card_eq_bigToSmallKernel_card_mul_classNumber :
    Nat.card (RayClass.NarrowClassGroup K) =
      Nat.card
          (MonoidHom.ker
            (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
              (K := K))) *
        NumberField.classNumber K
theorem

narrowClassGroup_card_eq_smallHilbertNormImage_card_mul_classNumber

L313 ↗
GlobalClassFieldTheory.GlobalClassFields.narrowClassGroup_card_eq_smallHilbertNormImage_card_mul_classNumber
Documentation

The exact difference between the narrow and ordinary class numbers is the order of the image of the small-Hilbert norm subgroup in the big-Hilbert reciprocity quotient.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    narrowClassGroup_card_eq_smallHilbertNormImage_card_mul_classNumber :
    Nat.card (RayClass.NarrowClassGroup K) =
      Nat.card
          (Subgroup.map
            (QuotientGroup.mk'
              (bigHilbertClassFieldNormSubgroup (K := K)))
            (smallHilbertClassFieldNormSubgroup (K := K))) *
        NumberField.classNumber K
theorem

smallHilbertClassField_narrowFiniteConductor

L327 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_narrowFiniteConductor
Documentation

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

Source context 7 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
variable {K : Type*} [Field K] [NumberField K]
/-- Fix the canonical commutative idèle-class structure used by the Hilbert
class-field quotients in this module. -/
local instance smallHilbertClassFieldIdeleClassGroupIsMulCommutative
    {F : Type*} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem smallHilbertClassField_narrowFiniteConductor :
    (smallHilbertClassFieldConductorialSubgroup
      (K := K)).narrowFiniteConductor = 0

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.