Module

InfinitePlacePositive.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlacePositive

2 declarations indexed from sourceView source ↗

Module documentation

The positive-radicand real infinite-place branch

When the radicand is positive at a real place, it is a square in the local completion. The existing Kummer tensor-norm theorem then makes the local norm subgroup all of the completion units, so the actual infinite-place Artin automorphism and its Kummer root character are trivial.

Imports3

Imported by2

theorem

infinitePlaceKummerRootCharacter_eq_one_of_real_of_radical_pos

L36 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_eq_one_of_real_of_radical_pos

Documentation

In the quadratic real case, a positive radicand makes the infinite-place Kummer root character 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_real_of_radical_pos
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (v : InfinitePlace K) (a b : Kˣ)
    (hn : (n : ℕ) = 2) (hv : v.IsReal)
    (hb : 0 < InfinitePlace.embedding_of_isReal hv (b : K)) :
    infinitePlaceKummerRootCharacter K n hnK hmu v a b = 1

theorem

infinitePlaceKummerRootCharacter_localGlobal_of_real_of_radical_pos

L83 ↗

GlobalClassFieldTheory.Reciprocity.infinitePlaceKummerRootCharacter_localGlobal_of_real_of_radical_pos