The characteristic-two Artin–Schreier tower step

The polynomial X² + X + a has no root exactly when its quadratic quotient is an extension field. In that extension, multiplication of a by the canonical root supplies the next no-root parameter. These are algebraic correctness lemmas for the explicit binary tower constructor; they do not choose a root by searching through the field.

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.quadratic {K : Type u_1} [Field K] (a : K) : Polynomial K

The monic quadratic used by the characteristic-two tower.

Equations

• MIPRE.LowDegree.BinaryArtinSchreier.quadratic a = Polynomial.X ^ 2 + Polynomial.X + Polynomial.C a

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.quadratic_natDegree {K : Type u_1} [Field K] (a : K) : (quadratic a).natDegree = 2

theorem MIPRE.LowDegree.BinaryArtinSchreier.quadratic_monic {K : Type u_1} [Field K] (a : K) : (quadratic a).Monic

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.quadratic_eval {K : Type u_1} [Field K] (a x : K) : Polynomial.eval x (quadratic a) = x ^ 2 + x + a

theorem MIPRE.LowDegree.BinaryArtinSchreier.quadratic_irreducible_iff {K : Type u_1} [Field K] (a : K) : Irreducible (quadratic a) ↔ ∀ (x : K), x ^ 2 + x + a ≠ 0

Degree two reduces irreducibility to the explicit no-root property.

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.quadraticBasis {K : Type u_1} [Field K] (a : K) : Module.Basis (Fin 2) K (AdjoinRoot (quadratic a))

The specified basis of every monic quadratic quotient, indexed by Fin 2.

Equations

• MIPRE.LowDegree.BinaryArtinSchreier.quadraticBasis a = (AdjoinRoot.powerBasis' ⋯).basis.reindex (finCongr ⋯)

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.quadraticBasis_apply {K : Type u_1} [Field K] (a : K) (i : Fin 2) : (quadraticBasis a) i = AdjoinRoot.root (quadratic a) ^ ↑i

theorem MIPRE.LowDegree.BinaryArtinSchreier.exists_coordinates {K : Type u_1} [Field K] (a : K) (x : AdjoinRoot (quadratic a)) : ∃ (u : K) (v : K), x = (algebraMap K (AdjoinRoot (quadratic a))) u + (algebraMap K (AdjoinRoot (quadratic a))) v * AdjoinRoot.root (quadratic a)

Each element has its two coefficients in the specified quadratic power basis.

theorem MIPRE.LowDegree.BinaryArtinSchreier.linear_coeff_eq_zero {K : Type u_1} [Field K] (a u v : K) (h : (algebraMap K (AdjoinRoot (quadratic a))) u + (algebraMap K (AdjoinRoot (quadratic a))) v * AdjoinRoot.root (quadratic a) = 0) : v = 0

The coefficient of the root in a zero linear combination is zero.

theorem MIPRE.LowDegree.BinaryArtinSchreier.root_relation {K : Type u_1} [Field K] (a : K) : AdjoinRoot.root (quadratic a) ^ 2 + AdjoinRoot.root (quadratic a) + (algebraMap K (AdjoinRoot (quadratic a))) a = 0

The root of the quadratic satisfies its defining Artin–Schreier equation.

theorem MIPRE.LowDegree.BinaryArtinSchreier.next_quadratic_irreducible {K : Type u_1} [Field K] [CharP K 2] (a : K) (ha : Irreducible (quadratic a)) : have this := ⋯; Irreducible (quadratic ((algebraMap K (AdjoinRoot (quadratic a))) a * AdjoinRoot.root (quadratic a)))

One no-root quadratic gives the next one over its explicitly presented extension.

theorem MIPRE.LowDegree.BinaryArtinSchreier.next_parameter_eq_cubic {K : Type u_1} [Field K] [CharP K 2] (a : K) (ha : Irreducible (quadratic a)) : have this := ⋯; (algebraMap K (AdjoinRoot (quadratic a))) a * AdjoinRoot.root (quadratic a) = AdjoinRoot.root (quadratic a) ^ 3 + AdjoinRoot.root (quadratic a) ^ 2

The multiplicative next parameter is the uniform cubic expression in the new root.

theorem MIPRE.LowDegree.BinaryArtinSchreier.cubic_quadratic_irreducible {K : Type u_1} [Field K] [CharP K 2] (a : K) (ha : Irreducible (quadratic a)) : have this := ⋯; Irreducible (quadratic (AdjoinRoot.root (quadratic a) ^ 3 + AdjoinRoot.root (quadratic a) ^ 2))

The source's cubic expression therefore preserves the no-root invariant.

theorem MIPRE.LowDegree.BinaryArtinSchreier.binary_initial_irreducible : Irreducible (quadratic 1)

The initial binary quadratic has no root.

theorem MIPRE.LowDegree.BinaryArtinSchreier.root_not_mem_range {K : Type u_1} [Field K] (a : K) (ha : Irreducible (quadratic a)) : AdjoinRoot.root (quadratic a) ∉ (algebraMap K (AdjoinRoot (quadratic a))).range

The quadratic root cannot already lie in the original field.

theorem MIPRE.LowDegree.BinaryArtinSchreier.comp_quadratic_irreducible {K : Type u_1} [Field K] [CharP K 2] [Finite K] [Algebra (ZMod 2) K] [FiniteDimensional (ZMod 2) K] (t : ℕ) (hK : Module.finrank (ZMod 2) K = 2 ^ t) (a : K) (ha : Irreducible (quadratic a)) (g : Polynomial (ZMod 2)) (hg : g.Monic) (hd : g.natDegree = 2 ^ t) (hz : (Polynomial.aeval a) g = 0) : Irreducible (g.comp (quadratic 0))

A binary annihilating polynomial of the old dimension gives the next irreducible polynomial by substitution of X² + X. The hypothesis on g is supplied by the explicit Frobenius orbit product, after coefficient descent.

theorem MIPRE.LowDegree.BinaryArtinSchreier.comp_quadratic_cubic_irreducible {K : Type u_1} [Field K] [CharP K 2] [Finite K] [Algebra (ZMod 2) K] [FiniteDimensional (ZMod 2) K] (t : ℕ) (hK : Module.finrank (ZMod 2) K = 2 ^ t) (a : K) (ha : Irreducible (quadratic a)) (g : Polynomial (ZMod 2)) (hg : g.Monic) (hd : g.natDegree = 2 ^ t) (hz : (Polynomial.aeval a) g = 0) : have this := ⋯; Irreducible (quadratic (AdjoinRoot.root (g.comp (quadratic 0)) ^ 3 + AdjoinRoot.root (g.comp (quadratic 0)) ^ 2))

Flattening the quadratic extension preserves the cubic no-root invariant. Only the canonical embedding of the flat quotient is required; no search for an isomorphism or a field element is part of this argument.

theorem MIPRE.LowDegree.BinaryArtinSchreier.cubic_irreducible_congr {f g : Polynomial (ZMod 2)} (hfg : f = g) (hf : Irreducible f) (hg : Irreducible g) (hc : have this := ⋯; Irreducible (quadratic (AdjoinRoot.root g ^ 3 + AdjoinRoot.root g ^ 2))) : have this := ⋯; Irreducible (quadratic (AdjoinRoot.root f ^ 3 + AdjoinRoot.root f ^ 2))

Transport the canonical-root cubic invariant across equality of binary moduli.