NYLL
Module

SmallActual.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.HilbertClassFieldReciprocity.SmallActual
6 declarations indexed from sourceView source ↗

Module documentation

Small Hilbert reciprocity over the realized base field

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

Imports2
Imported by4

Declarations

instance

smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative

L31 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
instance
    smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

smallHilbertClassField_ideleClassNorm_range_eq_intrinsic

L39 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_ideleClassNorm_range_eq_intrinsic
Documentation

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

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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem smallHilbertClassField_ideleClassNorm_range_eq_intrinsic :
    (_root_.ideleClassNorm
      (smallHilbertClassFieldBase K)
      (smallHilbertClassField K)).range =
      smallHilbertClassFieldNormSubgroup
        (K := smallHilbertClassFieldBase K)
def

smallHilbertClassFieldReciprocityData

L53 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldReciprocityData
Documentation

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

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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def smallHilbertClassFieldReciprocityData :
    {e : Gal((smallHilbertClassField K) /
          (smallHilbertClassFieldBase K)) ≃*
        ClassGroup (𝓞 K) //
      ∀ c : IdeleClassGroup (smallHilbertClassFieldBase K),
        e (globalNormResidueMonoidHom
            (smallHilbertClassFieldBase K)
            (smallHilbertClassField K) c) =
          smallHilbertClassGroupCongr
            (smallHilbertClassFieldBaseEquiv (K := K)).symm
            (smallHilbertClassFieldQuotientEquivClassGroup
              (K := smallHilbertClassFieldBase K)
              (QuotientGroup.mk'
                (smallHilbertClassFieldNormSubgroup
                  (K := smallHilbertClassFieldBase K)) c))}
def

smallHilbertClassFieldGaloisEquivClassGroup

L83 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldGaloisEquivClassGroup
Documentation

The reciprocity equivalence from the actual small Hilbert Galois group to the ordinary ideal class group of the original number field.

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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def smallHilbertClassFieldGaloisEquivClassGroup :
    Gal((smallHilbertClassField K) /
        (smallHilbertClassFieldBase K)) ≃*
      ClassGroup (𝓞 K)
theorem

smallHilbertClassFieldGaloisEquivClassGroup_globalNormResidue

L94 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldGaloisEquivClassGroup_globalNormResidue
Documentation

Under the small-Hilbert reciprocity equivalence, the actual global norm-residue symbol of an idèle class is its ordinary ideal class, transported back from the concrete base fixed field to the original number field.

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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem smallHilbertClassFieldGaloisEquivClassGroup_globalNormResidue
    (c : IdeleClassGroup (smallHilbertClassFieldBase K)) :
    smallHilbertClassFieldGaloisEquivClassGroup (K := K)
        (globalNormResidueMonoidHom
          (smallHilbertClassFieldBase K)
          (smallHilbertClassField K) c) =
      smallHilbertClassGroupCongr
        (smallHilbertClassFieldBaseEquiv (K := K)).symm
        (smallHilbertClassFieldQuotientEquivClassGroup
          (K := smallHilbertClassFieldBase K)
          (QuotientGroup.mk'
            (smallHilbertClassFieldNormSubgroup
              (K := smallHilbertClassFieldBase K)) c))
theorem

smallHilbertClassFieldGaloisEquivClassGroup_idele

L113 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldGaloisEquivClassGroup_idele
Documentation

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

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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    smallHilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem smallHilbertClassFieldGaloisEquivClassGroup_idele
    (a : IdeleGroup (smallHilbertClassFieldBase K)) :
    smallHilbertClassFieldGaloisEquivClassGroup (K := K)
        (globalNormResidueMonoidHom
          (smallHilbertClassFieldBase K)
          (smallHilbertClassField K)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup
              (smallHilbertClassFieldBase K)) a)) =
      smallHilbertClassGroupCongr
        (smallHilbertClassFieldBaseEquiv (K := K)).symm
        (IdeleGroup.idealClass a)

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