Module

InfinitePlace.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlace

4 declarations indexed from sourceView source ↗

Module documentation

Hilbert symbols at infinite places

At a complex place the Hilbert symbol is trivial. At a real place, once the base field contains the relevant roots of unity, the only nontrivial case is the quadratic one: its value is -1 exactly when both arguments are negative. The definition below records that evaluation directly in μₙ(K).

Imports2

Nyll.GaloisCohomology.Kummer.Concrete.RootCharacters
Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Imported by3

def

infinitePlaceHilbertSymbol

L37 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceHilbertSymbol

Documentation

The Hilbert symbol of two global units at an infinite place. Complex places and nonquadratic exponents contribute 1; a real quadratic place contributes -1 precisely when both real embeddings are negative.

Source context 8 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]
open scoped Classical in

Lean source · statement

def infinitePlaceHilbertSymbol
    (n : ℕ+) (v : InfinitePlace K) (a b : Kˣ) :
    nthRootsSubgroup K (n : ℕ)

theorem

infinitePlaceHilbertSymbol_eq_one_of_isComplex

L56 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceHilbertSymbol_eq_one_of_isComplex

Documentation

Every complex infinite place has trivial Hilbert symbol.

Source context 8 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in

Lean source · statement

theorem infinitePlaceHilbertSymbol_eq_one_of_isComplex
    (n : ℕ+) (v : InfinitePlace K) (a b : Kˣ)
    (hv : v.IsComplex) :
    infinitePlaceHilbertSymbol K n v a b = 1

theorem

infinitePlaceHilbertSymbol_eq_one_of_ne_two

L68 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceHilbertSymbol_eq_one_of_ne_two

Documentation

Away from the quadratic exponent, every infinite-place factor is trivial.

Source context 8 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in

Lean source · statement

theorem infinitePlaceHilbertSymbol_eq_one_of_ne_two
    (n : ℕ+) (v : InfinitePlace K) (a b : Kˣ)
    (hn : (n : ℕ) ≠ 2) :
    infinitePlaceHilbertSymbol K n v a b = 1

theorem

infinitePlaceHilbertSymbol_real_apply

L76 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceHilbertSymbol_real_apply

Documentation

Explicit real-place evaluation of the quadratic Hilbert symbol.

Source context 8 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in

Lean source · full declaration

theorem infinitePlaceHilbertSymbol_real_apply
    (n : ℕ+) (v : InfinitePlace K) (a b : Kˣ)
    (hn : (n : ℕ) = 2) (hv : v.IsReal) :
    (infinitePlaceHilbertSymbol K n v a b).1 =
      if InfinitePlace.embedding_of_isReal hv (a : K) < 0 ∧
          InfinitePlace.embedding_of_isReal hv (b : K) < 0 then
        (-1 : Kˣ)
      else
        1 := by
  by_cases ha : InfinitePlace.embedding_of_isReal hv (a : K) < 0
  · by_cases hb : InfinitePlace.embedding_of_isReal hv (b : K) < 0
    · simp [infinitePlaceHilbertSymbol, hn, hv, ha, hb]
    · simp [infinitePlaceHilbertSymbol, hn, hv, ha, hb]
  · simp [infinitePlaceHilbertSymbol, hn, hv, ha]

Module documentation

Hilbert symbols at infinite places

Declarations

infinitePlaceHilbertSymbol

infinitePlaceHilbertSymbol_eq_one_of_isComplex

infinitePlaceHilbertSymbol_eq_one_of_ne_two

infinitePlaceHilbertSymbol_real_apply