NYLL
Module

InfiniteArtinCompatibility.lean

Nyll.SawinTotallyRealTowers.InfiniteArtinCompatibility
4 declarations indexed from sourceView source ↗

Module documentation

Real Artin values and global reciprocity

Complex conjugation in the algebraic closure restricts to the chosen negative-one Artin value in every finite abelian subextension. These finite projections identify its maximal-abelian restriction with the actual idele Artin value. Consequently global reciprocity preserves the real value of an absolute character over a totally real number field.

Imports21
Imported by3

Declarations

theorem

conjugation_eq_chosenArtin

L45 ↗
ClassFieldTower.Sawin.conjugation_eq_chosenArtin
Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Sawin
open NumberField GlobalClassFieldTheory.Reciprocity
open ClassFieldTower.Martinet.Shafarevich
open scoped NumberField IsMulCommutative
Lean source · statement
theorem conjugation_eq_chosenArtin
    (F E : Type) [Field F] [Field E]
    [Algebra F E] [IsAbelianGalois F E]
    (v : InfinitePlace F) (phi : E →+* ℂ)
    (hw : (InfinitePlace.mk phi).comap (algebraMap F E) = v)
    (s : Gal(E/F)) (hs : ComplexEmbedding.IsConj phi s) :
    s = chosenInfinitePlaceArtinMonoidHom (K := F) (L := E)
      v (-1 : v.Completionˣ)
theorem

algebraicClosure_place_complex

L96 ↗
ClassFieldTower.Sawin.algebraicClosure_place_complex
Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Sawin
open NumberField GlobalClassFieldTheory.Reciprocity
open ClassFieldTower.Martinet.Shafarevich
open scoped NumberField IsMulCommutative
Lean source · statement
theorem algebraicClosure_place_complex
    (F : Type) [Field F] (w : InfinitePlace (AlgebraicClosure F)) : w.IsComplex
theorem

absoluteInfinitePlaceArtinNegOne_maximalAbelian

L109 ↗
ClassFieldTower.Sawin.absoluteInfinitePlaceArtinNegOne_maximalAbelian
Documentation

The actual real Artin generator restricts to the maximal-abelian idele Artin value of negative one.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Sawin
open NumberField GlobalClassFieldTheory.Reciprocity
open ClassFieldTower.Martinet.Shafarevich
open scoped NumberField IsMulCommutative
Lean source · statement
theorem absoluteInfinitePlaceArtinNegOne_maximalAbelian
    (F : Type) [Field F] [NumberField F] [IsTotallyReal F]
    (v : InfinitePlace F) :
    globalMaximalAbelianRestriction F (absoluteInfinitePlaceArtinNegOne F v) =
      maximalAbelianGlobalArtin F
        (IdeleGroup.infinitePlaceIdeleClass v (-1 : v.Completionˣ))
theorem

globalReciprocityIdeleCharacter_infinite_neg_one

L168 ↗
ClassFieldTower.Sawin.globalReciprocityIdeleCharacter_infinite_neg_one
Documentation

The global idele character has the same real sign as its given absolute character, through the actual Artin maps.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Sawin
open NumberField GlobalClassFieldTheory.Reciprocity
open ClassFieldTower.Martinet.Shafarevich
open scoped NumberField IsMulCommutative
Lean source · statement
theorem globalReciprocityIdeleCharacter_infinite_neg_one
    (F : Type) [Field F] [NumberField F] [IsTotallyReal F]
    (p : ℕ) [Fact p.Prime]
    (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
    (v : InfinitePlace F) :
    globalReciprocityIdeleCharacter F p chi
      (IdeleGroup.infinitePlaceIdele v (-1 : v.Completionˣ)) =
      chi (absoluteInfinitePlaceArtinNegOne F v)

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