Module

FinitePlaceLocalGlobal.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.FinitePlaceLocalGlobal

6 declarations indexed from sourceView source ↗

Module documentation

Finite-place local--global Kummer transport

This file compares the two splitting fields of the finite-place Kummer polynomial: the simple Kummer extension chosen directly over the completion and the localization of the chosen global simple Kummer extension. The completion input, finiteness, splitting-field, and equivalence data are kept as separate declarations so the eventual root-character comparison does not rebuild their instance towers.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.FinitePlaceComparison

Imported by2

abbrev

finitePlaceKummerPolynomial

L37 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceKummerPolynomial

Documentation

The Kummer polynomial obtained by mapping a global radicand into the finite-place completion.

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

abbrev finitePlaceKummerPolynomial
    (n : ℕ+) (v : HeightOneSpectrum (𝓞 K)) (b : Kˣ)

abbrev

finitePlaceKummerLocalExtension

L45 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceKummerLocalExtension

Documentation

The simple Kummer extension chosen intrinsically over the finite-place completion.

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

abbrev finitePlaceKummerLocalExtension
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (v : HeightOneSpectrum (𝓞 K)) (b : Kˣ)

theorem

finitePlaceLocalArtinInput_globalUnit

L56 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinInput_globalUnit

Documentation

Mapping a global unit through the concrete adic-completion model and then back through the canonical completion equivalence gives its ordinary image in the absolute-value completion.

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 finitePlaceLocalArtinInput_globalUnit
    (v : HeightOneSpectrum (𝓞 K)) (a : Kˣ) :
    finitePlaceLocalArtinInput v
        (Units.map
          (algebraMap K (v.adicCompletion K)).toMonoidHom a) =
      finitePlaceHilbert_completionUnit K v a

theorem

finitePlaceKummerLocalFiniteDimensional

L93 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceKummerLocalFiniteDimensional

Documentation

The named finite-dimensional certificate for the Kummer extension chosen directly over the completion.

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 finitePlaceKummerLocalFiniteDimensional
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (v : HeightOneSpectrum (𝓞 K)) (b : Kˣ) :
    FiniteDimensional (finitePlaceKummerBaseCompletion K v)
      (finitePlaceKummerLocalExtension K n hnK v b)

theorem

finitePlaceKummerLocal_isSplittingField

L105 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceKummerLocal_isSplittingField

Documentation

The simple Kummer extension chosen directly over the completion is a splitting field of the finite-place Kummer polynomial.

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 finitePlaceKummerLocal_isSplittingField
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (b : Kˣ) :
    Polynomial.IsSplittingField
      (finitePlaceKummerBaseCompletion K v)
      (finitePlaceKummerLocalExtension K n hnK v b)
      (finitePlaceKummerPolynomial K n v b)

def

finitePlaceKummerLocalGlobalAlgEquiv

L134 ↗

GlobalClassFieldTheory.Reciprocity.finitePlaceKummerLocalGlobalAlgEquiv

Documentation

A canonical algebra equivalence between the intrinsically local Kummer extension and the localization of the chosen global Kummer extension. It is constructed solely from the fact that both fields split the same polynomial; no compatibility between their chosen roots is assumed.

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 · full declaration

def finitePlaceKummerLocalGlobalAlgEquiv
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : HeightOneSpectrum (𝓞 K)) (b : Kˣ)
    (w : AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (chosenSimpleKummerExtension K n hnK b)) :
    let C := finitePlaceKummerBaseCompletion K v
    let S := finitePlaceKummerLocalExtension K n hnK v b
    let E := finitePlaceKummerLocalizedCompletion K n hnK v b w
    letI : Algebra C E :=
      finitePlaceKummerLocalizedAlgebra K n hnK v b w
    S ≃ₐ[C] E := by
  let C := finitePlaceKummerBaseCompletion K v
  let S := finitePlaceKummerLocalExtension K n hnK v b
  let E := finitePlaceKummerLocalizedCompletion K n hnK v b w
  let f := finitePlaceKummerPolynomial K n v b
  letI : Algebra C E :=
    finitePlaceKummerLocalizedAlgebra K n hnK v b w
  letI : FiniteDimensional C S :=
    finitePlaceKummerLocalFiniteDimensional K n hnK v b
  letI : FiniteDimensional C E :=
    finitePlaceKummerLocalizedFiniteDimensional K n hnK v b w
  letI : Polynomial.IsSplittingField C S f :=
    finitePlaceKummerLocal_isSplittingField K n hnK hmu v b
  letI : Polynomial.IsSplittingField C E f :=
    finitePlaceKummerLocalized_isSplittingField K n hnK hmu v b w
  exact
    (Polynomial.IsSplittingField.algEquiv S f).trans
      (Polynomial.IsSplittingField.algEquiv E f).symm

Module documentation

Finite-place local--global Kummer transport

Declarations

finitePlaceKummerPolynomial

finitePlaceKummerLocalExtension

finitePlaceLocalArtinInput_globalUnit

finitePlaceKummerLocalFiniteDimensional

finitePlaceKummerLocal_isSplittingField

finitePlaceKummerLocalGlobalAlgEquiv