Module

InfinitePlaceCharacter.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlaceCharacter

4 declarations indexed from sourceView source ↗

Module documentation

Infinite-place Kummer root characters

This file connects the infinite-place Hilbert factor to the Kummer root character of the actual infinite-place Artin map. The complex-place branch is completed here. The real quadratic action is kept as the next arithmetic leaf rather than being introduced as an assumption.

Imports3

Imported by2

def

infinitePlaceKummerRootCharacter

L36 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter

Documentation

The Kummer root character of the actual Artin automorphism at an infinite place.

Source context 7 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]

Lean source · statement

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

theorem

chosenInfinitePlaceArtinMonoidHom_eq_one_of_isComplex

L55 ↗

GlobalClassFieldTheory.Reciprocity.chosenInfinitePlaceArtinMonoidHom_eq_one_of_isComplex

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 chosenInfinitePlaceArtinMonoidHom_eq_one_of_isComplex
    {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L]
    (v : InfinitePlace K) (hv : v.IsComplex) (x : v.Completionˣ) :
    chosenInfinitePlaceArtinMonoidHom (K := K) (L := L) v x = 1

theorem

infinitePlaceKummerRootCharacter_eq_one_of_isComplex

L78 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_eq_one_of_isComplex

Documentation

At a complex place the infinite-place Kummer root character is trivial.

Source context 7 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]

Lean source · statement

theorem infinitePlaceKummerRootCharacter_eq_one_of_isComplex
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : InfinitePlace K) (a b : Kˣ) (hv : v.IsComplex) :
    infinitePlaceKummerRootCharacter K n hnK hmu v a b = 1

theorem

infinitePlaceKummerRootCharacter_localGlobal_of_isComplex

L104 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_localGlobal_of_isComplex

Documentation

The Kummer root character and the explicit Hilbert factor agree at every complex infinite place.

Source context 7 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]

Lean source · statement

theorem infinitePlaceKummerRootCharacter_localGlobal_of_isComplex
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : InfinitePlace K) (a b : Kˣ) (hv : v.IsComplex) :
    infinitePlaceKummerRootCharacter K n hnK hmu v a b =
      infinitePlaceHilbertSymbol K n v a b

Module documentation

Infinite-place Kummer root characters

Declarations

infinitePlaceKummerRootCharacter

chosenInfinitePlaceArtinMonoidHom_eq_one_of_isComplex

infinitePlaceKummerRootCharacter_eq_one_of_isComplex

infinitePlaceKummerRootCharacter_localGlobal_of_isComplex