Algebra of closed binary Frobenius-orbit polynomials

noncomputable def MIPRE.LowDegree.BinaryQuotient.orbitPolynomial {R : Type u_1} [CommRing R] (x : R) (n : ℕ) : Polynomial R

The monic polynomial product over a specified initial Frobenius orbit.

Equations

• MIPRE.LowDegree.BinaryQuotient.orbitPolynomial x n = (List.ofFn fun (i : Fin n) => Polynomial.X + Polynomial.C (x ^ 2 ^ ↑i)).prod

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomial_zero {R : Type u_1} [CommRing R] (x : R) : orbitPolynomial x 0 = 1

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomial_succ {R : Type u_1} [CommRing R] (x : R) (n : ℕ) : orbitPolynomial x (n + 1) = (Polynomial.X + Polynomial.C x) * orbitPolynomial (x ^ 2) n

Splitting off the first conjugate shifts the remaining orbit by squaring.

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomial_succ' {R : Type u_1} [CommRing R] (x : R) (n : ℕ) : orbitPolynomial x (n + 1) = orbitPolynomial x n * (Polynomial.X + Polynomial.C (x ^ 2 ^ n))

Splitting off the last conjugate gives the other endpoint of the same product.

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomial_monic {R : Type u_1} [CommRing R] (x : R) (n : ℕ) : (orbitPolynomial x n).Monic

Every orbit polynomial is monic, including the empty orbit.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.natDegree_orbitPolynomial {R : Type u_1} [CommRing R] [Nontrivial R] (x : R) (n : ℕ) : (orbitPolynomial x n).natDegree = n

The degree is the specified orbit length even when conjugates repeat.

theorem MIPRE.LowDegree.BinaryQuotient.map_frobenius_orbitPolynomial {R : Type u_1} [CommRing R] [CharP R 2] (x : R) (n : ℕ) : Polynomial.map (frobenius R 2) (orbitPolynomial x n) = orbitPolynomial (x ^ 2) n

Applying Frobenius to coefficients shifts the starting element by one conjugate.

theorem MIPRE.LowDegree.BinaryQuotient.map_frobenius_orbitPolynomial_of_closed {R : Type u_1} [CommRing R] [IsDomain R] [CharP R 2] (x : R) (n : ℕ) (hx : x ^ 2 ^ n = x) : Polynomial.map (frobenius R 2) (orbitPolynomial x n) = orbitPolynomial x n

A closed orbit gives a polynomial fixed by coefficient Frobenius.

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomial_coeff_zero_or_one {R : Type u_1} [CommRing R] [IsDomain R] [CharP R 2] (x : R) (n : ℕ) (hx : x ^ 2 ^ n = x) (i : ℕ) : (orbitPolynomial x n).coeff i = 0 ∨ (orbitPolynomial x n).coeff i = 1

Coefficients of a closed binary orbit polynomial belong to the prime field.

theorem MIPRE.LowDegree.BinaryQuotient.eval_orbitPolynomial {R : Type u_1} [CommRing R] [CharP R 2] (x : R) (n : ℕ) (hn : 0 < n) : Polynomial.eval x (orbitPolynomial x n) = 0

A nonempty binary orbit product vanishes at its starting element.