Module

QuadraticIntegralCoordinates.lean

Nyll.SawinTotallyRealTowers.QuadraticIntegralCoordinates

2 declarations indexed from sourceView source ↗

Module documentation

Integral coordinates in a quadratic number field

The trace and norm of an algebraic integer are integral. For a square-root generator of signed squarefree square d, these identities force both coordinates to be half-integers and give the congruence modulo four. Conversely, the congruence supplies a monic integer polynomial.

Imports5

Nyll.SawinTotallyRealTowers.QuadraticTrace
Nyll.SawinTotallyRealTowers.SquarefreeIntegralCoordinates
Nyll.SawinTotallyRealTowers.QuadraticIntegralGenerator
Mathlib.Algebra.GCDMonoid.IntegrallyClosed
Mathlib.RingTheory.Norm.Transitivity

Imported by2

theorem

exists_int_quadratic_coordinates_of_isIntegral

L28 ↗

ClassFieldTower.Sawin.exists_int_quadratic_coordinates_of_isIntegral

Documentation

An integral element in squarefree quadratic coordinates has half-integer coordinates satisfying the norm congruence modulo four.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_int_quadratic_coordinates_of_isIntegral
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (d : ℤ) (hd : Squarefree d.natAbs) (a b : ℚ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ))
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (hx : IsIntegral ℤ (algebraMap ℚ L a + algebraMap ℚ L b * α)) :
    ∃ m n : ℤ, 2 * a = (m : ℚ) ∧ 2 * b = (n : ℚ) ∧ 4 ∣ m ^ 2 - d * n ^ 2

theorem

isIntegral_quadratic_coordinates_iff

L59 ↗

ClassFieldTower.Sawin.isIntegral_quadratic_coordinates_iff