Cyclotomic fields and a common evaluation grid

The rational cyclotomic field ℚ[X] / (X ^ (2 ^ e) + 1) of 2 ^ (e + 1)-th roots of unity, with its power basis, its primitive additive character on ZMod (2 ^ (e + 1)) and its regular representation by 2 ^ e × 2 ^ e rational matrices. Over any field, a Schwartz–Zippel argument shows that one fixed grid S ^ k simultaneously avoids the zeros of a whole list of nonzero polynomials of bounded total degree, provided S is large enough.

Main definitions

• Rational.CyclotomicRing.R: the cyclotomic quotient AdjoinRoot (X ^ (2 ^ e) + 1) over ℚ.
• Rational.CyclotomicRing.basis: its power basis indexed by Fin (2 ^ e).
• Rational.CyclotomicRing.character: the additive character of the adjoined root.
• Rational.CyclotomicRing.rho: the regular representation by rational matrices.

Main results

• Rational.CyclotomicRing.root_primitive: the adjoined root is a primitive root of unity of order 2 ^ (e + 1).
• Rational.FiniteGrid.det_totalDegree_le: total degree of a polynomial determinant.
• Rational.FiniteGrid.simultaneous: a grid avoiding all zeros of a list of polynomials.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/CyclotomicGrid.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

def Cslib.Circuits.Rational.CyclotomicRing.degree (e : ℕ) : ℕ

Degree of the chosen cyclotomic modulus.

def Cslib.Circuits.Rational.CyclotomicRing.dimension (e : ℕ) : ℕ

Order of the chosen root of unity.

theorem Cslib.Circuits.Rational.CyclotomicRing.degree_pos (e : ℕ) : 0 < degree e

theorem Cslib.Circuits.Rational.CyclotomicRing.dimension_pos (e : ℕ) : 0 < dimension e

instance Cslib.Circuits.Rational.CyclotomicRing.dimension_neZero (e : ℕ) : NeZero (dimension e)

The order of the root of unity is nonzero.

noncomputable def Cslib.Circuits.Rational.CyclotomicRing.modulus (e : ℕ) : Polynomial ℚ

The cyclotomic modulus for roots of unity of power-of-two order.

theorem Cslib.Circuits.Rational.CyclotomicRing.modulus_eq_cyclotomic (e : ℕ) : modulus e = Polynomial.cyclotomic (dimension e) ℚ

instance Cslib.Circuits.Rational.CyclotomicRing.modulus_irreducible (e : ℕ) : Fact (Irreducible (modulus e))

The modulus X ^ (2 ^ e) + 1 is the 2 ^ (e + 1)-th cyclotomic polynomial, hence irreducible over ℚ.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.CyclotomicRing.R (e : ℕ) : Type

The rational cyclotomic quotient used for the matrix construction.

theorem Cslib.Circuits.Rational.CyclotomicRing.modulus_monic (e : ℕ) : (modulus e).Monic

theorem Cslib.Circuits.Rational.CyclotomicRing.modulus_natDegree (e : ℕ) : (modulus e).natDegree = degree e

noncomputable def Cslib.Circuits.Rational.CyclotomicRing.powerBasis (e : ℕ) : PowerBasis ℚ (R e)

The quotient's power basis generated by the adjoined root.

noncomputable def Cslib.Circuits.Rational.CyclotomicRing.basis (e : ℕ) : Module.Basis (Fin (degree e)) ℚ (R e)

Reindex the power basis by the explicit cyclotomic degree.

theorem Cslib.Circuits.Rational.CyclotomicRing.basis_apply (e : ℕ) (i : Fin (degree e)) : (basis e) i = AdjoinRoot.root (modulus e) ^ ↑i

instance Cslib.Circuits.Rational.CyclotomicRing.charZero (e : ℕ) : CharZero (R e)

The cyclotomic quotient contains ℚ, so it has characteristic zero.

instance Cslib.Circuits.Rational.CyclotomicRing.finite (e : ℕ) : Module.Finite ℚ (R e)

The cyclotomic quotient is finite-dimensional over ℚ.

noncomputable def Cslib.Circuits.Rational.CyclotomicRing.intoComplex (e : ℕ) : R e →ₐ[ℚ] ℂ

An embedding of the cyclotomic quotient into the complex numbers.

theorem Cslib.Circuits.Rational.CyclotomicRing.root_primitive (e : ℕ) : IsPrimitiveRoot (AdjoinRoot.root (modulus e)) (dimension e)

The adjoined root is a primitive root of unity of order 2 ^ (e + 1). Since the modulus is irreducible, the quotient is a field, so invertibility in the regular representation can be tested at this single primitive root.

noncomputable def Cslib.Circuits.Rational.CyclotomicRing.character (e : ℕ) : AddChar (ZMod (dimension e)) (R e)

The additive character generated by the primitive cyclotomic root.

theorem Cslib.Circuits.Rational.CyclotomicRing.character_primitive (e : ℕ) : (character e).IsPrimitive

noncomputable def Cslib.Circuits.Rational.CyclotomicRing.rho (e : ℕ) : R e →ₐ[ℚ] Matrix (Fin (degree e)) (Fin (degree e)) ℚ

The regular rational matrix representation of the cyclotomic field.

theorem Cslib.Circuits.Rational.FiniteGrid.exists_eval_ne_zero {K : Type u_1} [Field K] {k : ℕ} (p : MvPolynomial (Fin k) K) (hp : p ≠ 0) (S : Finset K) (hS : p.totalDegree < S.card) : ∃ (x : Fin k → K), (∀ (i : Fin k), x i ∈ S) ∧ (MvPolynomial.eval x) p ≠ 0

The fixed grid, independent of the coefficients, finds a nonzero value.

theorem Cslib.Circuits.Rational.FiniteGrid.det_totalDegree_le {K : Type u_1} [Field K] {k : ℕ} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι (MvPolynomial (Fin k) K)) (d : ℕ) (hA : ∀ (i j : ι), (A i j).totalDegree ≤ d) : A.det.totalDegree ≤ Fintype.card ι * d

A determinant of polynomials of total degree at most d has total degree at most |ι| * d.

theorem Cslib.Circuits.Rational.FiniteGrid.simultaneous {K : Type u_1} [Field K] {k : ℕ} (P : List (MvPolynomial (Fin k) K)) (hP : ∀ p ∈ P, p ≠ 0) (d : ℕ) (hd : ∀ p ∈ P, p.totalDegree ≤ d) (S : Finset K) (hS : P.length * d < S.card) : ∃ (x : Fin k → K), (∀ (i : Fin k), x i ∈ S) ∧ ∀ p ∈ P, (MvPolynomial.eval x) p ≠ 0

The common grid specializes a list of determinant conditions simultaneously, rather than one formula gate at a time.