Module

InfinitePlaceRealComparison.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlaceRealComparison

4 declarations indexed from sourceView source ↗

Module documentation

Complete infinite-place Kummer root-character comparison

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlaceNegative

Imported by2

theorem

infinitePlaceKummerRootCharacter_eq_one_of_real_of_left_pos

L30 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_eq_one_of_real_of_left_pos

Documentation

A global unit positive at a real place has trivial infinite-place Kummer root character.

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 infinitePlaceKummerRootCharacter_eq_one_of_real_of_left_pos
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : InfinitePlace K) (a b : Kˣ) (hv : v.IsReal)
    (ha : 0 < InfinitePlace.embedding_of_isReal hv (a : K)) :
    infinitePlaceKummerRootCharacter K n hnK hmu v a b = 1

theorem

infinitePlaceKummerRootCharacter_localGlobal_of_real_of_left_pos

L63 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_localGlobal_of_real_of_left_pos

Documentation

In the quadratic real case, positivity of the first argument gives the explicit local--global comparison.

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 infinitePlaceKummerRootCharacter_localGlobal_of_real_of_left_pos
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : InfinitePlace K) (a b : Kˣ)
    (hn : (n : ℕ) = 2) (hv : v.IsReal)
    (ha : 0 < InfinitePlace.embedding_of_isReal hv (a : K)) :
    infinitePlaceKummerRootCharacter K n hnK hmu v a b =
      infinitePlaceHilbertSymbol K n v a b

theorem

infinitePlaceKummerRootCharacter_localGlobal_of_real_of_two

L81 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_localGlobal_of_real_of_two

Documentation

Complete quadratic comparison at a real 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_real_of_two
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : InfinitePlace K) (a b : Kˣ)
    (hn : (n : ℕ) = 2) (hv : v.IsReal) :
    infinitePlaceKummerRootCharacter K n hnK hmu v a b =
      infinitePlaceHilbertSymbol K n v a b

theorem

infinitePlaceKummerRootCharacter_localGlobal

L118 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_localGlobal

Documentation

At every infinite place, the actual infinite-place Artin root character equals the explicit Hilbert factor.

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
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : InfinitePlace K) (a b : Kˣ) :
    infinitePlaceKummerRootCharacter K n hnK hmu v a b =
      infinitePlaceHilbertSymbol K n v a b

Module documentation

Complete infinite-place Kummer root-character comparison

Declarations

infinitePlaceKummerRootCharacter_eq_one_of_real_of_left_pos

infinitePlaceKummerRootCharacter_localGlobal_of_real_of_left_pos

infinitePlaceKummerRootCharacter_localGlobal_of_real_of_two

infinitePlaceKummerRootCharacter_localGlobal