NYLL
Module

SmallOriginal.lean

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

Module documentation

Small Hilbert reciprocity over the original number field

The original-base specialization is compiled separately from the realized-base specialization and reuses the shared reciprocity transport provider.

Imports2
Imported by5

Declarations

instance

smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative

L31 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative
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
    smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
theorem

smallHilbertClassField_ideleClassNorm_range_over_original

L40 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassField_ideleClassNorm_range_over_original
Documentation

Over the original number field scalar structure, the actual norm range of the selected small Hilbert class field is exactly the intrinsic small-Hilbert norm subgroup.

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
    smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem smallHilbertClassField_ideleClassNorm_range_over_original :
    (_root_.ideleClassNorm K (smallHilbertClassField K)).range =
      smallHilbertClassFieldNormSubgroup (K := K)
def

smallHilbertClassFieldReciprocityOverOriginalData

L76 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldReciprocityOverOriginalData
Documentation

Global reciprocity for the selected small Hilbert class field over the original number field gives the ordinary ideal class group directly.

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
    smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def
    smallHilbertClassFieldReciprocityOverOriginalData :
    {e : Gal((smallHilbertClassField K) / K) ≃*
        ClassGroup (𝓞 K) //
      ∀ c : IdeleClassGroup K,
        e (globalNormResidueMonoidHom K
            (smallHilbertClassField K) c) =
          smallHilbertClassFieldQuotientEquivClassGroup
            (K := K)
            (QuotientGroup.mk'
              (smallHilbertClassFieldNormSubgroup (K := K)) c)}
def

smallHilbertClassFieldGaloisEquivClassGroupOverOriginal

L99 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldGaloisEquivClassGroupOverOriginal
Documentation

The direct reciprocity equivalence for the small Hilbert class field, using the original number field as the scalar base.

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
    smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def smallHilbertClassFieldGaloisEquivClassGroupOverOriginal :
    Gal((smallHilbertClassField K) / K) ≃*
      ClassGroup (𝓞 K)
theorem

smallHilbertClassFieldGaloisEquivClassGroupOverOriginal_globalNormResidue

L107 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldGaloisEquivClassGroupOverOriginal_globalNormResidue
Documentation

The direct small-Hilbert reciprocity equivalence sends the genuine global norm-residue symbol to its ordinary ideal 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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem
    smallHilbertClassFieldGaloisEquivClassGroupOverOriginal_globalNormResidue
    (c : IdeleClassGroup K) :
    smallHilbertClassFieldGaloisEquivClassGroupOverOriginal
        (K := K)
        (globalNormResidueMonoidHom K
          (smallHilbertClassField K) c) =
      smallHilbertClassFieldQuotientEquivClassGroup
        (K := K)
        (QuotientGroup.mk'
          (smallHilbertClassFieldNormSubgroup (K := K)) c)
theorem

smallHilbertClassFieldGaloisEquivClassGroupOverOriginal_idele

L124 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldGaloisEquivClassGroupOverOriginal_idele
Documentation

On an actual idèle, direct small-Hilbert reciprocity is its ordinary ideal 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
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
local instance
    smallHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem smallHilbertClassFieldGaloisEquivClassGroupOverOriginal_idele
    (a : IdeleGroup K) :
    smallHilbertClassFieldGaloisEquivClassGroupOverOriginal
        (K := K)
        (globalNormResidueMonoidHom K
          (smallHilbertClassField K)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      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.