30.1. Introduction🔗

HexNumberFieldTower builds number fields one generator at a time: ℚ, then ℚ(α₁), then ℚ(α₁, α₂), each step adjoining a root of a polynomial that is irreducible over the field so far. Elements are stored as rational coordinates in the product basis of the tower, and arithmetic is polynomial arithmetic modulo the defining polynomials. Every tower also comes with a fixed embedding into ℂ, so a tower is a particular subfield of ℂ rather than a field known up to isomorphism. The embedding is what lets the library answer questions an abstract presentation cannot: which root of X² − 2 the generator denotes, and therefore whether a given algebraic number already lies in the field.

Four operations do the work. Hex.NumberTower.factor? factors a polynomial over a tower by Trager's method, one level at a time. Hex.NumberTower.adjoin? adjoins a specified algebraic number and recognises when it is already present. Hex.NumberTower.split? alternates factoring and adjoining until a polynomial splits into linear factors, and returns the splitting field together with all of the roots. Hex.NumberTower.flatten? replaces a tower by a single primitive element with exact coordinate changes in both directions, so a computation can move between the tower and the one-generator form Hex.PolyQuot of HexNumberField.

Each operation checks its own result before returning it, and returns none otherwise. The correspondence library HexNumberFieldTowerMathlib proves that none never occurs, that arithmetic in a tower computes the corresponding complex arithmetic, and it states what each result means: the factors are irreducible and multiply back to the input, the adjoined generator has the requested complex value, and the splitting field contains every root.

Hex.NumberTower.Extension (T : Hex.NumberTower) : Type
Hex.NumberTower.Extension
  (T : Hex.NumberTower) : Type

Hex.NumberTower.Extension.mk

tower : Hex.NumberTower

embed : T.Elem → self.tower.Elem

gen : self.tower.Elem

root : Hex.AlgebraicRoot