Module

SixPrimeQuadraticCompositum.lean

Nyll.SawinTotallyRealTowers.SixPrimeQuadraticCompositum

6 declarations indexed from sourceView source ↗

Module documentation

The five quadratic layers over the six-prime support

The radicands 5, 13, 17, 21, 33 give actual finite Galois fields inside the chosen algebraic closure of ℚ. Each satisfies the prescribed finite ramification and real-place conditions. Their finite supremum is therefore an admissible compositum of these five quadratic fields.

Imports7

Nyll.SawinTotallyRealTowers.FiveQuadraticSquareClasses
Nyll.SawinTotallyRealTowers.QuadraticAdmissibleLayer
Nyll.SawinTotallyRealTowers.SixPrimeSupport
Mathlib.Data.Finset.Lattice.Fold
Mathlib.Data.Nat.PrimeFin
Mathlib.Data.Nat.Squarefree
Mathlib.Tactic.FinCases

Imported by5

theorem

sawinQuadraticRadicand_arithmetic

L31 ↗

ClassFieldTower.Sawin.sawinQuadraticRadicand_arithmetic

Source context 4 commands

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

open scoped NumberField
open IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem sawinQuadraticRadicand_arithmetic (i : Fin 5) :
    0 < (sawinQuadraticRadicand i : ℤ) ∧
      Squarefree (sawinQuadraticRadicand i : ℤ).natAbs ∧
      (sawinQuadraticRadicand i : ℤ) % 4 = 1 ∧
      (sawinQuadraticRadicand i).primeFactors ⊆ sawinRationalPrimes

def

sawinQuadraticLayer

L39 ↗

ClassFieldTower.Sawin.sawinQuadraticLayer

Documentation

The quadratic field associated to the indexed radicand.

Source context 4 commands

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

open scoped NumberField
open IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

def sawinQuadraticLayer (i : Fin 5) :
    FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)

theorem

isAdmissibleFiniteLayer_sawinQuadraticLayer

L45 ↗

ClassFieldTower.Sawin.isAdmissibleFiniteLayer_sawinQuadraticLayer

Documentation

Each of the five constructed quadratic fields is an admissible real two-extension with ramification restricted to the six allowed primes.

Source context 4 commands

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

open scoped NumberField
open IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isAdmissibleFiniteLayer_sawinQuadraticLayer (i : Fin 5) :
    IsAdmissibleFiniteLayer 2 sawinRationalPrimeSupport (sawinQuadraticLayer i)

def

sawinQuadraticCompositum

L68 ↗

ClassFieldTower.Sawin.sawinQuadraticCompositum

Documentation

The actual finite compositum of the five quadratic layers.

Source context 4 commands

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

open scoped NumberField
open IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

def sawinQuadraticCompositum : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)

theorem

sawinQuadraticLayer_le_compositum

L72 ↗

ClassFieldTower.Sawin.sawinQuadraticLayer_le_compositum

Documentation

Each chosen quadratic field is contained in their finite compositum.

Source context 4 commands

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

open scoped NumberField
open IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem sawinQuadraticLayer_le_compositum (i : Fin 5) :
    sawinQuadraticLayer i ≤ sawinQuadraticCompositum

theorem

isAdmissibleFiniteLayer_sawinQuadraticCompositum

L78 ↗

ClassFieldTower.Sawin.isAdmissibleFiniteLayer_sawinQuadraticCompositum

Documentation

The compositum remains an admissible finite layer by the proved compositum closure of the arithmetic conditions.

Source context 4 commands

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

open scoped NumberField
open IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isAdmissibleFiniteLayer_sawinQuadraticCompositum :
    IsAdmissibleFiniteLayer 2 sawinRationalPrimeSupport sawinQuadraticCompositum

Module documentation

The five quadratic layers over the six-prime support

Declarations

sawinQuadraticRadicand_arithmetic

sawinQuadraticLayer

isAdmissibleFiniteLayer_sawinQuadraticLayer

sawinQuadraticCompositum

sawinQuadraticLayer_le_compositum

isAdmissibleFiniteLayer_sawinQuadraticCompositum