Formalization Blueprint for “An Introduction to Algebraic Combinatorics” by Darij Grinberg

1.5 Polynomials

1.5.1 Definition

Definition 1.134
#

(a) An FPS \(a\in K\left[ \left[ x\right] \right] \) is said to be a polynomial if all but finitely many \(n\in \mathbb {N}\) satisfy \(\left[ x^{n}\right] a=0\) (that is, if all but finitely many coefficients of \(a\) are \(0\)).

(b) We let \(K\left[ x\right] \) be the set of all polynomials \(a\in K\left[ \left[ x\right] \right] \). This set \(K\left[ x\right] \) is a subring of \(K\left[ \left[ x\right] \right] \) (according to Theorem 1.148 below), and is called the univariate polynomial ring over \(K\).

Lemma 1.135

An FPS \(f\in K\left[\left[x\right]\right]\) is a polynomial if and only if there exists an \(N\in \mathbb {N}\) such that \(\left[x^{n}\right]f=0\) for all \(n\geq N\).

theorem FPS.isPolynomial_iff_exists_degree_bound {K : Type u_1} [CommRing K] (f : PowerSeries K) :
IsPolynomial f ∃ (N : ), nN, (PowerSeries.coeff n) f = 0
Proof

\(\Longrightarrow \): If the set of nonzero-coefficient indices is finite, it is bounded above by some \(N\), so all coefficients beyond \(N\) vanish.

\(\Longleftarrow \): If all coefficients beyond \(N\) vanish, then the set of nonzero-coefficient indices is contained in \(\{ 0,1,\ldots ,N-1\} \), which is finite.

Lemma 1.136

An FPS \(f\in K\left[\left[x\right]\right]\) is a polynomial (in the sense of Definition 1.134) if and only if \(f\) equals the image of some element of \(K[x]\) under the canonical embedding \(K[x]\hookrightarrow K\left[\left[x\right]\right]\).

Proof

\(\Longrightarrow \): Use the degree bound from Lemma 1.135 and truncation.

\(\Longleftarrow \): The image of any polynomial has finite support (Lemma 1.137).

Lemma 1.137

The image of any polynomial \(p\in K[X]\) under the canonical embedding \(K[X]\hookrightarrow K\left[\left[x\right]\right]\) is a polynomial in the FPS sense.

Proof

The set of indices with nonzero coefficients is contained in the support of \(p\), which is a finite set.

Converting between polynomial FPSs and polynomials

Definition 1.138
#

Let \(f\in K\left[\left[x\right]\right]\) be a polynomial FPS (in the sense of Definition 1.134). We define \(\operatorname {toPolynomial}(f)\in K[X]\) as the truncation of \(f\) at the degree bound given by Lemma 1.135.

noncomputable def FPS.toPolynomial {K : Type u_1} [CommRing K] (f : PowerSeries K) (hf : IsPolynomial f) :
Lemma 1.139

Let \(f\in K\left[\left[x\right]\right]\) be a polynomial FPS. Then the coercion of \(\operatorname {toPolynomial}(f)\) back into \(K\left[\left[x\right]\right]\) equals \(f\):

\[ \iota \bigl(\operatorname {toPolynomial}(f)\bigr) = f, \]

where \(\iota \colon K[X]\hookrightarrow K\left[\left[x\right]\right]\) is the canonical embedding.

theorem FPS.coe_toPolynomial {K : Type u_1} [CommRing K] (f : PowerSeries K) (hf : IsPolynomial f) :
(toPolynomial f hf) = f
Proof

By the degree bound, all coefficients of \(f\) beyond the bound are zero, so truncation and coercion recover every coefficient of \(f\).

Lemma 1.140

For any polynomial \(p\in K[X]\), we have \(\operatorname {toPolynomial}(\iota (p))=p\), where \(\iota \) is the canonical embedding.

theorem FPS.toPolynomial_coe {K : Type u_1} [CommRing K] (p : Polynomial K) :
toPolynomial p = p
Proof

By Lemma 1.139, both sides have the same image under \(\iota \), and \(\iota \) is injective.

1.5.2 Polynomials form a subring of power series

Lemma 1.141

The zero power series \(\underline{0}\) is a polynomial.

Proof

All coefficients of \(\underline{0}\) are \(0\), so the set of nonzero-coefficient indices is empty, hence finite.

Lemma 1.142

The unity \(\underline{1}\) is a polynomial.

Proof

The unity \(\underline{1}\) equals the image of \(1\in K[X]\) under the canonical embedding.

Lemma 1.143

The sum of two polynomial power series is a polynomial.

theorem FPS.isPolynomial_add {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hf : IsPolynomial f) (hg : IsPolynomial g) :
Proof

If \(f\) and \(g\) are polynomials, then the set of indices where \((f+g)\) has a nonzero coefficient is contained in the union of the corresponding sets for \(f\) and \(g\). A finite union of finite sets is finite.

Lemma 1.144

The negation of a polynomial power series is a polynomial.

theorem FPS.isPolynomial_neg {K : Type u_1} [CommRing K] {f : PowerSeries K} (hf : IsPolynomial f) :
Proof

Negation does not change which coefficients are nonzero.

Lemma 1.145

The difference of two polynomial power series is a polynomial.

theorem FPS.isPolynomial_sub {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hf : IsPolynomial f) (hg : IsPolynomial g) :
Proof

Write \(f-g=f+(-g)\) and apply Lemma 1.143 and Lemma 1.144.

Lemma 1.146

The product of two polynomial power series is a polynomial.

theorem FPS.isPolynomial_mul {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hf : IsPolynomial f) (hg : IsPolynomial g) :
Proof

Let \(a,b\in K\left[ x\right] \). Since \(a\) is a polynomial, there exists a finite subset \(I\) of \(\mathbb {N}\) such that \(\left[ x^{i}\right] a=0\) for all \(i\in \mathbb {N}\setminus I\). Similarly, there exists a finite subset \(J\) of \(\mathbb {N}\) such that \(\left[ x^{j}\right] b=0\) for all \(j\in \mathbb {N}\setminus J\).

Let \(S=\left\{ i+j\ \mid \ i\in I\text{ and }j\in J\right\} \). This set \(S\) is again finite (since \(I\) and \(J\) are finite), and we have

\[ \left[ x^{n}\right] \left( ab\right) =\sum _{i=0}^{n}\left[ x^{i}\right] a\cdot \left[ x^{n-i}\right] b=0\text{ for all }n\in \mathbb {N}\setminus S, \]

because for each \(i\in \left\{ 0,1,\ldots ,n\right\} \), letting \(j=n-i\), we cannot have both \(i\in I\) and \(j\in J\) (otherwise \(n=i+j\in S\), contradicting \(n\notin S\)), so at least one of \(\left[ x^{i}\right] a\) and \(\left[ x^{j}\right] b\) is \(0\), making each summand \(0\). Thus, all but finitely many \(n\in \mathbb {N}\) satisfy \(\left[ x^{n}\right] \left( ab\right) =0\), so \(ab\in K\left[ x\right] \).

Lemma 1.147

Scalar multiplication of a polynomial power series by an element of \(K\) is a polynomial.

theorem FPS.isPolynomial_smul {K : Type u_1} [CommRing K] {f : PowerSeries K} (c : K) (hf : IsPolynomial f) :
Proof

If \(\left[x^{n}\right]f=0\), then \(\left[x^{n}\right](cf)=c\cdot \left[x^{n}\right]f=0\). So the nonzero-coefficient set of \(cf\) is contained in that of \(f\), which is finite.

Theorem 1.148

The set \(K\left[ x\right] \) is a subring of \(K\left[ \left[ x\right] \right] \) (that is, it is closed under addition, subtraction and multiplication, and contains the zero \(\underline{0}\) and the unity \(\underline{1}\)) and is a \(K\)-submodule of \(K\left[ \left[ x\right] \right] \) (that is, it is closed under addition and scaling by elements of \(K\)).

Proof

Follows from the preceding lemmas: \(K[x]\) contains \(\underline{0}\) (Lemma 1.141) and \(\underline{1}\) (Lemma 1.142), is closed under addition (Lemma 1.143), multiplication (Lemma 1.146), and scalar multiplication (Lemma 1.147).

Lemma 1.149

The polynomial \(x\in K\left[\left[x\right]\right]\) is a polynomial.

Proof

The only nonzero coefficient of \(x\) is the coefficient of \(x^1\), which is \(1\). Thus the set of nonzero-coefficient indices is contained in \(\{ 1\} \), which is finite.

Lemma 1.150

For any \(c\in K\), the constant FPS \(\underline{c}\) is a polynomial.

Proof

The only possibly nonzero coefficient of \(\underline{c}\) is the coefficient of \(x^0\). Thus the set of nonzero-coefficient indices is contained in \(\{ 0\} \), which is finite.

1.5.3 Reminders on rings and \(K\)-algebras

Definition 1.151
#

The notion of a ring (also known as a noncommutative ring) is defined in the exact same way as we defined the notion of a commutative ring in Definition 1.42, except that the “Commutativity of multiplication” axiom is removed.

theorem FPS.ring_add_assoc {R : Type u_2} [Ring R] (a b c : R) :
a + (b + c) = a + b + c
theorem FPS.ring_add_comm {R : Type u_2} [Ring R] (a b : R) :
a + b = b + a
theorem FPS.ring_add_zero {R : Type u_2} [Ring R] (a : R) :
a + 0 = a
theorem FPS.ring_zero_add {R : Type u_2} [Ring R] (a : R) :
0 + a = a
theorem FPS.ring_add_neg {R : Type u_2} [Ring R] (a : R) :
a + -a = 0
theorem FPS.ring_mul_assoc {R : Type u_2} [Ring R] (a b c : R) :
a * (b * c) = a * b * c
theorem FPS.ring_left_distrib {R : Type u_2} [Ring R] (a b c : R) :
a * (b + c) = a * b + a * c
theorem FPS.ring_right_distrib {R : Type u_2} [Ring R] (a b c : R) :
(a + b) * c = a * c + b * c
theorem FPS.ring_mul_one {R : Type u_2} [Ring R] (a : R) :
a * 1 = a
theorem FPS.ring_one_mul {R : Type u_2} [Ring R] (a : R) :
1 * a = a
theorem FPS.ring_mul_zero {R : Type u_2} [Ring R] (a : R) :
a * 0 = 0
theorem FPS.ring_zero_mul {R : Type u_2} [Ring R] (a : R) :
0 * a = 0
Definition 1.152
#

A \(K\)-algebra is a set \(A\) equipped with four maps

\begin{align*} \oplus & :A\times A\rightarrow A,\\ \ominus & :A\times A\rightarrow A,\\ \odot & :A\times A\rightarrow A,\\ \rightharpoonup & :K\times A\rightarrow A \end{align*}

and two elements \(\overrightarrow {0}\in A\) and \(\overrightarrow {1}\in A\) satisfying the following properties:

  1. The set \(A\), equipped with the maps \(\oplus \), \(\ominus \) and \(\odot \) and the two elements \(\overrightarrow {0}\) and \(\overrightarrow {1}\), is a (noncommutative) ring.

  2. The set \(A\), equipped with the maps \(\oplus \), \(\ominus \) and \(\rightharpoonup \) and the element \(\overrightarrow {0}\), is a \(K\)-module.

  3. We have

    \begin{equation} \lambda \rightharpoonup \left( a\odot b\right) =\left( \lambda \rightharpoonup a\right) \odot b=a\odot \left( \lambda \rightharpoonup b\right) \label{eq.def.alg.Kalg.scaleinv}\end{equation}
    14

    for all \(\lambda \in K\) and \(a,b\in A\).

(Thus, in a nutshell, a \(K\)-algebra is a set \(A\) that is simultaneously a ring and a \(K\)-module, with the property that the ring \(A\) and the \(K\)-module \(A\) have the same addition, the same subtraction and the same zero, and satisfy the additional compatibility property (14).)

theorem FPS.kalg_add_comm {A : Type u_2} [Ring A] (a b : A) :
a + b = b + a
theorem FPS.kalg_add_assoc {A : Type u_2} [Ring A] (a b c : A) :
a + (b + c) = a + b + c
theorem FPS.kalg_add_zero {A : Type u_2} [Ring A] (a : A) :
a + 0 = a
theorem FPS.kalg_mul_assoc {A : Type u_2} [Ring A] (a b c : A) :
a * (b * c) = a * b * c
theorem FPS.kalg_left_distrib {A : Type u_2} [Ring A] (a b c : A) :
a * (b + c) = a * b + a * c
theorem FPS.kalg_right_distrib {A : Type u_2} [Ring A] (a b c : A) :
(a + b) * c = a * c + b * c
theorem FPS.kalg_mul_one {A : Type u_2} [Ring A] (a : A) :
a * 1 = a
theorem FPS.kalg_one_mul {A : Type u_2} [Ring A] (a : A) :
1 * a = a
theorem FPS.kalg_smul_assoc {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u v : K) (a : A) :
u v a = (u * v) a
theorem FPS.kalg_smul_add {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u : K) (a b : A) :
u (a + b) = u a + u b
theorem FPS.kalg_add_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u v : K) (a : A) :
(u + v) a = u a + v a
theorem FPS.kalg_one_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (a : A) :
1 a = a
theorem FPS.kalg_zero_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (a : A) :
0 a = 0
theorem FPS.kalg_smul_zero {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u : K) :
u 0 = 0
theorem FPS.kalg_smul_mul_assoc {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (c : K) (a b : A) :
c (a * b) = c a * b
theorem FPS.kalg_mul_smul_comm {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (c : K) (a b : A) :
c (a * b) = a * c b
theorem FPS.kalg_smul_mul_eq_mul_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (c : K) (a b : A) :
c a * b = a * c b

1.5.4 Evaluation aka substitution into polynomials

Definition 1.153
#

Let \(f\in K\left[ x\right] \) be a polynomial. Let \(A\) be any \(K\)-algebra. Let \(a\in A\) be any element. We then define an element \(f\left[ a\right] \in A\) as follows:

Write \(f\) in the form \(f=\sum _{n\in \mathbb {N}}f_{n}x^{n}\) with \(f_{0},f_{1},f_{2},\ldots \in K\). (That is, \(f_{n}=\left[ x^{n}\right] f\) for each \(n\in \mathbb {N}\).) Then, set

\[ f\left[ a\right] :=\sum _{n\in \mathbb {N}}f_{n}a^{n}. \]

(This sum is essentially finite, since \(f\) is a polynomial.)

The element \(f\left[ a\right] \) is also denoted by \(f\circ a\) or by \(f\left( a\right) \), and is called the value of \(f\) at \(a\) (or the evaluation of \(f\) at \(a\), or the result of substituting \(a\) for \(x\) in \(f\)).

abbrev FPS.polyEval {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) :
A
Lemma 1.154

The evaluation \(f\left[a\right]\) can be computed as \(f\left[a\right]=\sum _{n}f_{n}\cdot a^{n}\), where the sum ranges over all \(n\) in the support of \(f\).

theorem FPS.eval_def {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) :
polyEval f a = f.sum fun (n : ) (c : K) => (algebraMap K A) c * a ^ n
Proof

Immediate from the definitions.

Lemma 1.155

The evaluation \(f\left[a\right]\) equals \(\sum _{n\in \operatorname {supp}(f)}f_{n}\cdot a^{n}\), making the finiteness of the sum explicit.

theorem FPS.eval_eq_finsum {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) :
polyEval f a = nf.support, (algebraMap K A) (f.coeff n) * a ^ n
Proof

This follows from the definition by restricting the sum to the support.

Lemma 1.156

The evaluation \(f\left[a\right]\) equals \(\sum _{n=0}^{\deg f}f_{n}\cdot a^{n}\), where the sum is taken up to the degree of \(f\).

theorem FPS.eval_eq_sum_range {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) :
polyEval f a = nFinset.range (f.natDegree + 1), (algebraMap K A) (f.coeff n) * a ^ n
Proof

Since all coefficients beyond the degree of \(f\) are zero, extending or restricting the sum to this range does not change the result.

Theorem 1.157

Let \(A\) be a \(K\)-algebra. Let \(a\in A\). Then:

(a) Any \(f,g\in K\left[ x\right] \) satisfy

\[ \left( f+g\right) \left[ a\right] =f\left[ a\right] +g\left[ a\right] \ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \left( fg\right) \left[ a\right] =f\left[ a\right] \cdot g\left[ a\right] . \]

(b) Any \(\lambda \in K\) and \(f\in K\left[ x\right] \) satisfy

\[ \left( \lambda f\right) \left[ a\right] =\lambda \cdot f\left[ a\right] . \]

(c) Any \(\lambda \in K\) satisfies \(\underline{\lambda }\left[ a\right] =\lambda \cdot 1_{A}\), where \(1_{A}\) is the unity of the ring \(A\).

(d) We have \(x\left[ a\right] =a\).

(e) We have \(x^{i}\left[ a\right] =a^{i}\) for each \(i\in \mathbb {N}\).

(f) Any \(f,g\in K\left[ x\right] \) satisfy \(f\left[ g\left[ a\right] \right] =\left( f\left[ g\right] \right) \left[ a\right] \).

theorem FPS.eval_add' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f g : Polynomial K) (a : A) :
polyEval (f + g) a = polyEval f a + polyEval g a
theorem FPS.eval_mul' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f g : Polynomial K) (a : A) :
polyEval (f * g) a = polyEval f a * polyEval g a
theorem FPS.eval_smul' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (c : K) (a : A) :
polyEval (c f) a = c polyEval f a
theorem FPS.eval_C' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (c : K) (a : A) :
theorem FPS.eval_X' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (a : A) :
theorem FPS.eval_X_pow' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (a : A) (i : ) :
theorem FPS.eval_comp' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f g : Polynomial K) (a : A) :
polyEval f (polyEval g a) = polyEval (f.comp g) a
Proof

See [ 19s , Theorem 7.6.3 ] for parts (a), (b), (c), (d) and (e). Part (f) is [ 19s , Proposition 7.6.14 ] .

1.5.5 Special evaluation results

Lemma 1.158

For any polynomial \(f\in K[x]\), we have \(f[x]=f\).

Proof

The evaluation map at \(x\) is the identity on \(K[x]\).

Lemma 1.159

For any polynomial \(f\in K[x]\) and any \(K\)-algebra \(A\), we have \(f[0]=\left[x^{0}\right]f\) (the constant term of \(f\), coerced into \(A\)).

theorem FPS.eval_zero_eq_coeff_zero {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) :
polyEval f 0 = (algebraMap K A) (f.coeff 0)
Proof

Setting \(a=0\): all terms \(f_{n}\cdot 0^{n}\) for \(n\geq 1\) vanish, leaving only \(f_{0}\cdot 0^{0}=f_{0}\cdot 1=f_{0}\).

Lemma 1.160

For any polynomial \(f\in K[x]\) and any \(K\)-algebra \(A\), we have \(f[1]=\left[x^{0}\right]f+\left[x^{1}\right]f+\left[x^{2}\right]f+\cdots \) (the sum of all coefficients of \(f\), coerced into \(A\)).

theorem FPS.eval_one_eq_sum_coeffs {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) :
polyEval f 1 = (algebraMap K A) (f.sum fun (x : ) (c : K) => c)
Proof

Setting \(a=1\): each term \(f_{n}\cdot 1^{n}=f_{n}\), so \(f[1]=\sum _{n}f_{n}\).