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

A.1 Details: Infinite products (part 1)

Fix a commutative ring \(K\).

A.1.1 Essentially finite families

Definition A.1
#

A family \((k_i)_{i \in I}\) of natural numbers is essentially finite if all but finitely many entries equal \(0\), i.e., the set \(\{ i \in I : k_i \neq 0\} \) is finite. This corresponds to \(S^I_{\mathrm{fin}}\) in the source.

Definition A.2
#

For a family \((p_{i,k})\) of FPSs, the coefficient support set \(T_m\) at degree \(m\) is the set \(\{ (i,k) : k \neq 0 \text{ and } [x^m] p_{i,k} \neq 0\} \).

def PowerSeries.CoeffSupportSet {K : Type u_1} [CommRing K] {I : Type u_2} (p : IPowerSeries K) (m : ) :
Set (I × )
Definition A.3
#

The coefficient support union \(T'_n = T_0 \cup T_1 \cup \cdots \cup T_n\) is the union of coefficient support sets up to degree \(n\).

Definition A.4
#

The index set \(I_n\) is the set of first components appearing in \(T'_n\): \(I_n = \{ i \in I : \exists k,\; (i,k) \in T'_n\} \).

def PowerSeries.IndexSetIn {K : Type u_1} [CommRing K] {I : Type u_2} (p : IPowerSeries K) (n : ) :
Set I
Definition A.5
#

The value set \(K_n\) is the set of second components appearing in \(T'_n\): \(K_n = \{ k \in \mathbb {N} : \exists i,\; (i,k) \in T'_n\} \).

def PowerSeries.ValueSetKn {K : Type u_1} [CommRing K] {I : Type u_2} (p : IPowerSeries K) (n : ) :
Definition A.6
#

The set \(S^I_{\mathrm{fin}}\) of essentially finite families in \(\prod _{i \in I} S_i\) is the set of all families \((k_i)_{i \in I}\) such that \(k_i \in S_i\) for all \(i\) and the family \((k_i)\) is essentially finite.

def PowerSeries.SfinI {I : Type u_2} (S : ISet ) :
Set (I)
Definition A.7
#

Given a finite subset \(I_n \subseteq I\) and a function \(f : I_n \to \mathbb {N}\), extend from finset produces a function \(I \to \mathbb {N}\) by setting \(f(i)\) for \(i \in I_n\) and \(0\) otherwise. This is used in the bijection between essentially finite families supported on \(I_n\) and functions \(I_n \to S\).

def PowerSeries.extendFromFinset {I : Type u_2} [DecidableEq I] (In : Finset I) (f : In) :
I
Definition A.8
#

Given a finite subset \(I_n \subseteq I\) and a function \(k : I \to \mathbb {N}\), restrict to finset produces the restriction \(k|_{I_n} : I_n \to \mathbb {N}\). This is the inverse direction of the bijection used in Claim 8.

def PowerSeries.restrictToFinset {I : Type u_2} (In : Finset I) (k : I) (i : In) :

A.1.2 Existence of approximators

Lemma A.9
#

For a multipliable family \((\mathbf{a}_i)_{i \in I}\) and any \(n \in \mathbb {N}\), there exists an \(x^n\)-approximator \(M\) for \((\mathbf{a}_i)_{i \in I}\). The proof takes the union of finite sets \(M_0, M_1, \ldots , M_n\) where each \(M_k\) determines the \(x^k\)-coefficient.

theorem PowerSeries.exists_xn_approximator {R : Type u_1} [CommRing R] {I : Type u_2} [DecidableEq I] (a : IPowerSeries R) (ha : Multipliable a) (n : ) :
∃ (M : Finset I), IsXnApproximator a M n

A.1.3 Multipliability criteria

Theorem A.10
#

If \((f_i)_{i \in I}\) is a family of FPSs such that for each \(n\), the set \(\{ i \in I : [x^n] f_i \neq 0\} \) is finite (i.e., the family is coefficient-wise summable), then the family \((1 + f_i)_{i \in I}\) is multipliable.

The proof constructs an approximator \(M\) as the union of the finite sets \(\{ i : [x^m] f_i \neq 0\} \) for \(m = 0, 1, \ldots , n\), and shows that multiplying by \((1 + f_i)\) for \(i \notin M\) does not change coefficients up to degree \(n\).

theorem PowerSeries.multipliable_one_add_of_summable {R : Type u_1} [CommRing R] {I : Type u_2} {f : IPowerSeries R} (hf : ∀ (n : ), {i : I | (coeff n) (f i) 0}.Finite) :
Multipliable fun (i : I) => 1 + f i
Theorem A.11
#

If \((a_i)_{i \in I}\) is a family of FPSs such that \(\{ i \in I : a_i \neq 1\} \) is finite, then the family is multipliable. The finite support set itself serves as a determining set for every coefficient.

theorem PowerSeries.multipliable_of_finite_ne_one {R : Type u_1} [CommRing R] {I : Type u_2} (a : IPowerSeries R) (h : {i : I | a i 1}.Finite) :
Theorem A.12
#

If \(J \subseteq I\) and both the subfamily \((a_i)_{i \in J}\) and the subfamily \((a_i)_{i \in I \setminus J}\) are multipliable, then the full family \((a_i)_{i \in I}\) is multipliable. The proof combines \(x^n\)-approximators for the two subfamilies.

theorem PowerSeries.multipliable_of_union {R : Type u_1} [CommRing R] {I : Type u_2} {a : IPowerSeries R} {J : Set I} (hJ : Multipliable fun (i : J) => a i) (hIJ : Multipliable fun (i : ↑(Set.univ \ J)) => a i) :

A.1.4 Multipliable product and division rules (Lean formalization)

Theorem A.13
#

If \((\mathbf{a}_i)_{i \in I}\) and \((\mathbf{b}_i)_{i \in I}\) are both multipliable, then the pointwise product family \((\mathbf{a}_i \cdot \mathbf{b}_i)_{i \in I}\) is multipliable. The proof takes \(M = U \cup V\) where \(U\) and \(V\) are \(x^n\)-approximators for the two families.

theorem PowerSeries.multipliable_mul {R : Type u_1} [CommRing R] {I : Type u_2} {a b : IPowerSeries R} (ha : Multipliable a) (hb : Multipliable b) :
Multipliable fun (i : I) => a i * b i
Theorem A.14
#

Under the hypotheses of Theorem A.13, the infinite product of the pointwise product equals the product of the two infinite products:

\[ \prod _{i \in I} (\mathbf{a}_i \cdot \mathbf{b}_i) = \Bigl(\prod _{i \in I} \mathbf{a}_i\Bigr) \cdot \Bigl(\prod _{i \in I} \mathbf{b}_i\Bigr). \]
theorem PowerSeries.tprod_mul_eq_mul_tprod {R : Type u_1} [CommRing R] {I : Type u_2} {a b : IPowerSeries R} (ha : Multipliable a) (hb : Multipliable b) (hab : Multipliable fun (i : I) => a i * b i := ) :
tprod (fun (i : I) => a i * b i) hab = tprod a ha * tprod b hb
Theorem A.15
#

If \((\mathbf{a}_i)_{i \in I}\) and \((\mathbf{b}_i)_{i \in I}\) are multipliable and each \(\mathbf{b}_i\) has invertible constant term, then the family \((\mathbf{a}_i \cdot \mathbf{b}_i^{-1})_{i \in I}\) is multipliable.

theorem PowerSeries.multipliable_div {R : Type u_1} [CommRing R] {I : Type u_2} {a b : IPowerSeries R} (ha : Multipliable a) (hb : Multipliable b) (hb_inv : ∀ (i : I), IsUnit ((coeff 0) (b i))) :
Multipliable fun (i : I) => a i * Ring.inverse (b i)
Theorem A.16
#

Under the hypotheses of Theorem A.15,

\[ \prod _{i \in I} \frac{\mathbf{a}_i}{\mathbf{b}_i} = \frac{\prod _{i \in I} \mathbf{a}_i}{\prod _{i \in I} \mathbf{b}_i}. \]
theorem PowerSeries.tprod_div_eq_div_tprod {R : Type u_1} [CommRing R] {I : Type u_2} {a b : IPowerSeries R} (ha : Multipliable a) (hb : Multipliable b) (hb_inv : ∀ (i : I), IsUnit ((coeff 0) (b i))) (hab : Multipliable fun (i : I) => a i * Ring.inverse (b i) := ) :
tprod (fun (i : I) => a i * Ring.inverse (b i)) hab = tprod a ha * Ring.inverse (tprod b hb)

A.1.5 Subfamily and reindexing lemmas

Lemma A.17
#

If \(U\) is an \(x^n\)-approximator for a family \((\mathbf{a}_i)_{i \in I}\) of invertible FPSs and \(J \subseteq I\), then \(U \cap J\) (as a preimage under the subtype embedding) is an \(x^n\)-approximator for the subfamily \((\mathbf{a}_i)_{i \in J}\). This is the Lean formalization of Lemma 1.368, using the invertibility hypothesis to cancel factors outside \(J\).

theorem PowerSeries.isXnApproximator_inter_subfamily {R : Type u_1} [CommRing R] {I : Type u_2} {a : IPowerSeries R} {U : Finset I} {n : } (hU : IsXnApproximator a U n) (ha_inv : ∀ (i : I), IsUnit ((coeff 0) (a i))) (J : Set I) :
IsXnApproximator (fun (i : J) => a i) (U.preimage Subtype.val ) n
Theorem A.18
#

If \((\mathbf{a}_i)_{i \in I}\) is multipliable and each \(\mathbf{a}_i\) has invertible constant term, then for any \(J \subseteq I\), the subfamily \((\mathbf{a}_i)_{i \in J}\) is multipliable.

theorem PowerSeries.multipliable_subfamily {R : Type u_1} [CommRing R] {I : Type u_2} {a : IPowerSeries R} (ha : Multipliable a) (ha_inv : ∀ (i : I), IsUnit ((coeff 0) (a i))) (J : Set I) :
Multipliable fun (i : J) => a i
Theorem A.19
#

If \(f : S \to T\) is a bijection and \((\mathbf{a}_t)_{t \in T}\) is multipliable, then \((\mathbf{a}_{f(s)})_{s \in S}\) is multipliable.

theorem PowerSeries.multipliable_reindex {R : Type u_1} [CommRing R] {S : Type u_3} {T : Type u_4} {f : ST} (hf : Function.Bijective f) {a : TPowerSeries R} (ha : Multipliable a) :
Theorem A.20
#

Under the hypotheses of Theorem A.19, the reindexed infinite product equals the original: \(\prod _{s \in S} \mathbf{a}_{f(s)} = \prod _{t \in T} \mathbf{a}_t\).

theorem PowerSeries.tprod_reindex {R : Type u_1} [CommRing R] {S : Type u_3} {T : Type u_4} {f : ST} (hf : Function.Bijective f) {a : TPowerSeries R} (ha : Multipliable a) (haf : Multipliable (a f) := ) :
tprod (a f) haf = tprod a ha

A.1.6 Fiber product decomposition

Theorem A.21
#

Let \(f : S \to W\) be a map, and \((\mathbf{a}_s)_{s \in S}\) a multipliable family. Suppose that for each \(w \in W\), the fiber subfamily \((\mathbf{a}_s)_{s \in f^{-1}(w)}\) is multipliable. Then the family of fiber products \(\bigl(\prod _{s \in f^{-1}(w)} \mathbf{a}_s\bigr)_{w \in W}\) is multipliable. The proof uses \(f(U)\) (the image of an \(x^n\)-approximator \(U\)) as the approximator for the outer product.

theorem PowerSeries.multipliable_prod_fibers {R : Type u_1} [CommRing R] {S : Type u_3} {W : Type u_4} {f : SW} {a : SPowerSeries R} (ha : Multipliable a) (ha_fibers : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a s) :
Multipliable fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a s)
Theorem A.22
#

Under the hypotheses of Theorem A.21,

\[ \prod _{s \in S} \mathbf{a}_s = \prod _{w \in W} \Bigl(\prod _{s \in f^{-1}(w)} \mathbf{a}_s\Bigr). \]

This is the Lean formalization of Proposition 1.372 (parts (a) and (b)).

theorem PowerSeries.tprod_eq_tprod_fibers {R : Type u_1} [CommRing R] {S : Type u_3} {W : Type u_4} {f : SW} {a : SPowerSeries R} (ha : Multipliable a) (ha_fibers : ∀ (w : W), Multipliable fun (s : { s : S // f s = w }) => a s) (ha_outer : Multipliable fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a s) := ) :
tprod a ha = tprod (fun (w : W) => tprod (fun (s : { s : S // f s = w }) => a s) ) ha_outer

A.1.7 Fubini rules for infinite products

Theorem A.23
#

Let \((\mathbf{a}_{(i,j)})_{(i,j) \in I \times J}\) be a multipliable family. Suppose that for each \(i \in I\), the row family \((\mathbf{a}_{(i,j)})_{j \in J}\) is multipliable. Then the family of row products \(\bigl(\prod _{j \in J} \mathbf{a}_{(i,j)}\bigr)_{i \in I}\) is multipliable.

theorem PowerSeries.multipliable_tprod_fubini {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × JPowerSeries R} (ha : Multipliable a) (ha_I : ∀ (i : I), Multipliable fun (j : J) => a (i, j)) :
Multipliable fun (i : I) => tprod (fun (j : J) => a (i, j))
Theorem A.24
#

Under the hypotheses of Theorem A.23,

\[ \prod _{(i,j) \in I \times J} \mathbf{a}_{(i,j)} = \prod _{i \in I} \Bigl(\prod _{j \in J} \mathbf{a}_{(i,j)}\Bigr). \]

This is the Fubini rule for infinite products of FPSs.

theorem PowerSeries.tprod_fubini {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × JPowerSeries R} (ha : Multipliable a) (ha_I : ∀ (i : I), Multipliable fun (j : J) => a (i, j)) (_ha_J : ∀ (j : J), Multipliable fun (i : I) => a (i, j)) (ha_outer_I : Multipliable fun (i : I) => tprod (fun (j : J) => a (i, j)) := ) :
tprod a ha = tprod (fun (i : I) => tprod (fun (j : J) => a (i, j)) ) ha_outer_I
Theorem A.25
#

If \((\mathbf{a}_{(i,j)})_{(i,j) \in I \times J}\) is a multipliable family of invertible FPSs (each has unit constant term), then both the row families \((\mathbf{a}_{(i,j)})_{j \in J}\) for each \(i\) and the column families \((\mathbf{a}_{(i,j)})_{i \in I}\) for each \(j\) are multipliable. No additional multipliability hypotheses are needed in the invertible case, because subfamilies of invertible multipliable families are automatically multipliable.

theorem PowerSeries.fubini_prod_invertible {R : Type u_1} [CommRing R] {I : Type u_3} {J : Type u_4} {a : I × JPowerSeries R} (ha : Multipliable a) (ha_inv : ∀ (p : I × J), IsUnit ((coeff 0) (a p))) :
(∀ (i : I), Multipliable fun (j : J) => a (i, j)) ∀ (j : J), Multipliable fun (i : I) => a (i, j)

A.1.8 Coefficient form of the generalized distributive law

Lemma A.26
#

For any finite set \(M \subseteq I\) and finite value sets \((S_i)_{i \in M}\),

\[ [x^n]\Bigl(\prod _{i \in M} \sum _{k \in S_i} p_{i,k}\Bigr) = [x^n]\Bigl(\sum _{(k_i) \in \prod _{i \in M} S_i} \prod _{i \in M} p_{i,k_i}\Bigr). \]

This is a direct corollary of Claim 11 (finite product-sum interchange).

theorem PowerSeries.prodRule_infInf_coeff {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : IPowerSeries K) (n : ) (M : Finset I) (Sfin : IFinset ) :
(coeff n) (∏ iM, kSfin i, p i k) = (coeff n) (∑ fFintype.piFinset fun (i : M) => Sfin i, i : M, p (↑i) (f i))

A.1.9 Congruence lemma for division

Lemma A.27

Let \(a, b, c, d \in K\left[\left[x\right]\right]\) be four FPSs such that \(c\) and \(d\) are invertible. Let \(n \in \mathbb {N}\). Assume that

\[ \left[x^{m}\right] a = \left[x^{m}\right] b \qquad \text{for each } m \in \left\{ 0, 1, \ldots , n\right\} . \]

Assume further that

\[ \left[x^{m}\right] c = \left[x^{m}\right] d \qquad \text{for each } m \in \left\{ 0, 1, \ldots , n\right\} . \]

Then,

\[ \left[x^{m}\right] \frac{a}{c} = \left[x^{m}\right] \frac{b}{d} \qquad \text{for each } m \in \left\{ 0, 1, \ldots , n\right\} . \]
theorem AlgebraicCombinatorics.FPS.xnEquiv_div {K : Type u_1} [CommRing K] {n : } {a b c d : PowerSeries K} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (hc : IsUnit (PowerSeries.constantCoeff c)) (hd : IsUnit (PowerSeries.constantCoeff d)) :
Proof

We have assumed that

\[ \left[x^{m}\right] a = \left[x^{m}\right] b \qquad \text{for each } m \in \left\{ 0, 1, \ldots , n\right\} . \]

In other words, \(a \overset {x^n}{\equiv } b\) (by the definition of the relation \(\overset {x^n}{\equiv }\)). Similarly, \(c \overset {x^n}{\equiv } d\). Hence, by the compatibility of \(\overset {x^n}{\equiv }\) with division (Theorem 1.328 (e)), we obtain \(\frac{a}{c} \overset {x^n}{\equiv } \frac{b}{d}\). In other words,

\[ \left[x^{m}\right] \frac{a}{c} = \left[x^{m}\right] \frac{b}{d} \qquad \text{for each } m \in \left\{ 0, 1, \ldots , n\right\} \]

(by the definition of the relation \(\overset {x^n}{\equiv }\)). This proves Lemma A.27.

A.1.10 Detailed proof of Proposition 1.367

Detailed proof of Proposition 1.367

This can be proved similarly to Proposition 1.366, with the obvious changes (replacing multiplication by division, and requiring each \(\mathbf{b}_i\) to be invertible). Of course, instead of Lemma 1.346, we need to use Lemma A.27.

A.1.11 Approximator intersection lemma

Lemma A.28

Let \(\left(\mathbf{a}_{i}\right)_{i \in I} \in K\left[\left[x\right]\right]^{I}\) be a family of invertible FPSs. Let \(J\) be a subset of \(I\). Let \(n \in \mathbb {N}\). Let \(U\) be an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Then, \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\).

theorem AlgebraicCombinatorics.FPS.xnApproximator_inter {K : Type u_1} [CommRing K] {ι : Type u_2} [DecidableEq ι] {a : ιPowerSeries K} {n : } {U J : Finset ι} (hU : IsXnApproximator a n U) (hinv : ∀ (i : ι), IsUnit (PowerSeries.constantCoeff (a i))) :
∃ (M : Finset J), IsXnApproximator (fun (i : J) => a i) n M
Proof

The set \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). In other words, \(U\) is a finite subset of \(I\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by the definition of an \(x^n\)-approximator). Hence, in particular, \(U\) is finite. Moreover, \(U \subseteq I\) (since \(U\) is a subset of \(I\)).

Let \(M = U \cap J\). Thus, \(M = U \cap J \subseteq U\), so that the set \(M\) is finite (since \(U\) is finite). Moreover, \(M\) is a subset of \(J\) (since \(M = U \cap J \subseteq J\)).

Now, let \(N\) be a finite subset of \(J\) satisfying \(M \subseteq N \subseteq J\). We shall show that

\[ \prod _{i \in N} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in M} \mathbf{a}_{i}. \]

Indeed, the set \(N \cup U\) is finite (since \(N\) and \(U\) are finite) and is a subset of \(I\) (since \(N \subseteq J \subseteq I\) and \(U \subseteq I\)); it also satisfies \(U \subseteq N \cup U \subseteq I\). Now, we recall that \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Hence, Proposition 1.364 (a) (applied to \(U\) and \(N \cup U\) instead of \(M\) and \(J\)) yields

\[ \prod _{i \in N \cup U} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in U} \mathbf{a}_{i} \]

(since \(N \cup U\) is a finite subset of \(I\) satisfying \(U \subseteq N \cup U \subseteq I\)).

On the other hand, we have assumed that \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is a family of invertible FPSs. Thus, for each \(i \in I\), the FPS \(\mathbf{a}_{i}\) is invertible, so that its inverse \(\mathbf{a}_{i}^{-1}\) is well-defined. We obviously have

\[ \prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1} \overset {x^n}{\equiv } \prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1} \]

(since the relation \(\overset {x^n}{\equiv }\) is reflexive).

Hence, by the compatibility of \(\overset {x^n}{\equiv }\) with multiplication (Theorem 1.328 (b)), applied to \(a = \prod _{i \in N \cup U} \mathbf{a}_{i}\) and \(b = \prod _{i \in U} \mathbf{a}_{i}\) and \(c = \prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\) and \(d = \prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\), we obtain

\[ \left(\prod _{i \in N \cup U} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\right) \overset {x^n}{\equiv } \left(\prod _{i \in U} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\right). \]

On the other hand, the sets \(N\) and \(U \setminus J\) are disjoint (since \(N \subseteq J\) and \(U \setminus J \subseteq J^c\)), and their union is \(N \cup (U \setminus J) = N \cup U\) (since \(U = (U \cap J) \cup (U \setminus J)\) and \(U \cap J = M \subseteq N\)). Hence, the set \(N \cup U\) is the union of its two disjoint subsets \(N\) and \(U \setminus J\). Thus, we can split the product \(\prod _{i \in N \cup U} \mathbf{a}_{i}\) as follows:

\[ \prod _{i \in N \cup U} \mathbf{a}_{i} = \left(\prod _{i \in N} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}\right). \]

Multiplying both sides of this equality by \(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\), we obtain

\begin{align*} \left(\prod _{i \in N \cup U} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\right) & = \left(\prod _{i \in N} \mathbf{a}_{i}\right) \underbrace{ \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\right) }_{= \prod _{i \in U \setminus J} \left(\mathbf{a}_{i} \mathbf{a}_{i}^{-1}\right)} \\ & = \left(\prod _{i \in N} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \underbrace{\left(\mathbf{a}_{i} \mathbf{a}_{i}^{-1}\right)}_{= 1}\right) = \left(\prod _{i \in N} \mathbf{a}_{i}\right) \underbrace{\left(\prod _{i \in U \setminus J} 1\right)}_{= 1} \\ & = \prod _{i \in N} \mathbf{a}_{i}. \end{align*}

However, the set \(U\) is the union of its two disjoint subsets \(U \cap J\) and \(U \setminus J\). Thus, we can split the product \(\prod _{i \in U} \mathbf{a}_{i}\) as follows:

\[ \prod _{i \in U} \mathbf{a}_{i} = \left(\prod _{i \in U \cap J} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}\right). \]

Multiplying both sides by \(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\), we obtain

\begin{align*} \left(\prod _{i \in U} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\right) & = \underbrace{\left(\prod _{i \in U \cap J} \mathbf{a}_{i}\right)}_{ = \prod _{i \in M} \mathbf{a}_{i} \text{ (since } U \cap J = M \text{)}} \underbrace{ \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \mathbf{a}_{i}^{-1}\right) }_{= \prod _{i \in U \setminus J} \left(\mathbf{a}_{i} \mathbf{a}_{i}^{-1}\right)} \\ & = \left(\prod _{i \in M} \mathbf{a}_{i}\right) \left(\prod _{i \in U \setminus J} \underbrace{\left(\mathbf{a}_{i} \mathbf{a}_{i}^{-1}\right)}_{= 1}\right) = \left(\prod _{i \in M} \mathbf{a}_{i}\right) \underbrace{\left(\prod _{i \in U \setminus J} 1\right)}_{= 1} \\ & = \prod _{i \in M} \mathbf{a}_{i}. \end{align*}

Substituting these two simplifications into the \(x^n\)-equivalence above, we obtain

\[ \prod _{i \in N} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in M} \mathbf{a}_{i}. \]

In other words, each \(m \in \left\{ 0, 1, \ldots , n\right\} \) satisfies

\[ \left[x^{m}\right] \left(\prod _{i \in N} \mathbf{a}_{i}\right) = \left[x^{m}\right] \left(\prod _{i \in M} \mathbf{a}_{i}\right) \]

(by the definition of \(\overset {x^n}{\equiv }\)).

Forget that we fixed \(N\). We have thus shown that every finite subset \(N\) of \(J\) satisfying \(M \subseteq N \subseteq J\) satisfies the above equality for each \(m \in \left\{ 0, 1, \ldots , n\right\} \).

Now, let \(m \in \left\{ 0, 1, \ldots , n\right\} \). Then, every finite subset \(N\) of \(J\) satisfying \(M \subseteq N \subseteq J\) satisfies

\[ \left[x^{m}\right] \left(\prod _{i \in N} \mathbf{a}_{i}\right) = \left[x^{m}\right] \left(\prod _{i \in M} \mathbf{a}_{i}\right). \]

In other words, the set \(M\) determines the \(x^m\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (by the definition of “determining the \(x^m\)-coefficient in a product”).

Forget that we fixed \(m\). We thus have shown that \(M\) determines the \(x^m\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) for each \(m \in \left\{ 0, 1, \ldots , n\right\} \). In other words, \(M\) determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\). In other words, \(M\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (by the definition of an “\(x^n\)-approximator”, since \(M\) is a finite subset of \(J\)). In other words, \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (since \(M = U \cap J\)). This proves Lemma A.28.

A.1.12 Detailed proof of Proposition 1.369

Detailed proof of Proposition 1.369

Let \(J\) be a subset of \(I\). We shall show that the family \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is multipliable.

Fix \(n \in \mathbb {N}\). We know that the family \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is multipliable. Hence, there exists an \(x^n\)-approximator \(U\) for \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by Lemma 1.363). Consider this \(U\).

Set \(M = U \cap J\). Lemma A.28 yields that \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\). In other words, \(M\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (since \(M = U \cap J\)). In other words, \(M\) is a finite subset of \(J\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) (by the definition of an \(x^n\)-approximator). Thus, the set \(M\) determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\). Hence, in particular, this set \(M\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\). Therefore, the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is finitely determined (by the definition of “finitely determined”, since \(M\) is a finite subset of \(J\)).

Forget that we fixed \(n\). We thus have proved that for each \(n \in \mathbb {N}\), the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is finitely determined. In other words, each coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is finitely determined. In other words, the family \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is multipliable (by the definition of “multipliable”).

Forget that we fixed \(J\). We thus have shown that the family \(\left(\mathbf{a}_{i}\right)_{i \in J}\) is multipliable whenever \(J\) is a subset of \(I\). In other words, any subfamily of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is multipliable. This proves Proposition 1.369.

A.1.13 Finite products and \(x^n\)-equivalence

Lemma A.29

Let \(n \in \mathbb {N}\). Let \(V\) be a finite set. Let \(\left(c_{w}\right)_{w \in V} \in K\left[\left[x\right]\right]^{V}\) and \(\left(d_{w}\right)_{w \in V} \in K\left[\left[x\right]\right]^{V}\) be two families of FPSs such that

\[ \text{each } w \in V \text{ satisfies } c_{w} \overset {x^n}{\equiv } d_{w}. \]

Then, we have

\[ \prod _{w \in V} c_{w} \overset {x^n}{\equiv } \prod _{w \in V} d_{w}. \]
theorem AlgebraicCombinatorics.FPS.xnEquiv_finprod {K : Type u_1} [CommRing K] {ι : Type u_2} {n : } {V : Finset ι} {c d : ιPowerSeries K} (h : vV, c v ≡[x^n] d v) :
vV, c v ≡[x^n] vV, d v
Proof

This is just Theorem 1.328 (f) (the part about products), with the letters \(S\), \(s\), \(a_s\), and \(b_s\) renamed as \(V\), \(w\), \(c_w\), and \(d_w\).

A.1.14 Detailed proof of Proposition 1.372

Detailed proof of Proposition 1.372

We shall subdivide our proof into several claims.

Claim 1: Let \(w \in W\). Then, the family \(\left(\mathbf{a}_{s}\right)_{s \in S,\; f(s) = w}\) is multipliable.

[Proof of Claim 1: This was an assumption of Proposition 1.372.]

Let us set

\[ \mathbf{b}_{w} := \prod _{\substack{[s, , \in , S, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s} \qquad \text{for each } w \in W. \]

This is well-defined, because for each \(w \in W\), the product \(\prod _{\substack{[s, , \in , S, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s}\) is well-defined (since Claim 1 shows that the family \(\left(\mathbf{a}_{s}\right)_{s \in S,\; f(s) = w}\) is multipliable).

Now, let \(n \in \mathbb {N}\). By Lemma 1.363 (applied to \(S\) and \(\left(\mathbf{a}_{s}\right)_{s \in S}\) instead of \(I\) and \(\left(\mathbf{a}_{i}\right)_{i \in I}\)), there exists an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in S}\). Pick such an \(x^n\)-approximator, and call it \(U\). Then, \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in S}\); in other words, \(U\) is a finite subset of \(S\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{s}\right)_{s \in S}\) (by the definition of an \(x^n\)-approximator).

The set \(U\) is finite. Thus, its image \(f(U) = \left\{ f(u) \mid u \in U\right\} \) is finite as well. Now, we claim the following:

Claim 2: For each \(w \in W\), we have

\[ \mathbf{b}_{w} \overset {x^n}{\equiv } \prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s}. \]

[Proof of Claim 2: Let \(w \in W\). Let \(J\) be the subset \(\left\{ s \in S \mid f(s) = w\right\} \) of \(S\). Then, the family \(\left(\mathbf{a}_{s}\right)_{s \in J}\) is just the family \(\left(\mathbf{a}_{s}\right)_{s \in S,\; f(s) = w}\), and thus is multipliable (by Claim 1). Furthermore, Lemma A.28 (applied to \(S\) and \(\left(\mathbf{a}_{s}\right)_{s \in S}\) instead of \(I\) and \(\left(\mathbf{a}_{i}\right)_{i \in I}\)) yields that \(U \cap J\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in J}\) (since \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{s}\right)_{s \in S}\)). Hence, Proposition 1.364 (b) (applied to \(J\), \(\left(\mathbf{a}_{s}\right)_{s \in J}\) and \(U \cap J\) instead of \(I\), \(\left(\mathbf{a}_{i}\right)_{i \in I}\) and \(M\)) yields

\[ \prod _{s \in J} \mathbf{a}_{s} \overset {x^n}{\equiv } \prod _{s \in U \cap J} \mathbf{a}_{s}. \]

However, we have \(J = \left\{ s \in S \mid f(s) = w\right\} \). Thus, \(\prod _{s \in J} \mathbf{a}_{s} = \prod _{\substack{[s, , \in , S, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s} = \mathbf{b}_w\) and \(U \cap J = \left\{ s \in U \mid f(s) = w\right\} \). So the product sign “\(\prod _{s \in U \cap J}\)” is equivalent to “\(\prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}}\)”. Thus,

\[ \mathbf{b}_{w} \overset {x^n}{\equiv } \prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s}. \]

This proves Claim 2.]

Claim 3: The set \(f(U)\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{b}_{w}\right)_{w \in W}\).

[Proof of Claim 3: Let \(T\) be a finite subset of \(W\) satisfying \(f(U) \subseteq T\). We must show that \(\left[x^n\right] \left(\prod _{w \in T} \mathbf{b}_w\right) = \left[x^n\right] \left(\prod _{w \in f(U)} \mathbf{b}_w\right)\).

By Claim 2, for each \(w \in W\) we have \(\mathbf{b}_{w} \overset {x^n}{\equiv } \prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s}\). Hence, by Lemma A.29, we get

\[ \prod _{w \in T} \mathbf{b}_w \overset {x^n}{\equiv } \prod _{w \in T} \prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s} \]

and similarly

\[ \prod _{w \in f(U)} \mathbf{b}_w \overset {x^n}{\equiv } \prod _{w \in f(U)} \prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s}. \]

Now, for \(w \notin f(U)\), there are no \(s \in U\) with \(f(s) = w\), so the inner product is \(1\) (the empty product). Hence, for any finite set \(V \supseteq f(U)\),

\[ \prod _{w \in V} \prod _{\substack{[s, , \in , U, ;, \\ , , f, (, s, ), , =, , w]}} \mathbf{a}_{s} = \prod _{s \in U} \mathbf{a}_{s} \]

(by the standard fiberwise reindexing of finite products). Applying this to both \(V = T\) and \(V = f(U)\), we conclude that both products equal \(\prod _{s \in U} \mathbf{a}_{s}\). Therefore,

\[ \left[x^n\right] \left(\prod _{w \in T} \mathbf{b}_w\right) = \left[x^n\right] \left(\prod _{s \in U} \mathbf{a}_s\right) = \left[x^n\right] \left(\prod _{w \in f(U)} \mathbf{b}_w\right). \]

This proves Claim 3.]

From Claim 3, the \(x^n\)-coefficient in the product of \(\left(\mathbf{b}_w\right)_{w \in W}\) is finitely determined (since \(f(U)\) is a finite subset of \(W\)). Since this holds for each \(n \in \mathbb {N}\), the family \(\left(\mathbf{b}_w\right)_{w \in W}\) is multipliable. This proves part (a) of Proposition 1.372.

For part (b), we observe that by Proposition 1.364 (b), the infinite product \(\prod _{s \in S} \mathbf{a}_s\) is \(x^n\)-equivalent to \(\prod _{s \in U} \mathbf{a}_s\). By the computation above, the infinite product \(\prod _{w \in W} \mathbf{b}_w\) is also \(x^n\)-equivalent to \(\prod _{s \in U} \mathbf{a}_s\). Since this holds for all \(n\), the two infinite products are equal.

A.1.15 Detailed proof of Proposition 1.366

Detailed proof of Proposition 1.366

(a) Fix \(n \in \mathbb {N}\). We know that the family \(\left(\mathbf{a}_{i}\right)_{i \in I}\) is multipliable. Hence, there exists an \(x^n\)-approximator \(U\) for \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by Lemma 1.363). Consider this \(U\).

We also know that the family \(\left(\mathbf{b}_{i}\right)_{i \in I}\) is multipliable. Hence, there exists an \(x^n\)-approximator \(V\) for \(\left(\mathbf{b}_{i}\right)_{i \in I}\) (by Lemma 1.363, applied to \(\mathbf{b}_{i}\) instead of \(\mathbf{a}_{i}\)). Consider this \(V\).

We know that \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). In other words, \(U\) is a finite subset of \(I\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (by the definition of an \(x^n\)-approximator). Hence, in particular, \(U\) is finite. Similarly, \(V\) is finite. Moreover, \(U \subseteq I\); similarly, \(V \subseteq I\).

Let \(M = U \cup V\). This set \(M\) is finite (since \(U\) and \(V\) are finite). Moreover, \(M = U \cup V \subseteq I \cup I = I\). Hence, \(M\) is a finite subset of \(I\).

Now, let \(N\) be a finite subset of \(I\) satisfying \(M \subseteq N \subseteq I\). We shall show that

\[ \left[x^{n}\right] \left(\prod _{i \in N} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left(\prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right). \]

Indeed, let \(m \in \left\{ 0, 1, \ldots , n\right\} \). We have \(U \subseteq U \cup V = M \subseteq N\). The set \(N\) is a finite subset of \(I\) and satisfies \(U \subseteq N\). Now, recall that \(U\) determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Hence, \(U\) determines the \(x^m\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) (since \(m \in \left\{ 0, 1, \ldots , n\right\} \)). In other words, every finite subset \(T\) of \(I\) satisfying \(U \subseteq T \subseteq I\) satisfies

\[ \left[x^{m}\right] \left(\prod _{i \in T} \mathbf{a}_{i}\right) = \left[x^{m}\right] \left(\prod _{i \in U} \mathbf{a}_{i}\right). \]

We can apply this to \(T = N\) (since \(N\) is a finite subset of \(I\) satisfying \(U \subseteq N \subseteq I\)), and thus obtain

\[ \left[x^{m}\right] \left(\prod _{i \in N} \mathbf{a}_{i}\right) = \left[x^{m}\right] \left(\prod _{i \in U} \mathbf{a}_{i}\right). \]

However, we can also apply it to \(T = M\) (since \(M\) is a finite subset of \(I\) satisfying \(U \subseteq M \subseteq I\)), and thus obtain

\[ \left[x^{m}\right] \left(\prod _{i \in M} \mathbf{a}_{i}\right) = \left[x^{m}\right] \left(\prod _{i \in U} \mathbf{a}_{i}\right). \]

Comparing these two equalities, we obtain

\[ \left[x^{m}\right] \left(\prod _{i \in N} \mathbf{a}_{i}\right) = \left[x^{m}\right] \left(\prod _{i \in M} \mathbf{a}_{i}\right). \]

The same argument (applied to \(\mathbf{b}_{i}\) and \(V\) instead of \(\mathbf{a}_{i}\) and \(U\)) yields

\[ \left[x^{m}\right] \left(\prod _{i \in N} \mathbf{b}_{i}\right) = \left[x^{m}\right] \left(\prod _{i \in M} \mathbf{b}_{i}\right). \]

Forget that we fixed \(m\). We thus have proved these equalities for each \(m \in \left\{ 0, 1, \ldots , n\right\} \). Hence, Lemma 1.346 (applied to \(a = \prod _{i \in N} \mathbf{a}_{i}\) and \(b = \prod _{i \in M} \mathbf{a}_{i}\) and \(c = \prod _{i \in N} \mathbf{b}_{i}\) and \(d = \prod _{i \in M} \mathbf{b}_{i}\)) yields that

\[ \left[x^{m}\right] \left( \left(\prod _{i \in N} \mathbf{a}_{i}\right) \left(\prod _{i \in N} \mathbf{b}_{i}\right)\right) = \left[x^{m}\right] \left( \left(\prod _{i \in M} \mathbf{a}_{i}\right) \left(\prod _{i \in M} \mathbf{b}_{i}\right)\right) \]

for each \(m \in \left\{ 0, 1, \ldots , n\right\} \). Applying this to \(m = n\), we obtain

\[ \left[x^{n}\right] \left( \left(\prod _{i \in N} \mathbf{a}_{i}\right) \left(\prod _{i \in N} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left( \left(\prod _{i \in M} \mathbf{a}_{i}\right) \left(\prod _{i \in M} \mathbf{b}_{i}\right)\right). \]

In view of

\[ \prod _{i \in N} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right) = \left(\prod _{i \in N} \mathbf{a}_{i}\right) \left(\prod _{i \in N} \mathbf{b}_{i}\right) \qquad \text{and} \qquad \prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right) = \left(\prod _{i \in M} \mathbf{a}_{i}\right) \left(\prod _{i \in M} \mathbf{b}_{i}\right), \]

this rewrites as

\[ \left[x^{n}\right] \left(\prod _{i \in N} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left(\prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right). \]

Forget that we fixed \(N\). We thus have shown that every finite subset \(N\) of \(I\) satisfying \(M \subseteq N \subseteq I\) satisfies the above equality. In other words, \(M\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) (by the definition of “determining the \(x^n\)-coefficient”). Hence, the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is finitely determined (since \(M\) is a finite subset of \(I\)).

Forget that we fixed \(n\). We thus have proved that for each \(n \in \mathbb {N}\), the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is finitely determined. In other words, the family \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is multipliable. This proves Proposition 1.366 (a).

(b) Proposition 1.366 (a) shows that the family \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\) is multipliable.

Let \(n \in \mathbb {N}\). In our above proof of Proposition 1.366 (a), we have seen the following:

  • There exists an \(x^n\)-approximator \(U\) for \(\left(\mathbf{a}_{i}\right)_{i \in I}\).

  • There exists an \(x^n\)-approximator \(V\) for \(\left(\mathbf{b}_{i}\right)_{i \in I}\).

Consider these \(U\) and \(V\). Let \(M = U \cup V\). Thus, \(M = U \cup V \supseteq U\) and \(M = U \cup V \supseteq V\). In our above proof, we have seen that \(M\) is a finite subset of \(I\) and \(M\) determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\).

We recall that the relation \(\overset {x^n}{\equiv }\) is an equivalence relation (by Theorem 1.328 (a)).

Now, the definition of the infinite product \(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\) (namely, Definition 1.343 (b)) yields that

\[ \left[x^{n}\right] \left(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left(\prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) \]

(since \(M\) is a finite subset of \(I\) that determines the \(x^n\)-coefficient in the product of \(\left(\mathbf{a}_{i} \mathbf{b}_{i}\right)_{i \in I}\)). On the other hand, the set \(U\) is an \(x^n\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i \in I}\). Thus, Proposition 1.364 (b) (applied to \(U\) instead of \(M\)) yields

\[ \prod _{i \in I} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in U} \mathbf{a}_{i}. \]

Since the relation \(\overset {x^n}{\equiv }\) is symmetric, we thus obtain \(\prod _{i \in U} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in I} \mathbf{a}_{i}\). Moreover, \(M\) is a finite subset of \(I\) satisfying \(U \subseteq M\); hence, Proposition 1.364 (a) yields

\[ \prod _{i \in M} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in U} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in I} \mathbf{a}_{i}. \]

Hence, \(\prod _{i \in M} \mathbf{a}_{i} \overset {x^n}{\equiv } \prod _{i \in I} \mathbf{a}_{i}\) (since the relation \(\overset {x^n}{\equiv }\) is transitive). The same argument (applied to \(\left(\mathbf{b}_{i}\right)_{i \in I}\) and \(V\) instead of \(\left(\mathbf{a}_{i}\right)_{i \in I}\) and \(U\)) yields \(\prod _{i \in M} \mathbf{b}_{i} \overset {x^n}{\equiv } \prod _{i \in I} \mathbf{b}_{i}\). From these two \(x^n\)-equivalences, we obtain

\[ \left(\prod _{i \in M} \mathbf{a}_{i}\right) \left(\prod _{i \in M} \mathbf{b}_{i}\right) \overset {x^n}{\equiv } \left(\prod _{i \in I} \mathbf{a}_{i}\right) \left(\prod _{i \in I} \mathbf{b}_{i}\right) \]

(by Theorem 1.328 (b)). In view of

\[ \left(\prod _{i \in M} \mathbf{a}_{i}\right) \left(\prod _{i \in M} \mathbf{b}_{i}\right) = \prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right), \]

this rewrites as

\[ \prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right) \overset {x^n}{\equiv } \left(\prod _{i \in I} \mathbf{a}_{i}\right) \left(\prod _{i \in I} \mathbf{b}_{i}\right). \]

In other words,

\[ \text{each } m \in \left\{ 0, 1, \ldots , n\right\} \text{ satisfies } \left[x^{m}\right] \left(\prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{m}\right] \left( \left(\prod _{i \in I} \mathbf{a}_{i}\right) \left(\prod _{i \in I} \mathbf{b}_{i}\right)\right). \]

Applying this to \(m = n\), we obtain

\[ \left[x^{n}\right] \left(\prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left( \left(\prod _{i \in I} \mathbf{a}_{i}\right) \left(\prod _{i \in I} \mathbf{b}_{i}\right)\right). \]

In view of \(\left[x^{n}\right] \left(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left(\prod _{i \in M} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right)\), this rewrites as

\[ \left[x^{n}\right] \left(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\right) = \left[x^{n}\right] \left( \left(\prod _{i \in I} \mathbf{a}_{i}\right) \left(\prod _{i \in I} \mathbf{b}_{i}\right)\right). \]

Now, forget that we fixed \(n\). We thus have proved that each \(n \in \mathbb {N}\) satisfies the above equality. In other words, each coefficient of the FPS \(\prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right)\) equals the corresponding coefficient of \(\left(\prod _{i \in I} \mathbf{a}_{i}\right) \left(\prod _{i \in I} \mathbf{b}_{i}\right)\). Hence, we have

\[ \prod _{i \in I} \left(\mathbf{a}_{i} \mathbf{b}_{i}\right) = \left(\prod _{i \in I} \mathbf{a}_{i}\right) \cdot \left(\prod _{i \in I} \mathbf{b}_{i}\right). \]

This proves Proposition 1.366 (b).

A.1.16 Product rule claims

Lemma A.30

(Claim 3.) If \((i,k) \notin T'_n\) (the coefficient support union up to \(n\)) and \(k \neq 0\), then \([x^m] p_{i,k} = 0\) for all \(m \in \{ 0,1,\ldots ,n\} \).

theorem PowerSeries.prodRule_claim3 {K : Type u_1} [CommRing K] {I : Type u_2} (p : IPowerSeries K) (n : ) (i : I) (k : ) (hk : k 0) (hnotin : (i, k)CoeffSupportSetUnion p n) (m : ) :
m n(coeff m) (p i k) = 0
Proof

If \([x^m] p_{i,k} \neq 0\) for some \(m \leq n\), then \((i,k) \in T_m \subseteq T'_n\), contradicting the hypothesis.

Lemma A.31

(Claim 4.) If \((k_i)_{i \in I}\) is essentially finite and \(p_{i,0} = 1\) for all \(i\), then the family \((p_{i,k_i})_{i \in I}\) is multipliable.

theorem PowerSeries.prodRule_claim4 {K : Type u_1} [CommRing K] {I : Type u_2} (p : IPowerSeries K) (hp0 : ∀ (i : I), p i 0 = 1) (k : I) (hk : EssentiallyFinite k) :
{i : I | p i (k i) 1}.Finite
Proof

All but finitely many \(i \in I\) satisfy \(k_i = 0\) (since \((k_i)_{i \in I}\) is essentially finite) and thus \(p_{i,k_i} = p_{i,0} = 1\). Hence, all but finitely many entries of the family \((p_{i,k_i})_{i \in I}\) equal \(1\). Thus, this family is multipliable (by Proposition 1.351).

Lemma A.32

(Claim 5.) If some \(j \in I\) satisfies \(k_j \neq 0\) and \((j, k_j) \notin T'_n\), then \([x^n](\prod _{i \in s} p_{i,k_i}) = 0\) for any finite \(s \ni j\).

theorem PowerSeries.prodRule_claim5 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : IPowerSeries K) (n : ) (k : I) (_hk : EssentiallyFinite k) (_hp0 : ∀ (i : I), p i 0 = 1) (j : I) (hkj : k j 0) (hnotin : (j, k j)CoeffSupportSetUnion p n) (s : Finset I) :
j s(coeff n) (∏ is, p i (k i)) = 0
Proof

The product \(\prod _{i \in s} p_{i,k_i}\) is a multiple of \(p_{j,k_j}\) (since \(p_{j,k_j}\) is one of the factors of this product). Moreover, by Claim 3, we have \([x^m] p_{j,k_j} = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \). Hence, Lemma A.42 (applied to \(u = p_{j,k_j}\) and \(v = \prod _{i \in s} p_{i,k_i}\)) shows that \([x^m](\prod _{i \in s} p_{i,k_i}) = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \). Applying this to \(m = n\) yields the claim.

Lemma A.33

(Claim 6.) If \(j \notin I_n\) and \(k_j \neq 0\), then \([x^n](\prod _{i \in s} p_{i,k_i}) = 0\) for any finite \(s \ni j\).

theorem PowerSeries.prodRule_claim6 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : IPowerSeries K) (n : ) (k : I) (hk : EssentiallyFinite k) (hp0 : ∀ (i : I), p i 0 = 1) (j : I) (hj_notin : jIndexSetIn p n) (hkj : k j 0) (s : Finset I) :
j s(coeff n) (∏ is, p i (k i)) = 0
Proof

We have \(k_j \in S_j\) and \(k_j \neq 0\), so \((j, k_j) \in \overline{S}\). Moreover, \((j, k_j) \notin T'_n\) (because if we had \((j, k_j) \in T'_n\), then we would have \(j \in I_n\) by the definition of \(I_n\); but this would contradict \(j \notin I_n\)). Hence, \((j, k_j) \in \overline{S} \setminus T'_n\). Therefore, Claim 5 yields \([x^n](\prod _{i \in s} p_{i,k_i}) = 0\).

Lemma A.34

(Claim 7.) The family \((\prod _{i \in I_n} p_{i,k_i})\) indexed by essentially finite families \((k_i)\) supported on \(I_n\) is summable: for each \(n\), only finitely many such families yield \([x^n](\prod _{i \in I_n} p_{i,k_i}) \neq 0\).

theorem PowerSeries.prodRule_claim7 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : IPowerSeries K) (_hp0 : ∀ (i : I), p i 0 = 1) (n : ) (_hTn_finite : (CoeffSupportSetUnion p n).Finite) (hIn_finite : (IndexSetIn p n).Finite) (hKn_finite : (ValueSetKn p n).Finite) :
{k : I | EssentiallyFinite k (∀ ihIn_finite.toFinset, k i = 0) (coeff n) (∏ ihIn_finite.toFinset, p i (k i)) 0}.Finite
Proof

Let \((k_i)_{i \in I} \in S^I_{\mathrm{fin}}\) satisfy \([x^n](\prod _{i \in I} p_{i,k_i}) \neq 0\). Then it must satisfy two properties: (1) all \(i \in I \setminus I_n\) satisfy \(k_i = 0\) (otherwise Claim 6 would give a contradiction); (2) all \(i \in I_n\) satisfy \(k_i \in K_n \cup \{ 0\} \) (otherwise \((j, k_j) \in \overline{S} \setminus T'_n\) for some \(j \in I_n\), and Claim 5 would give a contradiction). These two properties together restrict \((k_i)\) to finitely many possibilities (since the sets \(I_n\) and \(K_n \cup \{ 0\} \) are finite). Hence, all but finitely many families yield \([x^n](\prod _{i \in I} p_{i,k_i}) = 0\), proving summability.

Lemma A.35

(Claim 9.) For \(i \notin I_n\), we have \([x^m](\sum _{k \in S_i \setminus \{ 0\} } p_{i,k}) = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \).

theorem PowerSeries.prodRule_claim9 {K : Type u_1} [CommRing K] {I : Type u_2} (p : IPowerSeries K) (n : ) (i : I) (hi : iIndexSetIn p n) (Si : Finset ) (_hSi : 0 Si) (m : ) :
m n(coeff m) (∑ kSi \ {0}, p i k) = 0
Proof

Each term \(p_{i,k}\) with \(k \neq 0\) has \([x^m] p_{i,k} = 0\) by Claim 3 (since \((i,k) \notin T'_n\) because \(i \notin I_n\)).

Lemma A.36

(Claim 10.) For any finite set \(J \supseteq I_n\), \([x^n](\prod _{i \in J} \sum _{k \in S_i} p_{i,k}) = [x^n](\prod _{i \in I_n} \sum _{k \in S_i} p_{i,k})\). The product stabilizes at \(I_n\).

theorem PowerSeries.prodRule_claim10 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : IPowerSeries K) (n : ) (hp0 : ∀ (i : I), p i 0 = 1) (In : Finset I) (hIn : iIn, iIndexSetIn p n) (S : IFinset ) (hS0 : ∀ (i : I), 0 S i) (J : Finset I) (hInJ : In J) :
(coeff n) (∏ iJ, kS i, p i k) = (coeff n) (∏ iIn, kS i, p i k)
Proof

For \(i \in J \setminus I_n\), we have \(\sum _{k \in S_i} p_{i,k} = 1 + \sum _{k \in S_i \setminus \{ 0\} } p_{i,k}\). By Claim 9, the remainder has zero coefficients up to degree \(n\), so multiplying by it does not change the coefficient at degree \(n\).

Lemma A.37

(Claim 11.) For a finite index set \(I_n\),

\[ \prod _{i \in I_n} \sum _{k \in S_i} p_{i,k} = \sum _{(k_i) \in S^{I_n}} \prod _{i \in I_n} p_{i,k_i}. \]

This is the standard finite distributive law (product of sums equals sum of products).

theorem PowerSeries.prodRule_claim11 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : IPowerSeries K) (In : Finset I) (S : IFinset ) :
iIn, kS i, p i k = fFintype.piFinset fun (i : In) => S i, i : In, p (↑i) (f i)
Proof

This is the standard finite distributive law (product of sums equals sum of products over all choice functions). See Proposition 1.383.

Lemma A.38

(Claim 8.) The coefficient of the sum over essentially finite families equals the coefficient of the sum restricted to the finite index set \(I_n\):

\[ [x^n]\Bigl(\sum _{\substack{[(, k, _, i, ), , \in , S, ^, I, _, {, \mathrm , {, f, i, n, }, }]}} \prod _{i \in I_n} p_{i,k_i}\Bigr) = [x^n]\Bigl(\sum _{(k_i) \in S^{I_n}} \prod _{i \in I_n} p_{i,k_i}\Bigr). \]
theorem PowerSeries.prodRule_claim8 {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (p : IPowerSeries K) (n : ) (_hp0 : ∀ (i : I), p i 0 = 1) (In : Finset I) (_hIn : iIn, iIndexSetIn p n) (S : IFinset ) (_hS0 : ∀ (i : I), 0 S i) (essFinFamilies : Finset (I)) (_hEss : kessFinFamilies, EssentiallyFinite k) (hSIn : kessFinFamilies, iIn, k i = 0) (hValInS : kessFinFamilies, iIn, k i S i) (hComplete : ∀ (k : I), (∀ iIn, k i = 0)(∀ iIn, k i S i)k essFinFamilies) :
(coeff n) (∑ kessFinFamilies, iIn, p i (k i)) = (coeff n) (∑ fFintype.piFinset fun (i : In) => S i, i : In, p (↑i) (f i))
Proof

The proof establishes a bijection between essentially finite families supported on \(I_n\) and functions \(I_n \to S\), via restriction and extension by \(0\).

A.1.17 Composition rules for infinite products

Lemma A.39

If \(f_1 \overset {x^n}{\equiv } f_2\) and \([x^0]g = 0\), then \(f_1 \circ g \overset {x^n}{\equiv } f_2 \circ g\). That is, \(x^n\)-equivalence is preserved under composition with a fixed inner series.

theorem PowerSeries.xnEquiv_comp {K : Type u_1} [CommRing K] {n : } {f₁ f₂ g : PowerSeries K} (hf : kn, (coeff k) f₁ = (coeff k) f₂) (hg : constantCoeff g = 0) (k : ) :
k n(coeff k) (subst g f₁) = (coeff k) (subst g f₂)
Proof

The coefficient \([x^k](f \circ g)\) involves a sum over \(d\) of \([x^d]f \cdot [x^k](g^d)\). For \(d {\gt} k\), \([x^k](g^d) = 0\) since \(\operatorname {ord}(g^d) \geq d {\gt} k\). For \(d \leq k \leq n\), \([x^d]f_1 = [x^d]f_2\) by \(x^n\)-equivalence.

Lemma A.40

If \(M\) is an \(x^n\)-approximator for \((f_i)_{i \in I}\) (i.e., for all \(k \leq n\) and \(J \supseteq M\), \([x^k](\prod _{i \in J} f_i) = [x^k](\prod _{i \in M} f_i)\)), and \([x^0]g = 0\), then for all \(J \supseteq M\), \([x^n](\prod _{i \in J} (f_i \circ g)) = [x^n](\prod _{i \in M} (f_i \circ g))\).

theorem PowerSeries.comp_prod_approx_determines {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (f : IPowerSeries K) (g : PowerSeries K) (hg : constantCoeff g = 0) (n : ) (M : Finset I) (hM_approx : kn, ∀ (J : Finset I), M J(coeff k) (∏ iJ, f i) = (coeff k) (∏ iM, f i)) (J : Finset I) :
M J(coeff n) (∏ iJ, subst g (f i)) = (coeff n) (∏ iM, subst g (f i))
Proof

By Lemma A.43, \(\prod _{i \in J} (f_i \circ g) = (\prod _{i \in J} f_i) \circ g\). The approximator condition gives \(\prod _{i \in J} f_i \overset {x^n}{\equiv } \prod _{i \in M} f_i\). By Lemma A.39, composing with \(g\) preserves the equivalence.

Proposition A.41

If \((f_i)_{i \in I}\) is multipliable and \([x^0]g = 0\), then \((f_i \circ g)_{i \in I}\) is multipliable.

theorem PowerSeries.comp_prod_multipliable {K : Type u_1} [CommRing K] {I : Type u_2} [DecidableEq I] (f : IPowerSeries K) (g : PowerSeries K) (hg : constantCoeff g = 0) (hf_mulable : ∀ (n : ), ∃ (M : Finset I), ∀ (J : Finset I), M J(coeff n) (∏ iJ, f i) = (coeff n) (∏ iM, f i)) (n : ) :
∃ (M : Finset I), ∀ (J : Finset I), M J(coeff n) (∏ iJ, subst g (f i)) = (coeff n) (∏ iM, subst g (f i))
Proof

For each \(n\), combine the approximators for degrees \(0, 1, \ldots , n\) into a single approximator \(M\) (their union), then apply Lemma A.40.

A.1.18 Additional supporting lemmas

Lemma A.42

If \(u \mid v\) and \([x^m] u = 0\) for all \(m \leq n\), then \([x^m] v = 0\) for all \(m \leq n\).

theorem PowerSeries.coeff_zero_of_dvd {K : Type u_1} [CommRing K] {n : } {u v : PowerSeries K} (hdvd : u v) (hu : mn, (coeff m) u = 0) (m : ) :
m n(coeff m) v = 0
Proof

Write \(v = u \cdot w\). Then \([x^m] v = \sum _{(i,j) \in \mathrm{antidiag}(m)} [x^i] u \cdot [x^j] w\). Since \(i \leq m \leq n\), we have \([x^i] u = 0\), so each term vanishes.