NYLL
Module

ProductFormula.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.ProductFormula
8 declarations indexed from sourceView source ↗

Module documentation

The local--global norm-symbol bridge

This file isolates the exact quotient calculation used by the Hilbert-symbol product formula. The one-place embedding sends the chosen local norm group directly into the ordinary idele-class norm group, so it descends without an intermediate raw-idele quotient. The resulting character identity gives the finite-support and principal-idèle product identities for every character of that target.

Imports3
Imported by2

Declarations

theorem

productFormulaIdeleClassGroupIsMulCommutative

L31 ↗
GlobalClassFieldTheory.Reciprocity.productFormulaIdeleClassGroupIsMulCommutative
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
Lean source · statement
theorem productFormulaIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
def

finitePlaceNormQuotientToGlobalClass

L46 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormQuotientToGlobalClass
Documentation

The one-place embedding, descended directly from the chosen local norm quotient to the ordinary idele-class norm quotient.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] productFormulaIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def finitePlaceNormQuotientToGlobalClass
    (v : HeightOneSpectrum (𝓞 K)) :
    ChosenFinitePlaceNormQuotient
      (K := K) (L := L) v →*
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range
theorem

finitePlaceNormQuotientToGlobalClass_localClass

L83 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceNormQuotientToGlobalClass_localClass
Documentation

Exact local--global compatibility on representatives.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] productFormulaIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem finitePlaceNormQuotientToGlobalClass_localClass
    (v : HeightOneSpectrum (𝓞 K))
    (a : (v.adicCompletion K)ˣ) :
    finitePlaceNormQuotientToGlobalClass
        (K := K) (L := L) v
        (finitePlaceTensorNormClass
          (K := K) (L := L) v a) =
      globalNormClassFromIdele K L
        (finitePlaceIdele v a)
def

finitePlaceGlobalSymbol

L97 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalSymbol
Documentation

A character of the global class norm quotient, restricted to the one-place class at v.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] productFormulaIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
def finitePlaceGlobalSymbol
    {A : Type*} [CommGroup A]
    (chi :
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) →* A)
    (v : HeightOneSpectrum (𝓞 K)) :
    (v.adicCompletion K)ˣ →* A
theorem

finitePlaceGlobalSymbol_eq_localNormClass

L111 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalSymbol_eq_localNormClass
Documentation

The one-place global symbol is the character of the transported local norm class.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] productFormulaIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem finitePlaceGlobalSymbol_eq_localNormClass
    {A : Type*} [CommGroup A]
    (chi :
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) →* A)
    (v : HeightOneSpectrum (𝓞 K))
    (a : (v.adicCompletion K)ˣ) :
    finitePlaceGlobalSymbol (K := K) (L := L) chi v a =
      chi
        (finitePlaceNormQuotientToGlobalClass
          (K := K) (L := L) v
          (finitePlaceTensorNormClass
            (K := K) (L := L) v a))
theorem

finitePlaceGlobalSymbol_finiteLocalFamily

L131 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalSymbol_finiteLocalFamily
Documentation

Finite-support form of the product formula for a global norm-quotient character.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] productFormulaIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem finitePlaceGlobalSymbol_finiteLocalFamily
    {A : Type*} [CommGroup A]
    (chi :
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) →* A)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ) :
    ∏ v : ↥S,
        finitePlaceGlobalSymbol (K := K) (L := L) chi v.1 (a v) =
      chi
        (globalNormClassFromIdele K L
          (IdeleGroup.ideleOfFiniteLocalFamily S a))
theorem

globalNormQuotientCharacter_principal

L151 ↗
GlobalClassFieldTheory.Reciprocity.globalNormQuotientCharacter_principal
Documentation

A global norm-quotient character is trivial on a principal idèle.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] productFormulaIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem globalNormQuotientCharacter_principal
    {A : Type*} [CommGroup A]
    (chi :
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) →* A)
    (x : Kˣ) :
  chi
        (globalNormClassFromIdele K L
          (IdeleGroup.principalIdele K x)) = 1
theorem

finitePlaceGlobalSymbol_product_eq_one_of_eq_principal

L166 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceGlobalSymbol_product_eq_one_of_eq_principal
Documentation

Exact bridge from a finite local representative of a principal global norm class to the product-one identity. The premise is a concrete equality in C_K / N C_L, not a product-formula assumption.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
open IdeleGroup RelativeIdeleGroup
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
attribute [local instance] productFormulaIdeleClassGroupIsMulCommutative
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem finitePlaceGlobalSymbol_product_eq_one_of_eq_principal
    {A : Type*} [CommGroup A]
    (chi :
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) →* A)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : ∀ v : ↥S, (v.1.adicCompletion K)ˣ)
    (x : Kˣ)
    (hprincipal :
      globalNormClassFromIdele K L
          (IdeleGroup.ideleOfFiniteLocalFamily S a) =
        globalNormClassFromIdele K L
          (IdeleGroup.principalIdele K x)) :
    ∏ v : ↥S,
        finitePlaceGlobalSymbol (K := K) (L := L) chi v.1 (a v) = 1

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