Module

BigActual.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldReciprocity.BigActual

6 declarations indexed from sourceView source ↗

Module documentation

Big Hilbert reciprocity over the realized base field

This leaf specializes the shared reciprocity transport to the actual base field of the selected big Hilbert class field.

Imports3

Imported by4

instance

bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

L31 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

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 Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem

bigHilbertClassField_ideleClassNorm_range_eq_intrinsic

L39 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_ideleClassNorm_range_eq_intrinsic

Documentation

The actual norm range of the selected big Hilbert class field is the intrinsic big-Hilbert norm subgroup of its actual base field.

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 Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

Lean source · statement

theorem bigHilbertClassField_ideleClassNorm_range_eq_intrinsic :
    (_root_.ideleClassNorm
      (bigHilbertClassFieldBase K)
      (bigHilbertClassField K)).range =
      bigHilbertClassFieldNormSubgroup
        (K := bigHilbertClassFieldBase K)

def

bigHilbertClassFieldReciprocityData

L53 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldReciprocityData

Documentation

Global reciprocity identifies the genuine Galois group of the selected big Hilbert class field with the narrow ideal class group of the original number field.

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 Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

Lean source · statement

def bigHilbertClassFieldReciprocityData :
    {e : Gal((bigHilbertClassField K) /
          (bigHilbertClassFieldBase K)) ≃*
        RayClass.NarrowClassGroup K //
      ∀ c : IdeleClassGroup (bigHilbertClassFieldBase K),
        e (globalNormResidueMonoidHom
            (bigHilbertClassFieldBase K)
            (bigHilbertClassField K) c) =
          bigHilbertNarrowClassGroupCongr
            (bigHilbertClassFieldBaseEquiv (K := K)).symm
            (bigHilbertClassFieldQuotientEquivNarrowClassGroup
              (K := bigHilbertClassFieldBase K)
              (QuotientGroup.mk'
                (bigHilbertClassFieldNormSubgroup
                  (K := bigHilbertClassFieldBase K)) c))}

def

bigHilbertClassFieldGaloisEquivNarrowClassGroup

L83 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldGaloisEquivNarrowClassGroup

Documentation

The reciprocity equivalence from the actual big Hilbert Galois group to the narrow class group of the original number field.

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 Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

Lean source · statement

def bigHilbertClassFieldGaloisEquivNarrowClassGroup :
    Gal((bigHilbertClassField K) /
        (bigHilbertClassFieldBase K)) ≃*
      RayClass.NarrowClassGroup K

theorem

bigHilbertClassFieldGaloisEquivNarrowClassGroup_globalNormResidue

L93 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldGaloisEquivNarrowClassGroup_globalNormResidue

Documentation

Under big-Hilbert reciprocity, the actual global norm-residue symbol is the narrow ideal class of its idèle-class representative, transported back to the original number field.

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 Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

Lean source · statement

theorem bigHilbertClassFieldGaloisEquivNarrowClassGroup_globalNormResidue
    (c : IdeleClassGroup (bigHilbertClassFieldBase K)) :
    bigHilbertClassFieldGaloisEquivNarrowClassGroup (K := K)
        (globalNormResidueMonoidHom
          (bigHilbertClassFieldBase K)
          (bigHilbertClassField K) c) =
      bigHilbertNarrowClassGroupCongr
        (bigHilbertClassFieldBaseEquiv (K := K)).symm
        (bigHilbertClassFieldQuotientEquivNarrowClassGroup
          (K := bigHilbertClassFieldBase K)
          (QuotientGroup.mk'
            (bigHilbertClassFieldNormSubgroup
              (K := bigHilbertClassFieldBase K)) c))

theorem

bigHilbertClassFieldGaloisEquivNarrowClassGroup_idele

L112 ↗

GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldGaloisEquivNarrowClassGroup_idele

Documentation

Representative form of big-Hilbert reciprocity: the global norm-residue symbol of an actual idèle maps to its narrow ideal class, with only the canonical base-field transport remaining.

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 Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

Lean source · statement

theorem bigHilbertClassFieldGaloisEquivNarrowClassGroup_idele
    (a : IdeleGroup (bigHilbertClassFieldBase K)) :
    bigHilbertClassFieldGaloisEquivNarrowClassGroup (K := K)
        (globalNormResidueMonoidHom
          (bigHilbertClassFieldBase K)
          (bigHilbertClassField K)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup
              (bigHilbertClassFieldBase K)) a)) =
      bigHilbertNarrowClassGroupCongr
        (bigHilbertClassFieldBaseEquiv (K := K)).symm
        (QuotientGroup.mk'
          (RayClass.narrowDenominator
            (K := bigHilbertClassFieldBase K)) a)

Module documentation

Big Hilbert reciprocity over the realized base field

Declarations

bigHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

bigHilbertClassField_ideleClassNorm_range_eq_intrinsic

bigHilbertClassFieldReciprocityData

bigHilbertClassFieldGaloisEquivNarrowClassGroup

bigHilbertClassFieldGaloisEquivNarrowClassGroup_globalNormResidue

bigHilbertClassFieldGaloisEquivNarrowClassGroup_idele