noncomputable def Hex.PolyQuot.definingPolynomial (p : ZPoly) : Polynomial ℚ

The monic rational associate used for the quotient-field comparison.

Equations

• Hex.PolyQuot.definingPolynomial p = (↑(Hex.DensePoly.leadingCoeff p))⁻¹ • HexPolyZMathlib.toPolyℚ p

theorem Hex.PolyQuot.definingPolynomial_monic (p : ZPoly) [p.CheckedIrreducible] : (definingPolynomial p).Monic

The rational defining polynomial is the monic associate of the checked integer polynomial.

theorem Hex.PolyQuot.natDegree_definingPolynomial (p : ZPoly) [p.CheckedIrreducible] : (definingPolynomial p).natDegree = DensePoly.natDegree p

Monic normalization preserves the executable defining degree.

theorem Hex.PolyQuot.definingPolynomial_irreducible (p : ZPoly) [p.CheckedIrreducible] : Irreducible (definingPolynomial p)

The monic rational defining polynomial remains irreducible.

noncomputable def Hex.PolyQuot.toAdjoinRoot {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) : AdjoinRoot (definingPolynomial p)

Send reduced executable coordinates to the corresponding AdjoinRoot class. This function is defined before a ring structure is installed on Hex.PolyQuot.

Equations

• a.toAdjoinRoot = (AdjoinRoot.mk (Hex.PolyQuot.definingPolynomial p)) (HexPolyMathlib.toPolynomial a.coeffs)

theorem Hex.PolyQuot.toAdjoinRoot_bijective {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : Function.Bijective toAdjoinRoot

Reduced coordinates give a bijection with the quotient by the monic rational defining relation.

theorem Hex.PolyQuot.eval_definingPolynomial {p : ZPoly} [p.CheckedIrreducible] (rep : RefinedIsolation p) : Polynomial.eval₂ (algebraMap ℚ ℂ) rep.root (definingPolynomial p) = 0

The selected complex root zeros the monic rational defining polynomial.

noncomputable def Hex.PolyQuot.rootHom {p : ZPoly} [p.CheckedIrreducible] (rep : RefinedIsolation p) : AdjoinRoot (definingPolynomial p) →+* ℂ

Evaluate the quotient presentation at its selected complex root.

Equations

• Hex.PolyQuot.rootHom rep = AdjoinRoot.lift (algebraMap ℚ ℂ) rep.root ⋯

theorem Hex.PolyQuot.rootHom_toAdjoinRoot {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (rootHom rep) a.toAdjoinRoot = a.toComplex rep h

Quotient evaluation agrees with direct evaluation of executable coordinates.

theorem Hex.PolyQuot.toComplex_injective {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : Function.Injective fun (a : PolyQuot p x) => a.toComplex rep h

Evaluation at the selected root is injective for a checked irreducible presentation.

theorem Hex.PolyQuot.isZero_iff {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) : a.isZero = true ↔ a = 0

The executable coordinate test recognizes precisely the zero element.

theorem Hex.PolyQuot.inverse_gcd_size {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (ha : a.isZero = false) : (a.coeffs.xgcdLeftMonic p.toRatPoly).gcd.size = 1

Irreducibility and the reduced-degree invariant make the executable gcd guard in Hex.PolyQuot.inv succeed for every nonzero element.

theorem Hex.PolyQuot.map_zero {p : ZPoly} {x : SimpleRoot p} (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : toComplex 0 rep h = 0

Fixed-presentation zero evaluates to complex zero.

theorem Hex.PolyQuot.map_one {p : ZPoly} {x : SimpleRoot p} (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : toComplex 1 rep h = 1

Fixed-presentation one evaluates to complex one.

theorem Hex.PolyQuot.map_neg {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (-a).toComplex rep h = -a.toComplex rep h

Fixed-presentation negation agrees with complex negation.

theorem Hex.PolyQuot.map_sub {p : ZPoly} {x : SimpleRoot p} (a b : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (a - b).toComplex rep h = a.toComplex rep h - b.toComplex rep h

Fixed-presentation subtraction agrees with complex subtraction.

theorem Hex.PolyQuot.map_smul {p : ZPoly} {x : SimpleRoot p} (q : ℚ) (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (q • a).toComplex rep h = ↑q * a.toComplex rep h

The executable rational scalar action is semantic scalar multiplication.

theorem Hex.PolyQuot.map_inv {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : a⁻¹.toComplex rep h = (a.toComplex rep h)⁻¹

Executable extended-GCD inversion agrees with complex inversion.

theorem Hex.PolyQuot.map_div {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a b : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (a / b).toComplex rep h = a.toComplex rep h / b.toComplex rep h

Fixed-presentation division agrees with complex division.

theorem Hex.PolyQuot.map_natPow {p : ZPoly} {x : SimpleRoot p} (a : PolyQuot p x) (n : ℕ) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (a.natPow n).toComplex rep h = a.toComplex rep h ^ n

Executable natural powers preserve the selected interpretation.

theorem Hex.PolyQuot.map_intPow {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (n : ℤ) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (a.intPow n).toComplex rep h = a.toComplex rep h ^ n

Executable integer powers preserve the selected interpretation.

@[reducible]

noncomputable def Hex.PolyQuot.field (p : ZPoly) (x : SimpleRoot p) [p.CheckedIrreducible] : Field (PolyQuot p x)

The law-bearing field whose operations are exactly the existing executable reduced-coordinate operations.

Equations

• Hex.PolyQuot.field p x = Function.Injective.field (fun (a : Hex.PolyQuot p x) => a.toComplex (Quot.out x) ⋯) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem Hex.PolyQuot.QAdjoinField.factIrreducible (p : ZPoly) [p.CheckedIrreducible] : Fact (Irreducible (definingPolynomial p))

Opt-in irreducibility witness for the monic rational defining polynomial.

@[instance_reducible]

noncomputable def Hex.PolyQuot.QAdjoinField.instFieldOfCheckedIrreducible_hexNumberFieldMathlib (p : ZPoly) (x : SimpleRoot p) [p.CheckedIrreducible] : Field (PolyQuot p x)

Opt-in field instance for a checked fixed presentation. It is scoped so computational imports never acquire a noncomputable proof dictionary. Opening the scope makes field notation proof-bearing and therefore noncomputable; executable code should use the unscoped operations instead.

Equations

• Hex.PolyQuot.QAdjoinField.instFieldOfCheckedIrreducible_hexNumberFieldMathlib p x = Hex.PolyQuot.field p x

theorem Hex.PolyQuot.QAdjoinField.instCharZero_hexNumberFieldMathlib (p : ZPoly) (x : SimpleRoot p) [p.CheckedIrreducible] : CharZero (PolyQuot p x)

A checked rational presentation has characteristic zero.

theorem Hex.PolyQuot.toAdjoinRoot_zero {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : toAdjoinRoot 0 = 0

The quotient comparison preserves executable zero.

theorem Hex.PolyQuot.toAdjoinRoot_one {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : toAdjoinRoot 1 = 1

The quotient comparison preserves executable one.

theorem Hex.PolyQuot.toAdjoinRoot_add {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a b : PolyQuot p x) : (a + b).toAdjoinRoot = a.toAdjoinRoot + b.toAdjoinRoot

The quotient comparison preserves executable addition.

theorem Hex.PolyQuot.toAdjoinRoot_mul {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a b : PolyQuot p x) : (a * b).toAdjoinRoot = a.toAdjoinRoot * b.toAdjoinRoot

The quotient comparison preserves executable multiplication.

theorem Hex.PolyQuot.toAdjoinRoot_smul {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (q : ℚ) (a : PolyQuot p x) : (q • a).toAdjoinRoot = q • a.toAdjoinRoot

The quotient comparison preserves executable rational scalar multiplication.

noncomputable def Hex.PolyQuot.toAdjoinRootHom {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : PolyQuot p x →+* AdjoinRoot (definingPolynomial p)

The reduced-coordinate comparison as a ring homomorphism.

Equations

• Hex.PolyQuot.toAdjoinRootHom = { toFun := Hex.PolyQuot.toAdjoinRoot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def Hex.PolyQuot.adjoinRootEquiv {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] : PolyQuot p x ≃+* AdjoinRoot (definingPolynomial p)

Reduced executable coordinates are ring-equivalent to the monic rational AdjoinRoot presentation.

Equations

• Hex.PolyQuot.adjoinRootEquiv = RingEquiv.ofBijective Hex.PolyQuot.toAdjoinRootHom ⋯

@[simp]

theorem Hex.PolyQuot.adjoinRootEquiv_apply {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) : adjoinRootEquiv a = a.toAdjoinRoot

The packaged ring equivalence acts by the underlying comparison map.

noncomputable def Hex.PolyQuot.embedding {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : PolyQuot p x →+* ℂ

Evaluation at the selected root as an injective ring homomorphism.

Equations

• Hex.PolyQuot.embedding rep h = { toFun := fun (a : Hex.PolyQuot p x) => a.toComplex rep h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Hex.PolyQuot.embedding_apply {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a : PolyQuot p x) (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : (embedding rep h) a = a.toComplex rep h

The packaged ring homomorphism acts by evaluation at the selected root.

theorem Hex.PolyQuot.embedding_injective {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (rep : RefinedIsolation p) (h : SimpleRoot.mk rep = x) : Function.Injective ⇑(embedding rep h)

The selected-root ring homomorphism is an embedding.

theorem Hex.PolyQuot.eq_iff_toComplex {p : ZPoly} {x : SimpleRoot p} [p.CheckedIrreducible] (a b : PolyQuot p x) (rep : RefinedIsolation p) (hrep : SimpleRoot.mk rep = x) : a = b ↔ a.toComplex rep hrep = b.toComplex rep hrep

Equality in a checked presentation is exactly equality of interpreted complex values.