Module

QuadraticIntegerBasis.lean

Nyll.SawinTotallyRealTowers.QuadraticIntegerBasis

12 declarations indexed from sourceView source ↗

Module documentation

Integral bases of squarefree quadratic number fields

The square-root generator is integral. When its square is one modulo four, its half-integer translate is integral as well. Integer-coordinate classification gives spanning, and the concrete rational quadratic basis gives linear independence. These produce actual bases of the full ring of integers, with the two expected basis vectors.

Imports14

Nyll.SawinTotallyRealTowers.QuadraticBasis
Nyll.SawinTotallyRealTowers.QuadraticIntegerRepresentation
Nyll.SawinTotallyRealTowers.QuadraticIntegralGenerator
Mathlib.Algebra.Algebra.Basic
Mathlib.Algebra.Module.LinearMap.Defs
Mathlib.Data.Fin.VecNotation
Mathlib.LinearAlgebra.Basis.Basic
Mathlib.LinearAlgebra.LinearIndependent.Basic
Mathlib.LinearAlgebra.Span.Defs
Mathlib.NumberTheory.NumberField.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.Tactic.FinCases
Mathlib.Tactic.Ring
Lean.Elab.Tactic.Omega

Imported by2

def

quadraticIntegerGenerator

L40 ↗

ClassFieldTower.Sawin.quadraticIntegerGenerator

Documentation

The integral square-root generator as an element of the ring of integers.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

def quadraticIntegerGenerator
    (L : Type u) [Field L] [NumberField L] (d : ℤ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ)) : 𝓞 L

theorem

coe_quadraticIntegerGenerator

L46 ↗

ClassFieldTower.Sawin.coe_quadraticIntegerGenerator

Documentation

Coercing the integral square-root generator recovers the original element.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem coe_quadraticIntegerGenerator
    (L : Type u) [Field L] [NumberField L] (d : ℤ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ)) :
    (quadraticIntegerGenerator L d α hSquare : L) = α

def

quadraticHalfIntegerGenerator

L54 ↗

ClassFieldTower.Sawin.quadraticHalfIntegerGenerator

Documentation

The half-integer generator is integral when its square parameter is one modulo four.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

def quadraticHalfIntegerGenerator
    (L : Type u) [Field L] [NumberField L] (d : ℤ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ)) (hMod : d % 4 = 1) : 𝓞 L

theorem

coe_quadraticHalfIntegerGenerator

L66 ↗

ClassFieldTower.Sawin.coe_quadraticHalfIntegerGenerator

Documentation

Coercing the half-integer generator recovers its field expression.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem coe_quadraticHalfIntegerGenerator
    (L : Type u) [Field L] [NumberField L] (d : ℤ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ)) (hMod : d % 4 = 1) :
    (quadraticHalfIntegerGenerator L d α hSquare hMod : L) = (1 + α) / 2

theorem

adjoin_half_quadraticGenerator_eq_top

L75 ↗

ClassFieldTower.Sawin.adjoin_half_quadraticGenerator_eq_top

Documentation

Replacing a primitive element by its half-integer translate preserves its generated field over ℚ.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem adjoin_half_quadraticGenerator_eq_top
    (L : Type u) [Field L] [Algebra ℚ L] (α : L)
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    IntermediateField.adjoin ℚ ({(1 + α) / 2} : Set L) = ⊤

theorem

linearIndependent_one_integer_generator

L94 ↗

ClassFieldTower.Sawin.linearIndependent_one_integer_generator

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem linearIndependent_one_integer_generator
    (L : Type u) [Field L] [NumberField L] [Algebra.IsQuadraticExtension ℚ L]
    (β : 𝓞 L)
    (hGenerate : IntermediateField.adjoin ℚ ({(β : L)} : Set L) = ⊤) :
    LinearIndependent ℤ ![(1 : 𝓞 L), β]

def

quadraticIntegerBasisOfModFourNeOne

L117 ↗

ClassFieldTower.Sawin.quadraticIntegerBasisOfModFourNeOne

Documentation

The integral basis 1, α when the signed squarefree radicand is not one modulo four.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

def quadraticIntegerBasisOfModFourNeOne
    (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) : Module.Basis (Fin 2) ℤ (𝓞 L)

theorem

quadraticIntegerBasisOfModFourNeOne_apply_zero

L141 ↗

ClassFieldTower.Sawin.quadraticIntegerBasisOfModFourNeOne_apply_zero

Documentation

The first basis vector is one in the non-one-modulo-four case.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem quadraticIntegerBasisOfModFourNeOne_apply_zero
    (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) :
    quadraticIntegerBasisOfModFourNeOne L d hd α hSquare hGenerate hMod 0 = 1

theorem

quadraticIntegerBasisOfModFourNeOne_apply_one

L150 ↗

ClassFieldTower.Sawin.quadraticIntegerBasisOfModFourNeOne_apply_one

Documentation

The second basis vector is the integral square-root generator.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem quadraticIntegerBasisOfModFourNeOne_apply_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) :
    quadraticIntegerBasisOfModFourNeOne L d hd α hSquare hGenerate hMod 1 =
      quadraticIntegerGenerator L d α hSquare

def

quadraticIntegerBasisOfModFourEqOne

L162 ↗

ClassFieldTower.Sawin.quadraticIntegerBasisOfModFourEqOne

Documentation

The integral basis 1, (1 + α) / 2 when the signed squarefree radicand is one modulo four.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

def quadraticIntegerBasisOfModFourEqOne
    (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) : Module.Basis (Fin 2) ℤ (𝓞 L)

theorem

quadraticIntegerBasisOfModFourEqOne_apply_zero

L187 ↗

ClassFieldTower.Sawin.quadraticIntegerBasisOfModFourEqOne_apply_zero

Documentation

The first basis vector is one in the one-modulo-four case.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem quadraticIntegerBasisOfModFourEqOne_apply_zero
    (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) :
    quadraticIntegerBasisOfModFourEqOne L d hd α hSquare hGenerate hMod 0 = 1

theorem

quadraticIntegerBasisOfModFourEqOne_apply_one

L196 ↗

ClassFieldTower.Sawin.quadraticIntegerBasisOfModFourEqOne_apply_one

Documentation

The second basis vector is the integral half-integer generator.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem quadraticIntegerBasisOfModFourEqOne_apply_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) :
    quadraticIntegerBasisOfModFourEqOne L d hd α hSquare hGenerate hMod 1 =
      quadraticHalfIntegerGenerator L d α hSquare hMod

Module documentation

Integral bases of squarefree quadratic number fields

Declarations