Binary composed-sum polynomials as products of Frobenius translates

noncomputable def MIPRE.LowDegree.BinaryQuotient.translatedPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (g : Polynomial (ZMod 2)) (x : R) : Polynomial R

Translate a binary polynomial by an element of the ambient binary algebra.

Equations

• MIPRE.LowDegree.BinaryQuotient.translatedPolynomial g x = (Polynomial.map (algebraMap (ZMod 2) R) g).comp (Polynomial.X + Polynomial.C x)

noncomputable def MIPRE.LowDegree.BinaryQuotient.composedSumPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (g : Polynomial (ZMod 2)) (x : R) (n : ℕ) : Polynomial R

Product of all specified Frobenius translates of a binary polynomial.

Equations

• MIPRE.LowDegree.BinaryQuotient.composedSumPolynomial g x n = (List.ofFn fun (i : Fin n) => MIPRE.LowDegree.BinaryQuotient.translatedPolynomial g (x ^ 2 ^ ↑i)).prod

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.composedSumPolynomial_zero {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (g : Polynomial (ZMod 2)) (x : R) : composedSumPolynomial g x 0 = 1

theorem MIPRE.LowDegree.BinaryQuotient.composedSumPolynomial_succ {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (g : Polynomial (ZMod 2)) (x : R) (n : ℕ) : composedSumPolynomial g x (n + 1) = translatedPolynomial g x * composedSumPolynomial g (x ^ 2) n

theorem MIPRE.LowDegree.BinaryQuotient.composedSumPolynomial_succ' {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (g : Polynomial (ZMod 2)) (x : R) (n : ℕ) : composedSumPolynomial g x (n + 1) = composedSumPolynomial g x n * translatedPolynomial g (x ^ 2 ^ n)

theorem MIPRE.LowDegree.BinaryQuotient.translatedPolynomial_monic {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (g : Polynomial (ZMod 2)) (hg : g.Monic) (x : R) : (translatedPolynomial g x).Monic

Translating a monic polynomial preserves monicity.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.natDegree_translatedPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] [IsDomain R] (g : Polynomial (ZMod 2)) (x : R) : (translatedPolynomial g x).natDegree = g.natDegree

theorem MIPRE.LowDegree.BinaryQuotient.composedSumPolynomial_monic {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (g : Polynomial (ZMod 2)) (hg : g.Monic) (x : R) (n : ℕ) : (composedSumPolynomial g x n).Monic

The product is monic even when its translates repeat.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.natDegree_composedSumPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] [IsDomain R] (g : Polynomial (ZMod 2)) (hg : g.Monic) (x : R) (n : ℕ) : (composedSumPolynomial g x n).natDegree = n * g.natDegree

theorem MIPRE.LowDegree.BinaryQuotient.map_frobenius_translatedPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] [CharP R 2] (g : Polynomial (ZMod 2)) (x : R) : Polynomial.map (frobenius R 2) (translatedPolynomial g x) = translatedPolynomial g (x ^ 2)

Coefficient Frobenius commutes with translation of a binary polynomial.

theorem MIPRE.LowDegree.BinaryQuotient.map_frobenius_composedSumPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] [CharP R 2] (g : Polynomial (ZMod 2)) (x : R) (n : ℕ) : Polynomial.map (frobenius R 2) (composedSumPolynomial g x n) = composedSumPolynomial g (x ^ 2) n

Coefficient Frobenius shifts the translate orbit by one place.

theorem MIPRE.LowDegree.BinaryQuotient.map_frobenius_composedSumPolynomial_of_closed {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] [IsDomain R] [CharP R 2] (g : Polynomial (ZMod 2)) (hg : g.Monic) (x : R) (n : ℕ) (hx : x ^ 2 ^ n = x) : Polynomial.map (frobenius R 2) (composedSumPolynomial g x n) = composedSumPolynomial g x n

Closing the translate orbit fixes every product coefficient under Frobenius.

theorem MIPRE.LowDegree.BinaryQuotient.composedSumPolynomial_coeff_zero_or_one {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] [IsDomain R] [CharP R 2] (g : Polynomial (ZMod 2)) (hg : g.Monic) (x : R) (n : ℕ) (hx : x ^ 2 ^ n = x) (i : ℕ) : (composedSumPolynomial g x n).coeff i = 0 ∨ (composedSumPolynomial g x n).coeff i = 1

The coefficients of a closed product of binary translates are binary.

theorem MIPRE.LowDegree.BinaryQuotient.eval_composedSumPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] [CharP R 2] (g : Polynomial (ZMod 2)) (x y : R) (n : ℕ) (hn : 0 < n) (hy : (Polynomial.aeval y) g = 0) : Polynomial.eval (x + y) (composedSumPolynomial g x n) = 0

A nonempty translate product vanishes at the sum of the translating element and any root.

theorem MIPRE.LowDegree.BinaryQuotient.map_translatedPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] {S : Type u_2} [CommRing S] [Algebra (ZMod 2) S] (φ : R →ₐ[ZMod 2] S) (g : Polynomial (ZMod 2)) (x : R) : Polynomial.map φ.toRingHom (translatedPolynomial g x) = translatedPolynomial g (φ x)

Translation commutes with an algebra embedding of the coefficient field.

theorem MIPRE.LowDegree.BinaryQuotient.map_composedSumPolynomial {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] {S : Type u_2} [CommRing S] [Algebra (ZMod 2) S] (φ : R →ₐ[ZMod 2] S) (g : Polynomial (ZMod 2)) (x : R) (n : ℕ) : Polynomial.map φ.toRingHom (composedSumPolynomial g x n) = composedSumPolynomial g (φ x) n

The composed-sum product commutes with coefficient-field embeddings.