Module

InfinitePlaceNegativeUnit.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlaceNegativeUnit

3 declarations indexed from sourceView source ↗

Module documentation

Negative units and the real infinite-place Artin map

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.GlobalHilbertSymbol.InfinitePlaceNegativeRoot

Imported by2

theorem

ringEquiv_unit_div_neg_one

L25 ↗

GlobalClassFieldTheory.Reciprocity.ringEquiv_unit_div_neg_one

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

Lean source · statement

theorem ringEquiv_unit_div_neg_one
    {F : Type*} [Field F] (e : F ≃+* ℝ) (x : Fˣ) :
    e ((x / (-1 : Fˣ) : Fˣ) : F) = -e (x : F)

theorem

monoidHom_eq_of_div_apply_eq_one

L37 ↗

GlobalClassFieldTheory.Reciprocity.monoidHom_eq_of_div_apply_eq_one

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

Lean source · statement

theorem monoidHom_eq_of_div_apply_eq_one
    {G H : Type*} [Group G] [Monoid H]
    (f : G →* H) (x y : G) (h : f (x / y) = 1) :
    f x = f y

theorem

chosenInfinitePlaceArtin_globalUnit_eq_neg_one_of_real_of_neg

L49 ↗

GlobalClassFieldTheory.Reciprocity.chosenInfinitePlaceArtin_globalUnit_eq_neg_one_of_real_of_neg

Documentation

At a real infinite place, the Artin value of a negative global unit is the Artin value of -1.

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 chosenInfinitePlaceArtin_globalUnit_eq_neg_one_of_real_of_neg
    {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L]
    (v : InfinitePlace K) (hv : v.IsReal) (a : Kˣ)
    (ha : InfinitePlace.embedding_of_isReal hv (a : K) < 0) :
    chosenInfinitePlaceArtinMonoidHom (K := K) (L := L) v
        (Units.map (algebraMap K v.Completion).toMonoidHom a) =
      chosenInfinitePlaceArtinMonoidHom (K := K) (L := L) v
        (-1 : v.Completionˣ)

Module documentation

Negative units and the real infinite-place Artin map

Declarations

ringEquiv_unit_div_neg_one

monoidHom_eq_of_div_apply_eq_one

chosenInfinitePlaceArtin_globalUnit_eq_neg_one_of_real_of_neg