30.2. ℚ(√2)🔗

Every tower starts from Hex.NumberTower.rat, the tower with no extensions, whose elements are the rational numbers. Adjoining an algebraic number to a tower T returns an Hex.NumberTower.Extension of T: the new tower, the adjoined generator gen as an element of it, and the inclusion embed of the elements of T. The type Extension T names T because embed is a function out of Elem T. Coordinates in ℚ(√2) are the pair #[a, b] standing for a + b√2:

open Hex Hex.NumberTower

namespace HexNumberFieldTowerChapter

def sqrt2 : AlgebraicNumber :=
  (ZPoly.algebraicRoots #p[-2, 0, 1])[1]!
def sqrt3 : AlgebraicNumber :=
  (ZPoly.algebraicRoots #p[-3, 0, 1])[1]!

-- `adjoin` is the Mathlib companion library's total
-- form of `adjoin?`, which never returns `none`
-- (`adjoin?_isSome`).
def Q2 : Extension NumberTower.rat :=
  adjoin NumberTower.rat sqrt2.toRoot
abbrev T2 : NumberTower := Q2.tower
def r2 : Elem T2 := Q2.gen

#guard T2.dim = 2
#guard coeffs (r2 * r2) = #[2, 0]
#guard coeffs (Q2.embed (ofRat NumberTower.rat 5)) = #[5, 0]

-- √2 is already there: adjoining it again changes nothing.
#guard (adjoin T2 sqrt2.toRoot).tower.dim = 2

def

Hex.NumberTower.adjoin? (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot) : Option T.Extension
Hex.NumberTower.adjoin?
  (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot) :
  Option T.Extension

Adjoin the specified absolute algebraic root. A selected linear factor produces the identity extension; a nonlinear factor is admitted only through Hex.NumberTower.Internal.extend?, which reruns structural, relative-irreducibility, and fixed- embedding checks before constructing the new carrier index.