NYLL
Module

NegativeThreeLocalRadical.lean

Nyll.SawinTotallyRealTowers.NegativeThreeLocalRadical
2 declarations indexed from sourceView source ↗

Module documentation

The local value at three of the negative-three character

Global reciprocity applied to the principal idele of negative one identifies its local value at three with its nontrivial real sign. All other finite components disappear by the proved unramifiedness of the actual quadratic character. No Hilbert-symbol or norm-pairing comparison is assumed.

Imports20
Imported by2

Declarations

instance

negativeThreeLocalRadicalZModAddCommGroup

L45 ↗
ClassFieldTower.Sawin.negativeThreeLocalRadicalZModAddCommGroup
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
Lean source · statement
instance negativeThreeLocalRadicalZModAddCommGroup : AddCommGroup (ZMod 2)
theorem

negativeThreeCharacter_three_neg_one_ne_one

L50 ↗
ClassFieldTower.Sawin.negativeThreeCharacter_three_neg_one_ne_one
Documentation

The character of the actual field ℚ(√−3), evaluated through global reciprocity on the three-adic unit −1, is nontrivial.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
local instance negativeThreeLocalRadicalZModAddCommGroup : AddCommGroup (ZMod 2) :=
  (ZMod.commRing 2).toAddCommGroup
Lean source · statement
theorem negativeThreeCharacter_three_neg_one_ne_one :
    globalReciprocityIdeleCharacter ℚ 2 negativeThreeCharacter
      (IdeleGroup.finitePlaceIdele
        ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
          (⟨3, Nat.prime_three⟩ : Nat.Primes)) (-1)) ≠ 1

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