NYLL
Module

BigOriginal.lean

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

Module documentation

Big 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 by4

Declarations

instance

bigHilbertClassFieldReciprocityOverOriginalIsMulCommutative

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

bigHilbertClassField_ideleClassNorm_range_over_original

L40 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassField_ideleClassNorm_range_over_original
Documentation

Over the original number field scalar structure, the actual norm range of the selected big Hilbert class field is exactly the intrinsic big-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
    bigHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem bigHilbertClassField_ideleClassNorm_range_over_original :
    (_root_.ideleClassNorm K (bigHilbertClassField K)).range =
      bigHilbertClassFieldNormSubgroup (K := K)
def

bigHilbertClassFieldReciprocityOverOriginalData

L76 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldReciprocityOverOriginalData
Documentation

Global reciprocity for the selected big Hilbert class field over the original number field gives the narrow ideal class group directly, without a residual fixed-field transport.

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
    bigHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def
    bigHilbertClassFieldReciprocityOverOriginalData :
    {e : Gal((bigHilbertClassField K) / K) ≃*
        RayClass.NarrowClassGroup K //
      ∀ c : IdeleClassGroup K,
        e (globalNormResidueMonoidHom K
            (bigHilbertClassField K) c) =
          bigHilbertClassFieldQuotientEquivNarrowClassGroup
            (K := K)
            (QuotientGroup.mk'
              (bigHilbertClassFieldNormSubgroup (K := K)) c)}
def

bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal

L99 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal
Documentation

The direct reciprocity equivalence for the big 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
    bigHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
def
    bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal :
    Gal((bigHilbertClassField K) / K) ≃*
      RayClass.NarrowClassGroup K
theorem

bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_globalNormResidue

L108 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_globalNormResidue
Documentation

The direct big-Hilbert reciprocity equivalence sends the genuine global norm-residue symbol to its narrow 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
    bigHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem
    bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_globalNormResidue
    (c : IdeleClassGroup K) :
    bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal
        (K := K)
        (globalNormResidueMonoidHom K
          (bigHilbertClassField K) c) =
      bigHilbertClassFieldQuotientEquivNarrowClassGroup
        (K := K)
        (QuotientGroup.mk'
          (bigHilbertClassFieldNormSubgroup (K := K)) c)
theorem

bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_idele

L125 ↗
GlobalClassFieldTheory.GlobalClassFields.bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_idele
Documentation

On an actual idèle, direct big-Hilbert reciprocity is its narrow 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
    bigHilbertClassFieldReciprocityOverOriginalIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  hilbertClassFieldReciprocityIdeleClassGroupIsMulCommutative
Lean source · statement
theorem bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal_idele
    (a : IdeleGroup K) :
    bigHilbertClassFieldGaloisEquivNarrowClassGroupOverOriginal
        (K := K)
        (globalNormResidueMonoidHom K
          (bigHilbertClassField K)
          (QuotientGroup.mk'
            (IdeleGroup.principalSubgroup K) a)) =
      QuotientGroup.mk'
        (RayClass.narrowDenominator (K := K)) a

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