29.10. Choosing a field for several values
Hex.QAdjoin.ofAlgebraic? expresses a value in a chosen generator's
power basis. It returns none precisely when the value is outside that
field. Another root of the same polynomial need not lie in the chosen
field: the nonreal roots of X³ - 2 are outside the field generated by its
real root. The negative square root does lie in the field generated by the
positive square root.
Hex.QAdjoin.ofAlgebraics? converts an array with one shared power
table and returns an option for each input, preserving order and duplicates.
Hex.QAdjoin.common instead computes one primitive generator and
coordinates for every input. Its dependent entries array has type
Array (QAdjoin generator). Empty and all-zero arrays use generator zero.
The primitive-element search and coordinate recovery can be expensive;
once converted, field arithmetic uses rational coordinates.
open HexNumberFieldChapter
#guard (QAdjoin.ofAlgebraic? sqrt2 (-sqrt2)).isSome
#guard (QAdjoin.ofAlgebraic? sqrt2 sqrt3).isNone
def := QAdjoin.common #[sqrt2, sqrt3, sqrt2]
#guard sharedField.entries.map (·.toAlgebraicNumber) == #[sqrt2, sqrt3, sqrt2]
example (a b : AlgebraicNumber) (c : QAdjoin a)
(h : QAdjoin.ofAlgebraic? a b = some c) : c.toAlgebraicNumber = b :=
QAdjoin.ofAlgebraic?_sound a b h
For the chosen generator γ = √2 + √3, the coordinates are
√2 = (γ³ - 9γ)/2 and √3 = (11γ - γ³)/2.
Hex.QAdjoin.ofAlgebraic?_isSome_iff proves the membership decision;
Hex.QAdjoin.common_get proves that converting each common-field
entry back recovers the corresponding input.
The Mathlib companion provides the field's algebraic-closure instances, using completeness of the executable polynomial root solver:
example : IsAlgClosed AlgebraicNumber := inferInstance
example : IsAlgClosure ℚ AlgebraicNumber := inferInstance
example : Algebra.IsAlgebraic ℚ AlgebraicNumber := inferInstance