1 Finset

1.1 Piecewise

Lemma 1 prod ite not mem

✓

Let \(s, t\) be finite sets of indices in \(\iota \), and let \(f \colon \iota \to M\). Then

\[ \prod _{x \in s} \begin{cases} 1, & \text{if } x \in t, \\ f(x), & \text{otherwise} \end{cases} = \prod _{x \in s \setminus t} f(x). \]

Proof ▶

We split the product over the disjoint union \(s = (s \setminus t) \cup (s \cap t)\).

\begin{align*} \prod _{x \in s} \begin{cases} 1, & \text{if } x \in t \\ f(x), & \text{otherwise} \end{cases}& = \left( \prod _{x \in s \setminus t} f(x) \right) \cdot \left( \prod _{x \in s \cap t} 1 \right) \\ & = \prod _{x \in s \setminus t} f(x). \end{align*}

The first equality holds because for any \(x \in s \setminus t\), the term is \(f(x)\), while for any \(x \in s \cap t\), the term is \(1\). The product of ones is one.

Lemma 2 sum ite not mem

✓

Let \(s, t\) be finite sets of indices in \(\iota \), and let \(f \colon \iota \to A\) be a function to an additive commutative monoid. Then

\[ \sum _{x \in s} \begin{cases} 0, & \text{if } x \in t, \\ f(x), & \text{otherwise} \end{cases} = \sum _{x \in s \setminus t} f(x). \]

Proof ▶

We split the sum over the disjoint union \(s = (s \setminus t) \cup (s \cap t)\).

\begin{align*} \sum _{x \in s} \begin{cases} 0, & \text{if } x \in t \\ f(x), & \text{otherwise} \end{cases}& = \left( \sum _{x \in s \setminus t} f(x) \right) + \left( \sum _{x \in s \cap t} 0 \right) \\ & = \sum _{x \in s \setminus t} f(x). \end{align*}

The first equality holds because for any \(x \in s \setminus t\), the term is \(f(x)\), while for any \(x \in s \cap t\), the term is \(0\). The sum of zeros is zero.

1.2 Off-diagonal

Lemma 3 prod product eq prod offDiag of diag one

✓

Let \(s\) be a finite set of indices in \(\iota \), and let \(F \colon \iota \times \iota \to M\) where \(M\) is a commutative monoid. Assume that the diagonal values are all \(1\), i.e.

\[ \forall a \in s,\quad F(a,a)=1. \]

Then the product of \(F\) over the Cartesian product \(s\times s\) equals the product over the off-diagonal part:

\[ \prod _{x\in s\times s} F(x) \; =\; \prod _{x\in s.\mathrm{offDiag}} F(x). \]

Proof ▶

We use the decomposition of the square into diagonal and off-diagonal parts:

\[ s\times s \; =\; s.\mathrm{diag} \, \cup \, s.\mathrm{offDiag}, \]

and these two subsets are disjoint. Hence the product over \(s\times s\) splits as

\[ \prod _{x\in s\times s} F(x) \; =\; \left(\prod _{x\in s.\mathrm{diag}} F(x)\right) \cdot \left(\prod _{x\in s.\mathrm{offDiag}} F(x)\right). \]

On the diagonal, we have \(F(a,a)=1\) for all \(a\in s\), so

\[ \prod _{x\in s.\mathrm{diag}} F(x) = \prod _{a\in s} F(a,a) = \prod _{a\in s} 1 = 1. \]

Therefore,

\[ \prod _{x\in s\times s} F(x) = 1 \cdot \prod _{x\in s.\mathrm{offDiag}} F(x) = \prod _{x\in s.\mathrm{offDiag}} F(x), \]

which is exactly the desired equality.

Lemma 4 sum product eq sum offDiag of diag zero

✓

Let \(s\) be a finite set of indices in \(\iota \), and let \(F \colon \iota \times \iota \to A\) where \(A\) is an additive commutative monoid. Assume that the diagonal values are all \(0\), i.e.

\[ \forall a \in s,\quad F(a,a)=0. \]

Then the sum of \(F\) over the Cartesian product \(s\times s\) equals the sum over the off-diagonal part:

\[ \sum _{x\in s\times s} F(x) \; =\; \sum _{x\in s.\mathrm{offDiag}} F(x). \]

Proof ▶

We use the decomposition of the square into diagonal and off-diagonal parts:

\[ s\times s \; =\; s.\mathrm{diag} \, \cup \, s.\mathrm{offDiag}, \]

and these two subsets are disjoint. Hence the sum over \(s\times s\) splits as

\[ \sum _{x\in s\times s} F(x) \; =\; \left(\sum _{x\in s.\mathrm{diag}} F(x)\right) + \left(\sum _{x\in s.\mathrm{offDiag}} F(x)\right). \]

On the diagonal, we have \(F(a,a)=0\) for all \(a\in s\), so

\[ \sum _{x\in s.\mathrm{diag}} F(x) = \sum _{a\in s} F(a,a) = \sum _{a\in s} 0 = 0. \]

Therefore,

\[ \sum _{x\in s\times s} F(x) = 0 + \sum _{x\in s.\mathrm{offDiag}} F(x) = \sum _{x\in s.\mathrm{offDiag}} F(x), \]

which is exactly the desired equality.