NYLL
Module

AbsoluteRealKernelField.lean

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

Module documentation

Killing real conjugation makes the kernel field totally real

The real local Artin value of negative one is complex conjugation whenever an infinite place ramifies. If a discrete absolute representation kills these actual elements over a totally real base, its finite Galois kernel field has a real place above each base place. Galois conjugacy then gives total reality, independently of the order of the target group.

Imports11
Imported by11

Declarations

def

absoluteInfinitePlaceArtinNegOne

L36 ↗
ClassFieldTower.Sawin.absoluteInfinitePlaceArtinNegOne
Documentation

The negative-one local Artin element in the standard absolute Galois model. This fixes the algebraic-closure scalar structure before specialization.

Source context 3 commands

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

namespace ClassFieldTower.Sawin
open NumberField GlobalClassFieldTheory.Reciprocity
open ClassFieldTower.Martinet.Shafarevich
Lean source · statement
def absoluteInfinitePlaceArtinNegOne
    (F : Type) [Field F] [CharZero F] (v : InfinitePlace F) :
    Field.absoluteGaloisGroup F
theorem

absoluteDiscreteKernelField_isTotallyReal_of_infiniteArtin

L45 ↗
ClassFieldTower.Sawin.absoluteDiscreteKernelField_isTotallyReal_of_infiniteArtin
Documentation

Killing each actual real Artin generator makes the finite kernel field over a totally real base totally real. No p-group or odd-order input is used.

Source context 3 commands

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

namespace ClassFieldTower.Sawin
open NumberField GlobalClassFieldTheory.Reciprocity
open ClassFieldTower.Martinet.Shafarevich
Lean source · statement
theorem absoluteDiscreteKernelField_isTotallyReal_of_infiniteArtin
    (F : Type) [Field F] [NumberField F] [IsTotallyReal F]
    {Q : Type*} [Group Q] [TopologicalSpace Q] [DiscreteTopology Q]
    (s : Field.absoluteGaloisGroup F →ₜ* Q)
    (hs : ∀ v : InfinitePlace F, s (absoluteInfinitePlaceArtinNegOne F v) = 1) :
    IsTotallyReal (absoluteDiscreteKernelField F s)

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