|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Xavier Généreux. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Xavier Généreux, María Inés de Frutos Fernández |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Algebra.Defs |
| 7 | +import Mathlib.Algebra.SkewMonoidAlgebra.Basic |
| 8 | +/-! |
| 9 | +# Univariate skew polynomials |
| 10 | +
|
| 11 | +Given a ring `R` and an endomorphism `φ` on `R` the skew polynomials over `R` |
| 12 | +are polynomials |
| 13 | +$$\sum_{i= 0}^n a_iX^n, n\geq 0, a_i\in R$$ |
| 14 | +where the addition is the usual addition of polynomials |
| 15 | +$$\sum_{i= 0}^n a_iX^n + \sum_{i= 0}^n b_iX^n= \sum_{i= 0}^n (a_i + b_i)X^n.$$ |
| 16 | +The multiplication, however, is determined by |
| 17 | +$$Xa = \varphi (a)X$$ |
| 18 | +by extending it to all polynomials in the obvious way. |
| 19 | +
|
| 20 | +Skew polynomials are represented as `SkewMonoidAlgebra R (Multiplicative ℕ)`, |
| 21 | +where `R` is usually at least a Semiring. In this file, we define `SkewPolynomial` |
| 22 | +and provide basic instances. |
| 23 | +
|
| 24 | +**Note**: To register the endomorphism `φ` see notation below. |
| 25 | +
|
| 26 | +## Notation |
| 27 | +
|
| 28 | +The endomorphism `φ` is implemented using some action of `Multiplicative ℕ` on `R`. |
| 29 | +From this action, `φ` is an `abbrev` denoting $(\text{ofAdd } 1) \cdot a := \varphi(a)$. |
| 30 | +
|
| 31 | +Users that want to work with a specific map `φ` should introduce an an action of |
| 32 | +`Multiplicative ℕ` on `R`. Specifying that this action is a `MulSemiringAction` amounts |
| 33 | +to saying that `φ` is an endomorphism. |
| 34 | +
|
| 35 | +Furthermore, with this notation `φ^[n](a) = (ofAdd n) • a`, see `φ_iterate_apply`. |
| 36 | +
|
| 37 | +## Implementation notes |
| 38 | +
|
| 39 | +The implementation uses `Muliplicative ℕ` instead of `ℕ` as some notion |
| 40 | +of `AddSkewMonoidAlgebra` like the current implementation of `Polynomials` in Mathlib. |
| 41 | +
|
| 42 | +This decision was made because we use the type class `MulSemiringAction` to specify the properties |
| 43 | +the action needs to respect for associativity. There is no version of this in Mathlib that |
| 44 | +uses an acting `AddMonoid M` and so we need to use `Multiplicative ℕ` for the action. |
| 45 | +
|
| 46 | +For associativity to hold, there should be an instance of |
| 47 | +`MulSemiringAction (Multiplicative ℕ) R` present in the context. |
| 48 | +For example, in the context of $\mathbb{F}_q$-linear polynomials, this can be the |
| 49 | +$q$-th Frobenius endomorphism - so $\varphi(a) = a^q$. |
| 50 | +
|
| 51 | +## Reference |
| 52 | +
|
| 53 | +The definition is inspired by Chapter 3 of [Papikian2023]. |
| 54 | +
|
| 55 | +## Tags |
| 56 | +
|
| 57 | +Skew Polynomials, Twisted Polynomials. |
| 58 | +
|
| 59 | +## TODO : |
| 60 | + - Add algebra instance |
| 61 | + - Add `ext` lemma in terms of `Coeff`. |
| 62 | +
|
| 63 | +Note that [ore33] proposes a more general definition of skew polynomial ring, where the |
| 64 | +multiplication is determined by $Xa = \varphi (a)X + δ (a)$, where `ϕ` is as above and |
| 65 | +`δ` is a derivation. |
| 66 | +
|
| 67 | +-/ |
| 68 | + |
| 69 | +noncomputable section |
| 70 | + |
| 71 | +open Multiplicative SkewMonoidAlgebra |
| 72 | + |
| 73 | +/-- The skew polynomials over `R` is the type of univariate polynomials over `R` |
| 74 | +endowed with a skewed convolution product. -/ |
| 75 | +def SkewPolynomial (R : Type*) [AddCommMonoid R] := SkewMonoidAlgebra R (Multiplicative ℕ) |
| 76 | + |
| 77 | +namespace SkewPolynomial |
| 78 | +variable {R : Type*} |
| 79 | + |
| 80 | +section Semiring |
| 81 | +variable [Semiring R] {p q : SkewPolynomial R} |
| 82 | + |
| 83 | +instance : Inhabited (SkewPolynomial R) := SkewMonoidAlgebra.instInhabited |
| 84 | + |
| 85 | +instance : AddCommMonoid (SkewPolynomial R) := SkewMonoidAlgebra.instAddCommMonoid |
| 86 | + |
| 87 | +instance instSemiring [MulSemiringAction (Multiplicative ℕ) R] : Semiring (SkewPolynomial R) := |
| 88 | + SkewMonoidAlgebra.instSemiring |
| 89 | + |
| 90 | +variable {S S₁ S₂ : Type*} |
| 91 | + |
| 92 | +instance [Semiring S] [Module S R] : Module S (SkewPolynomial R) := |
| 93 | + SkewMonoidAlgebra.instModule |
| 94 | + |
| 95 | +instance [Semiring S₁] [Semiring S₂] [Module S₁ R] [Module S₂ R] |
| 96 | + [SMulCommClass S₁ S₂ R] : SMulCommClass S₁ S₂ (SkewPolynomial R) := |
| 97 | + SkewMonoidAlgebra.instSMulCommClass |
| 98 | + |
| 99 | +instance [SMulZeroClass S R] : SMulZeroClass S (SkewPolynomial R) := |
| 100 | + SkewMonoidAlgebra.instSMulZeroClass |
| 101 | + |
| 102 | +instance [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] |
| 103 | + [IsScalarTower S₁ S₂ R] : IsScalarTower S₁ S₂ (SkewPolynomial R) := |
| 104 | + SkewMonoidAlgebra.instIsScalarTower |
| 105 | + |
| 106 | +instance [Subsingleton R] : Unique (SkewPolynomial R) := |
| 107 | + SkewMonoidAlgebra.instUniqueOfSubsingleton |
| 108 | + |
| 109 | +/-- |
| 110 | +The set of all `n` such that `X^n` has a non-zero coefficient. |
| 111 | +-/ |
| 112 | +def support (p : SkewPolynomial R) : Finset ℕ := |
| 113 | + Finset.map ⟨toAdd, toAdd.injective⟩ (SkewMonoidAlgebra.support p) |
| 114 | + |
| 115 | +@[simp] lemma support_zero : (0 : SkewPolynomial R).support = ∅ := rfl |
| 116 | + |
| 117 | +@[simp] lemma support_eq_empty : p.support = ∅ ↔ p = 0 := by simp [support] |
| 118 | + |
| 119 | +lemma card_support_eq_zero : p.support.card = 0 ↔ p = 0 := by simp |
| 120 | + |
| 121 | +lemma support_add : (p + q).support ⊆ p.support ∪ q.support := by |
| 122 | + simpa [support, ← Finset.map_union, Finset.map_subset_map] using SkewMonoidAlgebra.support_add |
| 123 | + |
| 124 | +section phi |
| 125 | + |
| 126 | +variable [MulSemiringAction (Multiplicative ℕ) R] |
| 127 | + |
| 128 | +/-- Ring homomorphism associated to the twist of the skew polynomial ring. |
| 129 | +The multiplication in a skew polynomial ring is given by `xr = φ(r)x`. -/ |
| 130 | +abbrev φ := MulSemiringAction.toRingHom (Multiplicative ℕ) R (ofAdd 1) |
| 131 | + |
| 132 | +theorem φ_def : φ = MulSemiringAction.toRingHom (Multiplicative ℕ) R (ofAdd 1) := rfl |
| 133 | + |
| 134 | +lemma φ_iterate_apply (n : ℕ) (a : R) : (φ^[n] a) = ((ofAdd n) • a) := by |
| 135 | + induction n with |
| 136 | + | zero => simp |
| 137 | + | succ n hn => |
| 138 | + simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ, |
| 139 | + ← mul_smul, mul_comm] |
| 140 | + |
| 141 | +end phi |
| 142 | + |
| 143 | +/-- `monomial s a` is the monomial `a * X^s` -/ |
| 144 | +def monomial (n : ℕ) : R →ₗ[R] SkewPolynomial R := lsingle (ofAdd n) |
| 145 | + |
| 146 | +lemma monomial_zero_right (n : ℕ) : monomial n (0 : R) = 0 := single_zero _ |
| 147 | + |
| 148 | +lemma monomial_zero_one [MulSemiringAction (Multiplicative ℕ) R] : |
| 149 | + monomial (0 : ℕ) (1 : R) = 1 := by rfl |
| 150 | + |
| 151 | +lemma monomial_def (n : ℕ) (a : R) : monomial n a = single (ofAdd n) a := rfl |
| 152 | + |
| 153 | +lemma monomial_add (n : ℕ) (r s : R) : |
| 154 | + monomial n (r + s) = monomial n r + monomial n s := |
| 155 | + single_add .. |
| 156 | + |
| 157 | +lemma smul_monomial {S} [Semiring S] [Module S R] (a : S) (n : ℕ) (b : R) : |
| 158 | + a • monomial n b = monomial n (a • b) := |
| 159 | + smul_single .. |
| 160 | + |
| 161 | +lemma monomial_mul_monomial [MulSemiringAction (Multiplicative ℕ) R] (n m : ℕ) (r s : R) : |
| 162 | + monomial n r * monomial m s = monomial (n + m) (r * (φ^[n] s)) := by |
| 163 | + rw [φ_iterate_apply] |
| 164 | + exact SkewMonoidAlgebra.single_mul_single |
| 165 | + |
| 166 | +end Semiring |
| 167 | + |
| 168 | +end SkewPolynomial |
0 commit comments