Extracting polynomial factors from primitive quotient components

An idempotent represented by E corresponds to the factor gcd(f,E-1). Its multiples are exactly the polynomials annihilated by that component. Primitive-component inverses therefore prove irreducibility without a Chinese remainder construction or an enumeration of the quotient ring.

noncomputable def MIPRE.LowDegree.BinaryQuotient.componentFactor (f E : Polynomial (ZMod 2)) : Polynomial (ZMod 2)

The factor supported by the component represented by E.

Equations

• MIPRE.LowDegree.BinaryQuotient.componentFactor f E = gcd f (E - 1)

theorem MIPRE.LowDegree.BinaryQuotient.componentFactor_dvd_iff (f E H : Polynomial (ZMod 2)) (he : (AdjoinRoot.mk f) E * (AdjoinRoot.mk f) E = (AdjoinRoot.mk f) E) : componentFactor f E ∣ H ↔ (AdjoinRoot.mk f) E * (AdjoinRoot.mk f) H = 0

An idempotent's supported factor describes its polynomial annihilator.

theorem MIPRE.LowDegree.BinaryQuotient.componentFactor_prime (f E : Polynomial (ZMod 2)) (hf : f ≠ 0) [Finite (AdjoinRoot f)] (hsq : Function.Bijective fun (x : AdjoinRoot f) => x * x) (he : PrimitiveBinaryComponent ((AdjoinRoot.mk f) E)) : Prime (componentFactor f E)

A primitive component of a quotient with bijective squaring yields a prime factor.

theorem MIPRE.LowDegree.BinaryQuotient.componentFactor_irreducible (f E : Polynomial (ZMod 2)) (hf : f ≠ 0) [Finite (AdjoinRoot f)] (hsq : Function.Bijective fun (x : AdjoinRoot f) => x * x) (he : PrimitiveBinaryComponent ((AdjoinRoot.mk f) E)) : Irreducible (componentFactor f E)

Irreducibility follows from the primitive-component primality criterion.

theorem MIPRE.LowDegree.BinaryQuotient.componentFactor_monic (f E : Polynomial (ZMod 2)) (hf : f ≠ 0) : (componentFactor f E).Monic

Every nonzero quotient modulus has a monic supported gcd factor.

theorem MIPRE.LowDegree.BinaryQuotient.componentFactor_isCoprime (f E H : Polynomial (ZMod 2)) (he : Irreducible (componentFactor f E)) (heh : (AdjoinRoot.mk f) E * (AdjoinRoot.mk f) H = 0) : IsCoprime (componentFactor f E) (componentFactor f H)

Orthogonal components cannot share a nonunit supported factor.

theorem MIPRE.LowDegree.BinaryQuotient.componentFactors_prod (f : Polynomial (ZMod 2)) (hf : f.Monic) [Finite (AdjoinRoot f)] (hsq : Function.Bijective fun (x : AdjoinRoot f) => x * x) {n : ℕ} (E : Fin n → Polynomial (ZMod 2)) (he : ∀ (i : Fin n), PrimitiveBinaryComponent ((AdjoinRoot.mk f) (E i))) (horth : Pairwise fun (i j : Fin n) => (AdjoinRoot.mk f) (E i) * (AdjoinRoot.mk f) (E j) = 0) (hsum : ∑ i : Fin n, (AdjoinRoot.mk f) (E i) = 1) : ∏ i : Fin n, componentFactor f (E i) = f

A complete orthogonal primitive family reconstructs its monic quotient modulus.

theorem MIPRE.LowDegree.BinaryQuotient.componentFactors_list_prod (f : Polynomial (ZMod 2)) (hf : f.Monic) [Finite (AdjoinRoot f)] (hsq : Function.Bijective fun (x : AdjoinRoot f) => x * x) (l : List (Polynomial (ZMod 2))) (hl : ComponentFamily (List.map (⇑(AdjoinRoot.mk f)) l)) (he : ∀ E ∈ l, PrimitiveBinaryComponent ((AdjoinRoot.mk f) E)) : (List.map (componentFactor f) l).prod = f

The reconstruction theorem in the list representation used by the programs.

theorem MIPRE.LowDegree.BinaryQuotient.mk_polyOfBits (f : Polynomial (ZMod 2)) (a : Cost.BitStr) : (AdjoinRoot.mk f) (polyOfBits a) = BinaryPolynomial.evalBits (AdjoinRoot.root f) a

The quotient map reads coefficient bits by evaluation at its canonical root.

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.mk_polyOfBits_toBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : (AdjoinRoot.mk f) (polyOfBits (toBits f hf x)) = x

Canonical coordinate bits give a polynomial representative of the quotient element.

theorem MIPRE.LowDegree.BinaryQuotient.componentFactors_toBits_prod (f : Polynomial (ZMod 2)) (hf : f.Monic) [Finite (AdjoinRoot f)] (hsq : Function.Bijective fun (x : AdjoinRoot f) => x * x) (l : List (AdjoinRoot f)) (hl : ComponentFamily l) (he : ∀ e ∈ l, PrimitiveBinaryComponent e) : (List.map (fun (e : AdjoinRoot f) => componentFactor f (polyOfBits (toBits f hf e))) l).prod = f

Canonical representatives of a primitive component family yield the complete factorization.