NYLL
Module

InfinitePlaceRealSquare.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlaceRealSquare
2 declarations indexed from sourceView source ↗

Module documentation

Positive global units are local squares at real places

This is the arithmetic input for the positive-radicand branch of the real infinite-place Hilbert-symbol comparison.

Imports2
Imported by2

Declarations

theorem

realInfinitePlace_globalUnit_realCoordinate

L32 ↗
GlobalClassFieldTheory.Reciprocity.realInfinitePlace_globalUnit_realCoordinate
Documentation

The canonical real coordinate of a global unit in a real completion is its real infinite-place embedding.

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
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem realInfinitePlace_globalUnit_realCoordinate
    (v : InfinitePlace K) (hv : v.IsReal) (b : Kˣ) :
    InfinitePlace.Completion.ringEquivRealOfIsReal hv
        (Units.map (algebraMap K v.Completion).toMonoidHom b :
          v.Completionˣ) =
      InfinitePlace.embedding_of_isReal hv (b : K)
theorem

realInfinitePlace_globalUnit_mem_squareSubgroup_of_pos

L50 ↗
GlobalClassFieldTheory.Reciprocity.realInfinitePlace_globalUnit_mem_squareSubgroup_of_pos
Documentation

A global unit whose image at a real infinite place is positive becomes a square in the unit group of the completion.

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
variable (K : Type) [Field K] [NumberField K]
omit [NumberField K] in
Lean source · statement
theorem realInfinitePlace_globalUnit_mem_squareSubgroup_of_pos
    (v : InfinitePlace K) (hv : v.IsReal) (b : Kˣ)
    (hb : 0 < InfinitePlace.embedding_of_isReal hv (b : K)) :
    Units.map (algebraMap K v.Completion).toMonoidHom b ∈
      (powMonoidHom 2 : v.Completionˣ →* v.Completionˣ).range

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