Module

QuadraticIntegerRepresentation.lean

Nyll.SawinTotallyRealTowers.QuadraticIntegerRepresentation

3 declarations indexed from sourceView source ↗

Module documentation

Integer coordinates in a quadratic number field

The trace and norm conditions and their parity criterion give integer coordinates for every algebraic integer. Away from d = 1 modulo four the generators are 1, α. Every algebraic integer also has integer coordinates in 1, (1 + α) / 2 for every squarefree d. When d is one modulo four, the second generator is itself integral.

Imports5

Nyll.SawinTotallyRealTowers.QuadraticBasis
Nyll.SawinTotallyRealTowers.QuadraticIntegralCoordinates
Nyll.SawinTotallyRealTowers.QuadraticIntegralParity
Mathlib.Algebra.Ring.Parity
Mathlib.NumberTheory.NumberField.Basic

Imported by2

theorem

exists_int_twice_coordinates

L29 ↗

ClassFieldTower.Sawin.exists_int_twice_coordinates

Source context 3 commands

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

open scoped NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

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

theorem

exists_int_linear_combination_of_mod_four_ne_one

L53 ↗

ClassFieldTower.Sawin.exists_int_linear_combination_of_mod_four_ne_one

Documentation

When the squarefree radicand is not one modulo four, every algebraic integer has integer coordinates in 1, α.

Source context 3 commands

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

open scoped NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_int_linear_combination_of_mod_four_ne_one
    (L : Type u) [Field L] [NumberField L] [Algebra.IsQuadraticExtension ℚ L]
    (d : ℤ) (hd : Squarefree d.natAbs) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ))
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (hMod : d % 4 ≠ 1) (x : 𝓞 L) :
    ∃ m n : ℤ, (x : L) = (m : L) + (n : L) * α

theorem

exists_int_linear_combination_of_half_quadraticGenerator

L78 ↗

ClassFieldTower.Sawin.exists_int_linear_combination_of_half_quadraticGenerator

Documentation

Every algebraic integer has integer coordinates in 1, (1 + α) / 2. The parity of the two half-integer coordinates is the same, so this representation does not require a congruence assumption on d.

Source context 3 commands

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

open scoped NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_int_linear_combination_of_half_quadraticGenerator
    (L : Type u) [Field L] [NumberField L] [Algebra.IsQuadraticExtension ℚ L]
    (d : ℤ) (hd : Squarefree d.natAbs) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ))
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (x : 𝓞 L) :
    ∃ m n : ℤ, (x : L) = (m : L) + (n : L) * ((1 + α) / 2)

Module documentation

Integer coordinates in a quadratic number field

Declarations

exists_int_twice_coordinates

exists_int_linear_combination_of_mod_four_ne_one

exists_int_linear_combination_of_half_quadraticGenerator