Module

HilbertProductFormula.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.HilbertProductFormula

4 declarations indexed from sourceView source ↗

Module documentation

The global Hilbert product formula

The finite- and infinite-place Hilbert factors constructed in the preceding files all take values in the same group of n-th roots of unity in the base field. Their product is the image, under the global Kummer root character, of the product of the corresponding local Artin factors. Global reciprocity on a principal idele therefore makes this product equal to one.

Imports3

Imported by3

theorem

map_product_mul_finprod

L35 ↗

GlobalClassFieldTheory.Reciprocity.map_product_mul_finprod

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem map_product_mul_finprod
    {I J M N : Type} [Fintype I] [CommMonoid M] [CommMonoid N]
    (chi : M →* N) (f : I → M) (g : J → M)
    (hg : Function.HasFiniteMulSupport g) :
    (∏ i, chi (f i)) * ∏ᶠ j, chi (g j) =
      chi ((∏ i, f i) * ∏ᶠ j, g j)

def

globalHilbertProduct

L45 ↗

GlobalClassFieldTheory.Reciprocity.globalHilbertProduct

Documentation

The product of the Hilbert symbols of two global units over all places. The finite-place part is a genuine finite-support product.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

def globalHilbertProduct
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    nthRootsSubgroup K (n : ℕ)

theorem

globalHilbertProduct_principal

L58 ↗

GlobalClassFieldTheory.Reciprocity.globalHilbertProduct_principal

Documentation

The global Hilbert product of a principal pair is trivial. The proof maps the chosen local Artin product through the global Kummer root character and then uses the finite- and infinite-place comparison theorems.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem globalHilbertProduct_principal
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    globalHilbertProduct K n hnK hmu a b = 1

theorem

hilbertSymbol_allPlaces_product_eq_one

L180 ↗

GlobalClassFieldTheory.Reciprocity.hilbertSymbol_allPlaces_product_eq_one

Documentation

The Hilbert symbols of two global units have product one over all finite and infinite places.

Source context 7 commands

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

open scoped BigOperators IsMulCommutative NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem hilbertSymbol_allPlaces_product_eq_one
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) :
    (∏ v : InfinitePlace K,
        infinitePlaceHilbertSymbol K n v a b) *
      ∏ᶠ v : HeightOneSpectrum (𝓞 K),
        finitePlaceHilbertSymbol K n hnK hmu v a b = 1

Module documentation

The global Hilbert product formula

Declarations

map_product_mul_finprod

globalHilbertProduct

globalHilbertProduct_principal

hilbertSymbol_allPlaces_product_eq_one