Nyll.SawinTotallyRealTowers.QuadraticSupportedGenerator

Module documentation

Positive squarefree generators with prescribed ramification support

A totally real quadratic number field has a positive squarefree integer radicand. If its allowed finite ramification support excludes two, the discriminant formula forces the radicand to be one modulo four. The discriminant is then the radicand itself, so every prime divisor belongs to the prescribed support.

theorem

exists_positive_squarefree_supported_generator

L33 ↗

ClassFieldTower.Sawin.exists_positive_squarefree_supported_generator

Documentation

A totally real quadratic number field unramified outside a support excluding two has a positive squarefree radicand congruent to one modulo four, all of whose prime divisors lie in that support.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_positive_squarefree_supported_generator
    (L : Type u) [Field L] [NumberField L]
    [Algebra.IsQuadraticExtension ℚ L] [IsTotallyReal L]
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (hOutside : IsUnramifiedAtFinitePlacesOutside ℚ L T)
    (hTwo : (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨2, Nat.prime_two⟩ : Nat.Primes) ∉ T) :
    ∃ d : ℤ, ∃ β : L,
      0 < d ∧ Squarefree d.natAbs ∧ d % 4 = 1 ∧
        β ^ 2 = algebraMap ℚ L (d : ℚ) ∧
        IntermediateField.adjoin ℚ ({β} : Set L) = ⊤ ∧
        ¬ IsSquare (d : ℚ) ∧
        ∀ q : Nat.Primes, (q : ℤ) ∣ d →
          (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q ∈ T

Module documentation

Positive squarefree generators with prescribed ramification support

Declarations

exists_positive_squarefree_supported_generator