NYLL
Module

HilbertClassFieldComparison.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldComparison
24 declarations indexed from sourceView source ↗

Module documentation

Comparison of the big and small Hilbert class fields

This file identifies the canonical transition from the big-Hilbert reciprocity quotient to the small-Hilbert reciprocity quotient with the canonical map from the narrow class group to the ordinary class group. It then transports the archimedean sign exact sequence to a precise description of the kernel of that transition.

Imports1
Imported by7

Declarations

theorem

hilbertClassFieldComparison_ideleClassGroupIsMulCommutative

L34 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
Documentation

Fix the canonical commutativity needed for Hilbert norm-subgroup quotients in this module.

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 : Type*} [Field K] [NumberField K]
Lean source · statement
theorem hilbertClassFieldComparison_ideleClassGroupIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)
instance

hilbertClassFieldComparison_realSignGroupIsMulCommutative

L41 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldComparison_realSignGroupIsMulCommutative
Documentation

Keep the real-sign quotient normality instance stable across declarations.

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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
Lean source · statement
instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K)
theorem

bigHilbertClassFieldQuotientEquivNarrowClassGroup_mk

L49 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldQuotientEquivNarrowClassGroup_mk
Documentation

On an idele representative, the big-Hilbert quotient equivalence is the canonical representative in the narrow class group.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigHilbertClassFieldQuotientEquivNarrowClassGroup_mk
    (a : IdeleGroup K) :
    bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K))
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      QuotientGroup.mk'
        (RayClass.narrowDenominator (K := K)) a
theorem

smallHilbertClassFieldQuotientEquivClassGroup_mk

L64 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldQuotientEquivClassGroup_mk
Documentation

On an idele representative, the small-Hilbert quotient equivalence is the ordinary ideal-class map.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem smallHilbertClassFieldQuotientEquivClassGroup_mk
    (a : IdeleGroup K) :
    smallHilbertClassFieldQuotientEquivClassGroup
        (K := K)
        (QuotientGroup.mk'
          (smallHilbertClassFieldNormSubgroup (K := K))
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      IdeleGroup.idealClass a
theorem

bigToSmallHilbertQuotient_compatible_with_narrowToClassGroup

L78 ↗
GlobalClassFieldTheory.GlobalClassFields.bigToSmallHilbertQuotient_compatible_with_narrowToClassGroup
Documentation

Under the canonical quotient equivalences, the big-to-small Hilbert transition is the map from the narrow class group to the ordinary class group.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigToSmallHilbertQuotient_compatible_with_narrowToClassGroup
    (q : IdeleClassGroup K ⧸
      bigHilbertClassFieldNormSubgroup (K := K)) :
    smallHilbertClassFieldQuotientEquivClassGroup
        (K := K)
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K) q) =
      RayClass.narrowToClassGroup
        (bigHilbertClassFieldQuotientEquivNarrowClassGroup
          (K := K) q)
theorem

bigToSmallHilbertQuotient_compatibility

L101 ↗
GlobalClassFieldTheory.GlobalClassFields.bigToSmallHilbertQuotient_compatibility
Documentation

Homomorphism form of the compatibility between the Hilbert quotient transition and the narrow-to-ordinary class-group map.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigToSmallHilbertQuotient_compatibility :
    (smallHilbertClassFieldQuotientEquivClassGroup
        (K := K)).toMonoidHom.comp
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K)) =
      (RayClass.narrowToClassGroup (K := K)).comp
        (bigHilbertClassFieldQuotientEquivNarrowClassGroup
          (K := K)).toMonoidHom
def

realSignToBigHilbertClassFieldQuotient

L116 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToBigHilbertClassFieldQuotient
Documentation

The canonical map from real sign classes to the big-Hilbert reciprocity quotient.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def realSignToBigHilbertClassFieldQuotient :
    RayClass.realSignGroup K →*
      (IdeleClassGroup K ⧸
        bigHilbertClassFieldNormSubgroup (K := K))
theorem

realSignToBigHilbertClassFieldQuotient_apply

L127 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToBigHilbertClassFieldQuotient_apply
Documentation

The real-sign map to the big-Hilbert quotient is the composite used in its definition.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem realSignToBigHilbertClassFieldQuotient_apply
    (s : RayClass.realSignGroup K) :
    realSignToBigHilbertClassFieldQuotient (K := K) s =
      (bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)).symm
          (RayClass.signToNarrow (K := K) s)
theorem

integralUnitSign_range_eq_realSignToBigHilbertClassFieldQuotient_ker

L137 ↗
GlobalClassFieldTheory.GlobalClassFields.integralUnitSign_range_eq_realSignToBigHilbertClassFieldQuotient_ker
Documentation

The kernel of the real-sign map to the big-Hilbert quotient is the image of the sign classes of global integral units.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    integralUnitSign_range_eq_realSignToBigHilbertClassFieldQuotient_ker :
    (RayClass.integralUnitSignToRealSign (K := K)).range =
      (realSignToBigHilbertClassFieldQuotient (K := K)).ker
theorem

realSignToBigHilbertClassFieldQuotient_range_le_bigToSmallHilbertKernel

L163 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToBigHilbertClassFieldQuotient_range_le_bigToSmallHilbertKernel
Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    realSignToBigHilbertClassFieldQuotient_range_le_bigToSmallHilbertKernel :
    (realSignToBigHilbertClassFieldQuotient (K := K)).range ≤
      MonoidHom.ker
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K))
theorem

bigToSmallHilbertKernel_le_realSignToBigHilbertClassFieldQuotient_range

L184 ↗
GlobalClassFieldTheory.GlobalClassFields.bigToSmallHilbertKernel_le_realSignToBigHilbertClassFieldQuotient_range
Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    bigToSmallHilbertKernel_le_realSignToBigHilbertClassFieldQuotient_range :
    MonoidHom.ker
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K)) ≤
      (realSignToBigHilbertClassFieldQuotient (K := K)).range
theorem

realSignToBigHilbertClassFieldQuotient_range_eq_bigToSmallHilbertKernel

L218 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToBigHilbertClassFieldQuotient_range_eq_bigToSmallHilbertKernel
Documentation

The image of the real-sign map in the big-Hilbert quotient is exactly the kernel of the transition to the small-Hilbert quotient.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem
    realSignToBigHilbertClassFieldQuotient_range_eq_bigToSmallHilbertKernel :
    (realSignToBigHilbertClassFieldQuotient (K := K)).range =
      MonoidHom.ker
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K))
theorem

hilbertClassFieldSign_exact_sequence

L235 ↗
GlobalClassFieldTheory.GlobalClassFields.hilbertClassFieldSign_exact_sequence
Documentation

The archimedean sign exact sequence written directly on the big and small Hilbert reciprocity quotients:

1 → unit signs → real signs → big Hilbert quotient → small Hilbert quotient → 1.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem hilbertClassFieldSign_exact_sequence :
    Function.Injective
        (RayClass.integralUnitSignToRealSign (K := K)) ∧
      (RayClass.integralUnitSignToRealSign (K := K)).range =
        (realSignToBigHilbertClassFieldQuotient (K := K)).ker ∧
      (realSignToBigHilbertClassFieldQuotient (K := K)).range =
        MonoidHom.ker
          (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
            (K := K)) ∧
      Function.Surjective
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K))
theorem

bigHilbertQuotientEquiv_mem_narrowClassKernel

L256 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertQuotientEquiv_mem_narrowClassKernel
Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigHilbertQuotientEquiv_mem_narrowClassKernel
    (q : MonoidHom.ker
      (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
        (K := K))) :
    bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K) q.1 ∈
      MonoidHom.ker (RayClass.narrowToClassGroup (K := K))
theorem

bigHilbertQuotientEquiv_symm_mem_bigToSmallKernel

L269 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertQuotientEquiv_symm_mem_bigToSmallKernel
Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigHilbertQuotientEquiv_symm_mem_bigToSmallKernel
    (c : MonoidHom.ker
      (RayClass.narrowToClassGroup (K := K))) :
    (bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)).symm c.1 ∈
      MonoidHom.ker
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K))
def

bigToSmallHilbertKernelEquivNarrowClassKernel

L289 ↗
GlobalClassFieldTheory.GlobalClassFields.bigToSmallHilbertKernelEquivNarrowClassKernel
Documentation

The kernel of the big-to-small Hilbert quotient transition is canonically the kernel of the map from narrow to ordinary ideal classes.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · full declaration
def bigToSmallHilbertKernelEquivNarrowClassKernel :
    MonoidHom.ker
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K)) ≃*
      MonoidHom.ker (RayClass.narrowToClassGroup (K := K)) where
  toFun q :=
    ⟨bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K) q.1,
      bigHilbertQuotientEquiv_mem_narrowClassKernel
        (K := K) q⟩
  invFun c :=
    ⟨(bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)).symm c.1,
      bigHilbertQuotientEquiv_symm_mem_bigToSmallKernel
        (K := K) c⟩
  left_inv q := by
    apply Subtype.ext
    exact
      (bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)).symm_apply_apply q.1
  right_inv c := by
    apply Subtype.ext
    exact
      (bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)).apply_symm_apply c.1
  map_mul' q r := by
    apply Subtype.ext
    exact
      (bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)).map_mul q.1 r.1
theorem

signToNarrow_mem_narrowClassKernel

L320 ↗
GlobalClassFieldTheory.GlobalClassFields.signToNarrow_mem_narrowClassKernel
Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem signToNarrow_mem_narrowClassKernel
    (s : RayClass.realSignGroup K) :
    RayClass.signToNarrow (K := K) s ∈
      MonoidHom.ker (RayClass.narrowToClassGroup (K := K))
def

realSignToNarrowClassKernel

L331 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToNarrowClassKernel
Documentation

The real-sign map with codomain restricted to the kernel of the narrow-to-ordinary class-group map.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · full declaration
def realSignToNarrowClassKernel :
    RayClass.realSignGroup K →*
      MonoidHom.ker (RayClass.narrowToClassGroup (K := K)) where
  toFun s :=
    ⟨RayClass.signToNarrow (K := K) s,
      signToNarrow_mem_narrowClassKernel (K := K) s⟩
  map_one' := by
    apply Subtype.ext
    exact map_one (RayClass.signToNarrow (K := K))
  map_mul' s t := by
    apply Subtype.ext
    exact map_mul (RayClass.signToNarrow (K := K)) s t
theorem

realSignToNarrowClassKernel_apply

L347 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToNarrowClassKernel_apply
Documentation

The restricted real-sign map has the same underlying narrow ideal class as RayClass.signToNarrow.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem realSignToNarrowClassKernel_apply
    (s : RayClass.realSignGroup K) :
    (realSignToNarrowClassKernel (K := K) s :
      RayClass.NarrowClassGroup K) =
      RayClass.signToNarrow (K := K) s
theorem

realSignToNarrowClassKernel_surjective

L356 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToNarrowClassKernel_surjective
Documentation

Every narrow ideal class mapping trivially to the ordinary class group is represented by a real sign class.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem realSignToNarrowClassKernel_surjective :
    Function.Surjective
      (realSignToNarrowClassKernel (K := K))
theorem

realSignToNarrowClassKernel_ker

L371 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignToNarrowClassKernel_ker
Documentation

Restricting the codomain of the real-sign map does not change its kernel.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem realSignToNarrowClassKernel_ker :
    (realSignToNarrowClassKernel (K := K)).ker =
      (RayClass.signToNarrow (K := K)).ker
def

realSignModuloIntegralUnitSignsEquivNarrowClassKernel

L385 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignModuloIntegralUnitSignsEquivNarrowClassKernel
Documentation

The kernel of the narrow-to-ordinary class-group map is the quotient of real sign classes by the sign classes of global integral units.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def realSignModuloIntegralUnitSignsEquivNarrowClassKernel :
    RayClass.realSignGroup K ⧸
        (RayClass.integralUnitSignToRealSign (K := K)).range ≃*
      MonoidHom.ker (RayClass.narrowToClassGroup (K := K))
def

realSignModuloIntegralUnitSignsEquivBigToSmallHilbertKernel

L409 ↗
GlobalClassFieldTheory.GlobalClassFields.realSignModuloIntegralUnitSignsEquivBigToSmallHilbertKernel
Documentation

The relative big/small Hilbert kernel is exactly the quotient of real sign classes by the sign classes contributed by global integral units.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
def realSignModuloIntegralUnitSignsEquivBigToSmallHilbertKernel :
    RayClass.realSignGroup K ⧸
        (RayClass.integralUnitSignToRealSign (K := K)).range ≃*
      MonoidHom.ker
        (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
          (K := K))
theorem

bigToSmallHilbertKernel_card_eq_realSignQuotient_card

L422 ↗
GlobalClassFieldTheory.GlobalClassFields.bigToSmallHilbertKernel_card_eq_realSignQuotient_card
Documentation

The order of the relative big/small Hilbert kernel is the order of the real-sign quotient modulo signs of global integral units.

Source context 8 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 : Type*} [Field K] [NumberField K]
attribute [local instance] hilbertClassFieldComparison_ideleClassGroupIsMulCommutative
/-- Keep the real-sign quotient normality instance stable across declarations. -/
local instance
    hilbertClassFieldComparison_realSignGroupIsMulCommutative :
    IsMulCommutative (RayClass.realSignGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
theorem bigToSmallHilbertKernel_card_eq_realSignQuotient_card :
    Nat.card
        (MonoidHom.ker
          (bigHilbertClassFieldQuotientToSmallHilbertClassFieldQuotient
            (K := K))) =
      Nat.card
        (RayClass.realSignGroup K ⧸
          (RayClass.integralUnitSignToRealSign (K := K)).range)

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