30.4. Splitting and flattening🔗

(X² − 2)(X² − 3) needs two genuine extensions to split. The splitting field has dimension four and the four roots square to 2 or 3:

def biquadratic : Poly NumberTower.rat :=
  liftZPoly NumberTower.rat #p[6, 0, -5, 0, 1]

#guard
  let S := split NumberTower.rat biquadratic
  S.extension.tower.dim = 4 &&
    let rs := S.roots.toArray
    rs.size = 4 && rs.all fun r =>
      r.2 = 1 &&
        (coeffs (r.1 * r.1) = #[2, 0, 0, 0] ||
          coeffs (r.1 * r.1) = #[3, 0, 0, 0])

Building the same field by hand, ℚ(√2)(√3), gives a tower whose elements have coordinates over two successive generators. Arithmetic there is coordinate arithmetic: a power of √2 + √3 costs a few multiplications of coordinate vectors, whereas the same power of the canonical Hex.AlgebraicNumber recomputes a minimal polynomial at every step. Hex.NumberTower.flatten is the primitive element theorem as a function. It returns a Hex.NumberTower.Flattening: a single algebraic number γ generating the whole tower, and the coordinate changes between the tower and the field ℚ(γ):

Here γ has the quartic above as minimal polynomial, so it is ±√2 ± √3, and √2 = (γ³ − 9γ)/2 in terms of it. Converting a tower element through the flattening and then to a canonical number agrees with computing directly:

def Q23 : Extension T2 := adjoin T2 sqrt3.toRoot
abbrev T23 : NumberTower := Q23.tower
def s2 : Elem T23 := Q23.embed r2
def s3 : Elem T23 := Q23.gen

#guard T23.dim = 4
#guard (s2 + s3) * (s2 - s3) = -1

def F : Flattening T23 := flatten T23

#guard F.root.p = #p[1, 0, -10, 0, 1]
#guard (F.toPrimitive s2).coeffs = #p[0, -9 / 2, 0, 1 / 2]
#guard F.fromPrimitive (F.toPrimitive s3) = s3
-- (√2 + √3)^10 = 47525 + 19402√6 over the basis
-- 1, √2, √3, √6.
#guard coeffs ((s2 + s3) ^ 10) = #[47525, 0, 0, 19402]
#guard (F.toPrimitive ((s2 + s3) ^ 10)).toAlgebraicNumber =
  (sqrt2 + sqrt3) ^ 10

end HexNumberFieldTowerChapter

def

Hex.NumberTower.split? {T : Hex.NumberTower} (f : T.Poly) :
  Option (T.Splitting f)
Hex.NumberTower.split?
  {T : Hex.NumberTower} (f : T.Poly) :
  Option (T.Splitting f)

Construct an extension in which the input polynomial splits into linear factors, retaining multiplicities from checked factorization.

def

Hex.NumberTower.flatten? (T : Hex.NumberTower) : Option T.Flattening
Hex.NumberTower.flatten?
  (T : Hex.NumberTower) :
  Option T.Flattening

Replace a checked tower by one canonical primitive-element presentation. The result is returned only after exact generator recovery, a tower-basis round trip, and the primitive polynomial relation succeed.

The Option-valued operations are the computational library's; the total forms Hex.NumberTower.adjoin, Hex.NumberTower.factor, Hex.NumberTower.split and Hex.NumberTower.flatten come from the Mathlib companion, which unwraps each option with its completeness theorem.