NYLL
Module

NegativeThreeCharacter.lean

Nyll.SawinTotallyRealTowers.NegativeThreeCharacter
10 declarations indexed from sourceView source ↗

Module documentation

The quadratic character of negative three

Restriction to the actual field generated by a square root of negative three gives a continuous character of the absolute Galois group of the rationals. Its discriminant proves that it kills finite inertia away from three. Its imaginary generator proves that its real Artin value is nontrivial. These properties provide a sign correction without changing inertia away from three.

Imports34
Imported by4

Declarations

def

quadraticCharacterCoordinate

L64 ↗
ClassFieldTower.Sawin.quadraticCharacterCoordinate
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
def quadraticCharacterCoordinate (F : Type) [Field F]
    (E : FiniteGaloisIntermediateField F (AlgebraicClosure F))
    (hd : Module.finrank F E = 2) :
    Gal(E/F) ≃* Multiplicative (ZMod 2)
def

quadraticAbsoluteCharacter

L73 ↗
ClassFieldTower.Sawin.quadraticAbsoluteCharacter
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
def quadraticAbsoluteCharacter (F : Type) [Field F]
    (E : FiniteGaloisIntermediateField F (AlgebraicClosure F))
    (hd : Module.finrank F E = 2) :
    Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod 2)
theorem

quadraticAbsoluteCharacter_eq_one_iff

L87 ↗
ClassFieldTower.Sawin.quadraticAbsoluteCharacter_eq_one_iff
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
theorem quadraticAbsoluteCharacter_eq_one_iff (F : Type) [Field F]
    (E : FiniteGaloisIntermediateField F (AlgebraicClosure F))
    (hd : Module.finrank F E = 2) (σ : Field.absoluteGaloisGroup F) :
    quadraticAbsoluteCharacter F E hd σ = 1 ↔
      AlgEquiv.restrictNormalHom
        (F := F) (K₁ := AlgebraicClosure F) E.toIntermediateField σ = 1
theorem

quadraticAbsoluteCharacter_inertia

L98 ↗
ClassFieldTower.Sawin.quadraticAbsoluteCharacter_inertia
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
theorem quadraticAbsoluteCharacter_inertia
    (F : Type) [Field F] [NumberField F]
    (E : FiniteGaloisIntermediateField F (AlgebraicClosure F)) [NumberField E]
    (hd : Module.finrank F E = 2) (T : Set (HeightOneSpectrum (𝓞 F)))
    (hUnramified : IsUnramifiedAtFinitePlacesOutside F E T)
    (v : HeightOneSpectrum (𝓞 F)) (hv : v ∉ T)
    (σ : finitePlaceAbsoluteInertiaSubgroup F v) :
    quadraticAbsoluteCharacter F E hd
      (finitePlaceAbsoluteDecompositionInclusion F v
        (finitePlaceAbsoluteInertiaInclusion F v σ)) = 1
theorem

quadraticAbsoluteCharacter_infinite

L128 ↗
ClassFieldTower.Sawin.quadraticAbsoluteCharacter_infinite
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
theorem quadraticAbsoluteCharacter_infinite
    (F : Type) [Field F] [CharZero F] [IsTotallyReal F]
    (E : FiniteGaloisIntermediateField F (AlgebraicClosure F))
    (hd : Module.finrank F E = 2)
    (hNoReal : ∀ φ : E →+* ℂ, ¬ ComplexEmbedding.IsReal φ)
    (v : InfinitePlace F) :
    quadraticAbsoluteCharacter F E hd (absoluteInfinitePlaceArtinNegOne F v) ≠ 1
theorem

negativeThree_nonsquare

L171 ↗
ClassFieldTower.Sawin.negativeThree_nonsquare
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
theorem negativeThree_nonsquare : ¬ IsSquare (-3 : ℚ)
abbrev

negativeThreeField

L176 ↗
ClassFieldTower.Sawin.negativeThreeField
Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
abbrev negativeThreeField : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)
def

negativeThreeCharacter

L180 ↗
ClassFieldTower.Sawin.negativeThreeCharacter
Documentation

The continuous quadratic character cut out by the actual field ℚ(√−3).

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
def negativeThreeCharacter : Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2)
theorem

negativeThreeCharacter_inertia

L186 ↗
ClassFieldTower.Sawin.negativeThreeCharacter_inertia
Documentation

The character of negative three kills absolute inertia at every finite place other than the rational prime three, including the prime two.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
theorem negativeThreeCharacter_inertia
    (v : HeightOneSpectrum (𝓞 ℚ))
    (hv : v ≠ (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes))
    (σ : finitePlaceAbsoluteInertiaSubgroup ℚ v) :
    negativeThreeCharacter
      (finitePlaceAbsoluteDecompositionInclusion ℚ v
        (finitePlaceAbsoluteInertiaInclusion ℚ v σ)) = 1
theorem

negativeThreeCharacter_infinite

L223 ↗
ClassFieldTower.Sawin.negativeThreeCharacter_infinite
Documentation

Its value on the actual real Artin element of negative one is nontrivial.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity AlgebraicNumberTheory.Valuations

-- Keep the canonical intermediate-field scalar structure generic until
-- restriction and its finite cyclic coordinate have both been constructed.
Lean source · statement
theorem negativeThreeCharacter_infinite (v : InfinitePlace ℚ) :
    negativeThreeCharacter (absoluteInfinitePlaceArtinNegOne ℚ v) ≠ 1

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