Univariate skew polynomials

Given a ring R and an endomorphism φ on R the skew polynomials over R are polynomials $$\sum_{i= 0}^n a_iX^n, n\geq 0, a_i\in R$$ where the addition is the usual addition of polynomials $$\sum_{i= 0}^n a_iX^n + \sum_{i= 0}^n b_iX^n= \sum_{i= 0}^n (a_i + b_i)X^n.$$ The multiplication, however, is determined by $$Xa = \varphi (a)X$$ by extending it to all polynomials in the obvious way.

Skew polynomials are represented as SkewMonoidAlgebra R (Multiplicative ℕ), where R is usually at least a Semiring. In this file, we define SkewPolynomial and provide basic instances.

Note: To register the endomorphism φ see notation below.

Notation

The endomorphism φ is implemented using some action of Multiplicative ℕ on R. From this action, φ is an abbrev denoting $(\text{ofAdd } 1) \cdot a := \varphi(a)$.

Users that want to work with a specific map φ should introduce an action of Multiplicative ℕ on R. Specifying that this action is a MulSemiringAction amounts to saying that φ is an endomorphism.

Furthermore, with this notation φ^[n](a) = (ofAdd n) • a, see φ_iterate_apply.

Main definitions

• SkewPolynomial.monomial n a is the skew polynomial a X ^ n. Note that SkewPolynomial.monomial n is defined as an R-linear map.
• SkewPolynomial.C a is the constant skew polynomial a. Note that C is defined as an additive homomorphism.
• SkewPolynomial.CRingHom a is the constant skew polynomial a, as a ring homomorphism. This requires to assume [MulSemiringAction (Multiplicative ℕ) R].
• SkewPolynomial.X is the skew polynomial X, i.e., SkewPolynomial.monomial 1 1.
• p.sum f is ∑ n ∈ p.support, f n (p.coeff n), i.e., one sums the values of functions applied to coefficients of the polynomial p.
• SkewPolynomial.coeff p n is the coefficient of X ^ n in p.

Implementation notes

The implementation uses Multiplicative ℕ instead of ℕ, since Mathlib does not contain an additive version of SkewMonoidAlgebra.

This decision was made because we use the type class MulSemiringAction to specify the properties the action needs to respect for associativity. There is no version of this in Mathlib that uses an acting AddMonoid M and so we need to use Multiplicative ℕ for the action.

For associativity to hold, there should be an instance of MulSemiringAction (Multiplicative ℕ) R present in the context. For example, in the context of $\mathbb{F}_q$-linear polynomials, this can be the $q$-th Frobenius endomorphism - so $\varphi(a) = a^q$.

Reference

The definition is inspired by Chapter 3 of [Papikian2023].

Tags

Skew Polynomials, Twisted Polynomials.

TODO :

• Add algebra instance

Note that [ore33] proposes a more general definition of skew polynomial ring, where the multiplication is determined by $Xa = \varphi (a)X + δ (a)$, where φ is as above and δ is a derivation.

@[reducible, inline]

abbrev SkewPolynomial (R : Type u_1) [AddCommMonoid R] : Type u_1

The skew polynomials over R is the type of univariate polynomials over R endowed with a skewed convolution product.

Equations

• SkewPolynomial R = SkewMonoidAlgebra R (Multiplicative ℕ)

theorem SkewPolynomial.zero_def {R : Type u_1} [Semiring R] : 0 = 0

def SkewPolynomial.support {R : Type u_1} [Semiring R] (p : SkewPolynomial R) : Finset ℕ

The set of all n such that X^n has a non-zero coefficient.

Equations

• p.support = Finset.map { toFun := ⇑Multiplicative.toAdd, inj' := SkewPolynomial.support._proof_1 } (SkewMonoidAlgebra.support p)

theorem SkewPolynomial.support_eq_skewMonoidAlgebra_support {R : Type u_1} [Semiring R] (p : SkewPolynomial R) : p.support = Finset.map Multiplicative.toAdd.toEmbedding (SkewMonoidAlgebra.support p)

Though SkewPolynomial.support is not definiyionally equal to SkewMonoidAlgebra.support we can relate them using the following lemma.

@[simp]

theorem SkewPolynomial.support_zero {R : Type u_1} [Semiring R] : support 0 = ∅

@[simp]

theorem SkewPolynomial.support_eq_empty {R : Type u_1} [Semiring R] {p : SkewPolynomial R} : p.support = ∅ ↔ p = 0

theorem SkewPolynomial.card_support_eq_zero {R : Type u_1} [Semiring R] {p : SkewPolynomial R} : p.support.card = 0 ↔ p = 0

theorem SkewPolynomial.support_add {R : Type u_1} [Semiring R] {p q : SkewPolynomial R} : (p + q).support ⊆ p.support ∪ q.support

def SkewPolynomial.coeff {R : Type u_1} [Semiring R] (p : SkewPolynomial R) : ℕ → R

coeff p n is the coefficient of X ^ n in p.

Equations

• p.coeff n = SkewMonoidAlgebra.coeff p (Multiplicative.ofAdd n)

@[simp]

theorem SkewPolynomial.mem_support_iff {R : Type u_1} {n : ℕ} [Semiring R] {p : SkewPolynomial R} : n ∈ p.support ↔ p.coeff n ≠ 0

theorem SkewPolynomial.notMem_support_iff {R : Type u_1} {n : ℕ} [Semiring R] {p : SkewPolynomial R} : n ∉ p.support ↔ p.coeff n = 0

def SkewPolynomial.sum {R : Type u_1} [Semiring R] {S : Type u_5} [AddCommMonoid S] (p : SkewPolynomial R) (f : ℕ → R → S) : S

p.sum f is ∑ n ∈ p.support, f n (p.coeff n), i.e., one sums the values of functions applied to coefficients of the polynomial p.

Equations

• p.sum f = SkewMonoidAlgebra.sum p fun (n : Multiplicative ℕ) (r : R) => f (Multiplicative.toAdd n) r

theorem SkewPolynomial.sum_def' {R : Type u_1} [Semiring R] {S : Type u_5} [AddCommMonoid S] (p : SkewPolynomial R) (f : ℕ → R → S) : p.sum f = SkewMonoidAlgebra.sum p fun (n : Multiplicative ℕ) (r : R) => f (Multiplicative.toAdd n) r

For a skew polynomial p, p.sum f can be written in terms of SkewMonoidAlgebra.sum p.

theorem SkewPolynomial.sum_def {R : Type u_1} [Semiring R] {S : Type u_5} [AddCommMonoid S] (p : SkewPolynomial R) (f : ℕ → R → S) : p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

theorem SkewPolynomial.sum_sum_index {R : Type u_1} [Semiring R] {R' : Type u_5} {P : Type u_6} [AddCommMonoid P] [Semiring R'] {f : SkewPolynomial R} {g : ℕ → R → SkewPolynomial R'} {h : ℕ → R' → P} (h_zero : ∀ (a : ℕ), h a 0 = 0) (h_add : ∀ (a : ℕ) (b₁ b₂ : R'), h a (b₁ + b₂) = h a b₁ + h a b₂) : (f.sum g).sum h = f.sum fun (a : ℕ) (b : R) => (g a b).sum h

@[simp]

theorem SkewPolynomial.sum_zero {R : Type u_1} [Semiring R] {N : Type u_5} [AddCommMonoid N] {f : SkewPolynomial R} : (f.sum fun (x : ℕ) (x_1 : R) => 0) = 0

noncomputable def SkewPolynomial.monomial {R : Type u_1} (n : ℕ) [Semiring R] : R →ₗ[R] SkewPolynomial R

monomial s a is the monomial a * X ^ s.

Equations

• SkewPolynomial.monomial n = SkewMonoidAlgebra.lsingle R (Multiplicative.ofAdd n)

theorem SkewPolynomial.monomial_zero_right {R : Type u_1} (n : ℕ) [Semiring R] : (monomial n) 0 = 0

theorem SkewPolynomial.monomial_zero_one {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] : (monomial 0) 1 = 1

theorem SkewPolynomial.monomial_def {R : Type u_1} (n : ℕ) [Semiring R] (a : R) : (monomial n) a = SkewMonoidAlgebra.single (Multiplicative.ofAdd n) a

theorem SkewPolynomial.monomial_add {R : Type u_1} (n : ℕ) [Semiring R] (r s : R) : (monomial n) (r + s) = (monomial n) r + (monomial n) s

theorem SkewPolynomial.smul_monomial {R : Type u_1} (n : ℕ) [Semiring R] {S : Type u_5} [Semiring S] [Module S R] (a : S) (b : R) : a • (monomial n) b = (monomial n) (a • b)

@[simp]

theorem SkewPolynomial.sum_monomial {R : Type u_1} [Semiring R] (f : SkewPolynomial R) : (f.sum fun (a : ℕ) => ⇑(monomial a)) = f

@[simp]

theorem SkewPolynomial.sum_monomial_index {R : Type u_1} [Semiring R] {N : Type u_5} [AddCommMonoid N] {n : ℕ} {b : R} {h : ℕ → R → N} (h_zero : h n 0 = 0) : ((monomial n) b).sum h = h n b

theorem SkewPolynomial.monomial_injective {R : Type u_1} (n : ℕ) [Semiring R] : Function.Injective ⇑(monomial n)

@[simp]

theorem SkewPolynomial.monomial_eq_zero_iff {R : Type u_1} (n : ℕ) [Semiring R] (t : R) : (monomial n) t = 0 ↔ t = 0

theorem SkewPolynomial.monomial_eq_monomial_iff {R : Type u_1} [Semiring R] {m n : ℕ} {a b : R} : (monomial m) a = (monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

@[reducible, inline]

abbrev SkewPolynomial.φ {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] : R →+* R

Ring homomorphism associated to the twist of the skew polynomial ring. The multiplication in a skew polynomial ring is given by xr = φ(r)x.

Equations

• SkewPolynomial.φ = MulSemiringAction.toRingHom (Multiplicative ℕ) R (Multiplicative.ofAdd 1)

theorem SkewPolynomial.φ_def {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] : φ = MulSemiringAction.toRingHom (Multiplicative ℕ) R (Multiplicative.ofAdd 1)

theorem SkewPolynomial.φ_iterate_apply {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (a : R) : (⇑φ)^[n] a = Multiplicative.ofAdd n • a

theorem SkewPolynomial.monomial_mul_monomial {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n m : ℕ) (r s : R) : (monomial n) r * (monomial m) s = (monomial (n + m)) (r * (⇑φ)^[n] s)

theorem SkewPolynomial.mul_def {R : Type u_1} [Semiring R] {f g : SkewPolynomial R} [MulSemiringAction (Multiplicative ℕ) R] : f * g = f.sum fun (a₁ : ℕ) (b₁ : R) => g.sum fun (a₂ : ℕ) (b₂ : R) => (monomial (a₁ + a₂)) (b₁ * (⇑φ)^[a₁] b₂)

noncomputable def SkewPolynomial.C {R : Type u_1} [Semiring R] : R →+ SkewPolynomial R

C a is the constant SkewPolynomial a. C is provided as an additive homomorphism.

Equations

• SkewPolynomial.C = SkewMonoidAlgebra.singleAddHom 1

@[simp]

theorem SkewPolynomial.monomial_zero_left {R : Type u_1} [Semiring R] ⦃a : R⦄ : (monomial 0) a = C a

theorem SkewPolynomial.C_0 {R : Type u_1} [Semiring R] : C 0 = 0

theorem SkewPolynomial.C_add {R : Type u_1} [Semiring R] {a b : R} : C (a + b) = C a + C b

theorem SkewPolynomial.C_1 {R : Type u_1} [Semiring R] : C 1 = 1

@[simp]

theorem SkewPolynomial.sum_C_index {R : Type u_1} [Semiring R] {a : R} {β : Type u_5} [AddCommMonoid β] {f : ℕ → R → β} (h : f 0 0 = 0) : (C a).sum f = f 0 a

noncomputable def SkewPolynomial.CRingHom {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] : R →+* SkewPolynomial R

CRingHom a is the constant SkewPolynomial a, as a ring homomorphism. This requires [MulSemiringAction (Multiplicative ℕ) R].

Equations

• SkewPolynomial.CRingHom = SkewMonoidAlgebra.singleOneRingHom

theorem SkewPolynomial.CRingHom_eq_C {R : Type u_1} [Semiring R] {a : R} [MulSemiringAction (Multiplicative ℕ) R] : CRingHom a = C a

theorem SkewPolynomial.C_mul {R : Type u_1} [Semiring R] {a b : R} [MulSemiringAction (Multiplicative ℕ) R] : C (a * b) = C a * C b

theorem SkewPolynomial.C_pow {R : Type u_1} {n : ℕ} [Semiring R] {a : R} [MulSemiringAction (Multiplicative ℕ) R] : C (a ^ n) = C a ^ n

theorem SkewPolynomial.C_eq_natCast {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) : C ↑n = ↑n

@[simp]

theorem SkewPolynomial.C_mul_monomial {R : Type u_1} {n : ℕ} [Semiring R] {a b : R} [MulSemiringAction (Multiplicative ℕ) R] : C a * (monomial n) b = (monomial n) (a * b)

@[simp]

theorem SkewPolynomial.monomial_mul_C {R : Type u_1} {n : ℕ} [Semiring R] {a b : R} [MulSemiringAction (Multiplicative ℕ) R] : (monomial n) a * C b = (monomial n) (a * (⇑φ)^[n] b)

noncomputable def SkewPolynomial.X {R : Type u_1} [Semiring R] : SkewPolynomial R

X is the SkewPolynomial variable (aka indeterminate).

Equations

• SkewPolynomial.X = (SkewPolynomial.monomial 1) 1

theorem SkewPolynomial.monomial_one_one_eq_X {R : Type u_1} [Semiring R] : (monomial 1) 1 = X

theorem SkewPolynomial.monomial_one_right_eq_X_pow {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) : (monomial n) 1 = X ^ n

theorem SkewPolynomial.X_mul {R : Type u_1} [Semiring R] {p : SkewPolynomial R} [MulSemiringAction (Multiplicative ℕ) R] : X * p = (p.sum fun (a : ℕ) (b : R) => (monomial a) (φ b)) * X

theorem SkewPolynomial.X_pow_mul {R : Type u_1} [Semiring R] {p : SkewPolynomial R} [MulSemiringAction (Multiplicative ℕ) R] {n : ℕ} : X ^ n * p = (p.sum fun (a : ℕ) (b : R) => (monomial a) ((⇑φ)^[n] b)) * X ^ n

@[simp]

theorem SkewPolynomial.monomial_mul_X {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (r : R) : (monomial n) r * X = (monomial (n + 1)) r

@[simp]

theorem SkewPolynomial.monomial_mul_X_pow {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (r : R) (k : ℕ) : (monomial n) r * X ^ k = (monomial (n + k)) r

@[simp]

theorem SkewPolynomial.X_mul_monomial {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (r : R) : X * (monomial n) r = (monomial (n + 1)) (φ r)

@[simp]

theorem SkewPolynomial.X_pow_mul_monomial {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (k n : ℕ) (r : R) : X ^ k * (monomial n) r = (monomial (n + k)) ((⇑φ)^[k] r)

theorem SkewPolynomial.coeff_monomial {R : Type u_1} {m n : ℕ} [Semiring R] {a : R} : ((monomial n) a).coeff m = if n = m then a else 0

@[simp]

theorem SkewPolynomial.coeff_zero {R : Type u_1} [Semiring R] (n : ℕ) : coeff 0 n = 0

@[simp]

theorem SkewPolynomial.coeff_one_zero {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] : coeff 1 0 = 1

theorem SkewPolynomial.coeff_one {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) : coeff 1 n = if 0 = n then 1 else 0

@[simp]

theorem SkewPolynomial.coeff_X_one {R : Type u_1} [Semiring R] : X.coeff 1 = 1

@[simp]

theorem SkewPolynomial.coeff_X_zero {R : Type u_1} [Semiring R] : X.coeff 0 = 0

@[simp]

theorem SkewPolynomial.coeff_monomial_succ {R : Type u_1} {n : ℕ} [Semiring R] {a : R} : ((monomial (n + 1)) a).coeff 0 = 0

theorem SkewPolynomial.coeff_X {R : Type u_1} {n : ℕ} [Semiring R] : X.coeff n = if 1 = n then 1 else 0

theorem SkewPolynomial.coeff_X_of_ne_one {R : Type u_1} [Semiring R] {n : ℕ} (hn : n ≠ 1) : X.coeff n = 0

theorem SkewPolynomial.coeff_C {R : Type u_1} {n : ℕ} [Semiring R] {a : R} : (C a).coeff n = if n = 0 then a else 0

@[simp]

theorem SkewPolynomial.coeff_C_zero {R : Type u_1} [Semiring R] {a : R} : (C a).coeff 0 = a

theorem SkewPolynomial.coeff_C_ne_zero {R : Type u_1} {n : ℕ} [Semiring R] {a : R} (h : n ≠ 0) : (C a).coeff n = 0

@[simp]

theorem SkewPolynomial.coeff_C_succ {R : Type u_1} [Semiring R] {r : R} {n : ℕ} : (C r).coeff (n + 1) = 0

@[simp]

theorem SkewPolynomial.coeff_natCast_ite {R : Type u_1} {m n : ℕ} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] : (↑m).coeff n = ↑(if n = 0 then m else 0)

@[simp]

theorem SkewPolynomial.coeff_ofNat_zero {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (a : ℕ) [a.AtLeastTwo] : (OfNat.ofNat a).coeff 0 = OfNat.ofNat a

@[simp]

theorem SkewPolynomial.coeff_ofNat_succ {R : Type u_1} [Semiring R] [MulSemiringAction (Multiplicative ℕ) R] (a n : ℕ) [h : a.AtLeastTwo] : (OfNat.ofNat a).coeff (n + 1) = 0

theorem SkewPolynomial.C_mul_X_pow_eq_monomial {R : Type u_1} [Semiring R] {a : R} [MulSemiringAction (Multiplicative ℕ) R] ⦃n : ℕ⦄ : C a * X ^ n = (monomial n) a

theorem SkewPolynomial.C_mul_X_eq_monomial {R : Type u_1} [Semiring R] {a : R} [MulSemiringAction (Multiplicative ℕ) R] : C a * X = (monomial 1) a

theorem SkewPolynomial.C_injective {R : Type u_1} [Semiring R] : Function.Injective ⇑C

@[simp]

theorem SkewPolynomial.C_inj {R : Type u_1} [Semiring R] {a b : R} : C a = C b ↔ a = b

@[simp]

theorem SkewPolynomial.C_eq_zero {R : Type u_1} [Semiring R] {a : R} : C a = 0 ↔ a = 0

theorem SkewPolynomial.Nontrivial.of_polynomial_ne {R : Type u_1} [Semiring R] {p q : SkewPolynomial R} [MulSemiringAction (Multiplicative ℕ) R] (h : p ≠ q) : Nontrivial R

theorem SkewPolynomial.ext_iff {R : Type u_1} [Semiring R] {p q : SkewPolynomial R} : p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

theorem SkewPolynomial.ext {R : Type u_1} [Semiring R] {p q : SkewPolynomial R} : (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q

theorem SkewPolynomial.addHom_ext' {R : Type u_1} [Semiring R] {M : Type u_5} [AddMonoid M] {f g : SkewPolynomial R →+ M} (h : ∀ (n : ℕ), f.comp (monomial n).toAddMonoidHom = g.comp (monomial n).toAddMonoidHom) : f = g

theorem SkewPolynomial.addHom_ext'_iff {R : Type u_1} [Semiring R] {M : Type u_5} [AddMonoid M] {f g : SkewPolynomial R →+ M} : f = g ↔ ∀ (n : ℕ), f.comp (monomial n).toAddMonoidHom = g.comp (monomial n).toAddMonoidHom

theorem SkewPolynomial.addHom_ext {R : Type u_1} [Semiring R] {M : Type u_5} [AddMonoid M] {f g : SkewPolynomial R →+ M} (h : ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)) : f = g

theorem SkewPolynomial.addHom_ext_iff {R : Type u_1} [Semiring R] {M : Type u_5} [AddMonoid M] {f g : SkewPolynomial R →+ M} : f = g ↔ ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)

theorem SkewPolynomial.linearMap_ext' {R : Type u_1} [Semiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] {f g : SkewPolynomial R →ₗ[R] M} (h : ∀ (n : ℕ), f ∘ₗ monomial n = g ∘ₗ monomial n) : f = g

theorem SkewPolynomial.linearMap_ext'_iff {R : Type u_1} [Semiring R] {M : Type u_5} [AddCommMonoid M] [Module R M] {f g : SkewPolynomial R →ₗ[R] M} : f = g ↔ ∀ (n : ℕ), f ∘ₗ monomial n = g ∘ₗ monomial n

theorem SkewPolynomial.eq_zero_of_eq_zero {R : Type u_1} [Semiring R] (h : 0 = 1) (p : SkewPolynomial R) : p = 0