NYLL
Module

Core.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.Core
13 declarations indexed from sourceView source ↗

Module documentation

Global-place Hilbert symbols

This module starts the local-to-global Hilbert-symbol layer. At a finite place, global units are mapped into the canonical absolute-value completion, the genuine local Hilbert symbol is evaluated there, and its value is transported back to the roots of unity in the number field.

The later local--global comparison can therefore identify this intrinsically local definition with the root character of the finite-place global Artin automorphism without building that comparison into the definition.

Imports3
Imported by2

Declarations

theorem

rootQuotient_eq_of_same_pow_of_primitiveRoots

L44 ↗
GlobalClassFieldTheory.Reciprocity.rootQuotient_eq_of_same_pow_of_primitiveRoots
Documentation

A Kummer root quotient does not depend on the chosen n-th root once the base field contains a primitive n-th root of unity. This is the root-choice transport leaf used by the finite-place local--global comparison.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem rootQuotient_eq_of_same_pow_of_primitiveRoots
    {L : Type} [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (u u' : Lˣ)
    (hu : u ^ (n : ℕ) =
      Units.map (algebraMap K L).toMonoidHom a)
    (hu' : u' ^ (n : ℕ) =
      Units.map (algebraMap K L).toMonoidHom a)
    (sigma : Gal(L/K)) :
    rootQuotient (K := K) (L := L) u sigma =
      rootQuotient (K := K) (L := L) u' sigma
theorem

rootQuotient_map_algEquiv

L71 ↗
GlobalClassFieldTheory.Reciprocity.rootQuotient_map_algEquiv
Documentation

Conjugating a Galois automorphism through an algebra equivalence carries the corresponding root quotient through the same equivalence.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem rootQuotient_map_algEquiv
    {L E : Type} [Field L] [Field E] [Algebra K L] [Algebra K E]
    (e : L ≃ₐ[K] E) (u : Lˣ) (sigma : Gal(L/K)) :
    rootQuotient (K := K) (L := E)
        (Units.map e.toMonoidHom u) (AlgEquiv.autCongr e sigma) =
      Units.map e.toMonoidHom
        (rootQuotient (K := K) (L := L) u sigma)
theorem

isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top_of_primitiveRoots

L84 ↗
GlobalClassFieldTheory.Reciprocity.isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top_of_primitiveRoots
Documentation

A field generated by one n-th root is the splitting field of its Kummer polynomial as soon as the base field already contains a primitive n-th root of unity.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top_of_primitiveRoots
    (F E : Type) [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) F).Nonempty)
    (a : F) (alpha : E)
    (halpha : alpha ^ (n : ℕ) = algebraMap F E a)
    (hgenerate : IntermediateField.adjoin F {alpha} = ⊤) :
    Polynomial.IsSplittingField F E
      (Polynomial.X ^ (n : ℕ) - Polynomial.C a)
theorem

finitePlaceHilbert_natCast_ne_zero

L110 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_natCast_ne_zero
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbert_natCast_ne_zero
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (v : HeightOneSpectrum (𝓞 K)) :
    ((n : ℕ) :
        (NumberField.HeightOneSpectrum.adicAbv K v).Completion) ≠ 0
theorem

finitePlaceHilbert_primitiveRoots_nonempty

L122 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_primitiveRoots_nonempty
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbert_primitiveRoots_nonempty
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) :
    (primitiveRoots (n : ℕ)
      (NumberField.HeightOneSpectrum.adicAbv K v).Completion).Nonempty
def

finitePlaceHilbert_completionUnit

L137 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbert_completionUnit
Documentation

The image of a global unit in the canonical absolute-value completion at a finite place.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceHilbert_completionUnit
    (v : HeightOneSpectrum (𝓞 K)) (a : Kˣ) :
    (NumberField.HeightOneSpectrum.adicAbv K v).Completionˣ
def

finitePlaceLocalHilbertSymbol

L146 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceLocalHilbertSymbol
Documentation

The local Hilbert-symbol value in the canonical absolute-value completion at a finite place, before transport back to the number field.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceLocalHilbertSymbol
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ) :
    nthRootsSubgroup
      (NumberField.HeightOneSpectrum.adicAbv K v).Completion (n : ℕ)
def

finitePlaceHilbertSymbol

L166 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol
Documentation

The Hilbert symbol of two global units at a finite place, evaluated in the actual local completion and transported back to μₙ(K).

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceHilbertSymbol
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ) :
    nthRootsSubgroup K (n : ℕ)
theorem

finitePlaceHilbertSymbol_map_eq_localHilbertSymbol

L177 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceHilbertSymbol_map_eq_localHilbertSymbol
Documentation

Extending the finite-place symbol to the completion recovers the underlying local Hilbert symbol on the images of the two global units.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceHilbertSymbol_map_eq_localHilbertSymbol
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ) :
    nthRootsSubgroupMap K
        (NumberField.HeightOneSpectrum.adicAbv K v).Completion (n : ℕ)
        (finitePlaceHilbertSymbol K n hnK hmu v a b) =
      finitePlaceLocalHilbertSymbol K n hnK hmu v a b
def

finitePlaceKummerRootCharacterOfExtension

L200 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceKummerRootCharacterOfExtension
Documentation

The global Kummer root character evaluated at the finite-place Artin automorphism attached to a specified extension of the place. Its value is transported from the chosen global simple Kummer extension back to μₙ(K).

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceKummerRootCharacterOfExtension
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (chosenSimpleKummerExtension K n hnK b)) :
    nthRootsSubgroup K (n : ℕ)
theorem

finitePlaceKummerRootCharacterOfExtension_eq_of_extensions

L223 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceKummerRootCharacterOfExtension_eq_of_extensions
Documentation

Changing the extension of the base absolute value does not change the transported Kummer root-character value.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceKummerRootCharacterOfExtension_eq_of_extensions
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ)
    (w w' : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (chosenSimpleKummerExtension K n hnK b)) :
    finitePlaceKummerRootCharacterOfExtension
        K n hnK hmu v a b w =
      finitePlaceKummerRootCharacterOfExtension
        K n hnK hmu v a b w'
def

finitePlaceKummerRootCharacter

L252 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceKummerRootCharacter
Documentation

The finite-place Kummer root-character value obtained from the canonical chosen extension of the base place.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def finitePlaceKummerRootCharacter
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ) :
    nthRootsSubgroup K (n : ℕ)
theorem

finitePlaceKummerRootCharacterOfExtension_eq

L269 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceKummerRootCharacterOfExtension_eq
Documentation

The finite-place Kummer root-character value is independent of the extension of the base absolute value used to construct the local Artin map.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open KummerTheory
open AlgebraicNumberTheory.Valuations
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem finitePlaceKummerRootCharacterOfExtension_eq
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (a b : Kˣ)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (chosenSimpleKummerExtension K n hnK b)) :
    finitePlaceKummerRootCharacterOfExtension
        K n hnK hmu v a b w =
      finitePlaceKummerRootCharacter K n hnK hmu v a b

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