Module

QuadraticAdmissibleLayer.lean

Nyll.SawinTotallyRealTowers.QuadraticAdmissibleLayer

1 declaration indexed from sourceView source ↗

Module documentation

Admissible quadratic layers from supported radicands

A positive squarefree integer congruent to one modulo four determines an actual quadratic field in the fixed algebraic closure. Its Galois group has order two, its embeddings are real, and its discriminant is the given integer. Restricting its prime divisors therefore makes this constructed field an admissible finite layer of the real pro-two tower.

Imports8

Nyll.SawinTotallyRealTowers.FiniteRealPExtension
Nyll.SawinTotallyRealTowers.QuadraticClosure
Nyll.SawinTotallyRealTowers.QuadraticFieldDiscriminant
Nyll.SawinTotallyRealTowers.QuadraticReality
Nyll.SawinTotallyRealTowers.RationalRamificationSupport
Mathlib.Algebra.Order.Ring.Cast
Mathlib.FieldTheory.Galois.Basic
Mathlib.GroupTheory.PGroup

Imported by2

theorem

isAdmissibleFiniteLayer_quadraticClosure

L33 ↗

ClassFieldTower.Sawin.isAdmissibleFiniteLayer_quadraticClosure

Documentation

A positive squarefree nonsquare radicand congruent to one modulo four and supported on T produces an actual admissible quadratic layer.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isAdmissibleFiniteLayer_quadraticClosure
    (d : ℤ) (hdPos : 0 < d) (hdSquarefree : Squarefree d.natAbs)
    (hMod : d % 4 = 1) (hdNonsquare : ¬ IsSquare (d : ℚ))
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (hSupport : ∀ q : Nat.Primes, (q : ℤ) ∣ d →
      (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q ∈ T) :
    IsAdmissibleFiniteLayer 2 T (quadraticClosure (d : ℚ) hdNonsquare)

Module documentation

Admissible quadratic layers from supported radicands

Declarations

isAdmissibleFiniteLayer_quadraticClosure