Module

QuadraticClosureClassification.lean

Nyll.SawinTotallyRealTowers.QuadraticClosureClassification

3 declarations indexed from sourceView source ↗

Module documentation

Identifying quadratic subfields from their generators

A root of the same quadratic equation generates the same subfield of the fixed algebraic closure. This identifies arbitrary quadratic layers with the concrete constructors and makes squarefree radicands unique.

Imports5

Nyll.SawinTotallyRealTowers.QuadraticClosure
Nyll.SawinTotallyRealTowers.QuadraticSupportedGenerator
Nyll.SawinTotallyRealTowers.FiniteRealPExtension
Mathlib.Algebra.Ring.Commute
Mathlib.Algebra.Algebra.Rat

Imported by2

theorem

quadraticClosure_eq_adjoin_of_sq

L27 ↗

ClassFieldTower.Sawin.quadraticClosure_eq_adjoin_of_sq

Documentation

The quadratic subfield is independent of the choice of square root.

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 quadraticClosure_eq_adjoin_of_sq
    (d : ℚ) (hd : ¬ IsSquare d) (β : AlgebraicClosure ℚ)
    (hβ : β ^ 2 = algebraMap ℚ (AlgebraicClosure ℚ) d) :
    (quadraticClosure d hd).toIntermediateField =
      IntermediateField.adjoin ℚ ({β} : Set (AlgebraicClosure ℚ))

theorem

eq_quadraticClosure_of_generator

L49 ↗

ClassFieldTower.Sawin.eq_quadraticClosure_of_generator

Documentation

An internal square-root generator identifies an arbitrary finite Galois intermediate field with the concrete quadratic subfield.

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 eq_quadraticClosure_of_generator
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ))
    (d : ℚ) (hd : ¬ IsSquare d) (β : E)
    (hβ : β ^ 2 = algebraMap ℚ E d)
    (hGenerate : IntermediateField.adjoin ℚ ({β} : Set E) = ⊤) :
    E = quadraticClosure d hd

theorem

exists_supported_radicand_of_admissible_quadratic

L75 ↗

ClassFieldTower.Sawin.exists_supported_radicand_of_admissible_quadratic

Documentation

Every admissible quadratic layer has a positive squarefree supported radicand and equals the actual quadratic subfield constructed from it.

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 exists_supported_radicand_of_admissible_quadratic
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ))
    (hDegree : Module.finrank ℚ E = 2)
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (hE : IsAdmissibleFiniteLayer 2 T E)
    (hTwo : (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨2, Nat.prime_two⟩ : Nat.Primes) ∉ T) :
    ∃ d : ℤ, ∃ hd : ¬ IsSquare (d : ℚ),
      0 < d ∧ Squarefree d.natAbs ∧ d % 4 = 1 ∧
        (∀ q : Nat.Primes, (q : ℤ) ∣ d →
          (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q ∈ T) ∧
        E = quadraticClosure (d : ℚ) hd

Module documentation

Identifying quadratic subfields from their generators

Declarations

quadraticClosure_eq_adjoin_of_sq

eq_quadraticClosure_of_generator

exists_supported_radicand_of_admissible_quadratic