Module

QuadraticBasis.lean

Nyll.SawinTotallyRealTowers.QuadraticBasis

5 declarations indexed from sourceView source ↗

Module documentation

The basis associated to a quadratic generator

A generator of a quadratic extension of ℚ supplies the actual basis 1, α. Reindexing its power basis by Fin 2 gives named basis vectors and the rational coordinates of every element. No square relation is needed for this linear-algebra construction.

Imports7

Mathlib.Algebra.BigOperators.Fin
Mathlib.Data.Fin.SuccPred
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.LinearAlgebra.Basis.Defs
Mathlib.LinearAlgebra.Dimension.Free
Mathlib.RingTheory.Adjoin.PowerBasis
Mathlib.RingTheory.PowerBasis

Imported by5

def

quadraticBasis

L29 ↗

ClassFieldTower.Sawin.quadraticBasis

Documentation

The basis 1, α associated to a generator of a quadratic extension.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

def quadraticBasis
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (α : L) (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    Module.Basis (Fin 2) ℚ L

theorem

quadraticBasis_apply

L42 ↗

ClassFieldTower.Sawin.quadraticBasis_apply

Documentation

Reindexing the quadratic power basis preserves its powers.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem quadraticBasis_apply
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (α : L) (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (i : Fin 2) : quadraticBasis L α hGenerate i = α ^ (i : ℕ)

theorem

quadraticBasis_apply_zero

L51 ↗

ClassFieldTower.Sawin.quadraticBasis_apply_zero

Documentation

The first basis vector is one.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem quadraticBasis_apply_zero
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (α : L) (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    quadraticBasis L α hGenerate 0 = 1

theorem

quadraticBasis_apply_one

L58 ↗

ClassFieldTower.Sawin.quadraticBasis_apply_one

Documentation

The second basis vector is the chosen generator.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem quadraticBasis_apply_one
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (α : L) (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    quadraticBasis L α hGenerate 1 = α

theorem

exists_rat_linear_combination_of_quadraticGenerator

L65 ↗

ClassFieldTower.Sawin.exists_rat_linear_combination_of_quadraticGenerator

Documentation

Every element has rational coordinates in the basis 1, α.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_rat_linear_combination_of_quadraticGenerator
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (α : L) (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (x : L) : ∃ a b : ℚ, x = algebraMap ℚ L a + algebraMap ℚ L b * α

Module documentation

The basis associated to a quadratic generator

Declarations

quadraticBasis

quadraticBasis_apply

quadraticBasis_apply_zero

quadraticBasis_apply_one

exists_rat_linear_combination_of_quadraticGenerator