Module

SixPrimeQuadraticClassification.lean

Nyll.SawinTotallyRealTowers.SixPrimeQuadraticClassification

3 declarations indexed from sourceView source ↗

Module documentation

Exhausting the quadratic layers of the six-prime real tower

The ramification and discriminant classification supplies a positive squarefree radicand for every quadratic layer. Its explicit square-class factorization then places that layer inside the compositum of the five chosen quadratic fields.

Imports4

Imported by2

theorem

sawinQuadraticRoot_mem_compositum

L26 ↗

ClassFieldTower.Sawin.sawinQuadraticRoot_mem_compositum

Source context 3 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin

Lean source · statement

theorem sawinQuadraticRoot_mem_compositum (i : Fin 5) :
    quadraticClosureRoot (sawinQuadraticRadicand i : ℚ) ∈
      sawinQuadraticCompositum.toIntermediateField

theorem

admissible_quadratic_le_sawinQuadraticCompositum

L35 ↗

ClassFieldTower.Sawin.admissible_quadratic_le_sawinQuadraticCompositum

Documentation

Every quadratic layer of the real tower unramified outside the six specified primes lies in the concrete five-generator compositum.

Source context 3 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin

Lean source · statement

theorem admissible_quadratic_le_sawinQuadraticCompositum
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ))
    (hDegree : Module.finrank ℚ E = 2)
    (hE : IsAdmissibleFiniteLayer 2 sawinRationalPrimeSupport E) :
    E ≤ sawinQuadraticCompositum

theorem

sawinQuadraticCompositum_eq_iSup_quadratic_layers

L71 ↗

ClassFieldTower.Sawin.sawinQuadraticCompositum_eq_iSup_quadratic_layers

Documentation

The five-generator compositum is exactly the compositum of all admissible quadratic subfields, rather than only a subfield of that tower.

Source context 3 commands

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

open scoped NumberField BigOperators
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin

Lean source · statement

theorem sawinQuadraticCompositum_eq_iSup_quadratic_layers :
    sawinQuadraticCompositum.toIntermediateField =
      ⨆ (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ))
        (_ : IsAdmissibleFiniteLayer 2 sawinRationalPrimeSupport E)
        (_ : Module.finrank ℚ E = 2), E.toIntermediateField

Module documentation

Exhausting the quadratic layers of the six-prime real tower

Declarations

sawinQuadraticRoot_mem_compositum

admissible_quadratic_le_sawinQuadraticCompositum

sawinQuadraticCompositum_eq_iSup_quadratic_layers