The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form

Let $S$ be a finite set, $n := \lvert S\rvert$ (The cardinality $\lvert A\rvert$ of a finite set), and let $a : S \to \mathbb{R}$ or $a : S \to \mathbb{N}$, written $a_i$ for $a(i)$. Choose a bijection $\varphi : n \to S$, which exists because $S \approx n$ (Equinumerous sets, $A \approx B$ and $A \preceq B$), and set

$\sum_{i \in S} a_i := \sum_{k<n} a_{\varphi(k)}, \qquad \prod_{i \in S} a_i := \prod_{k<n} a_{\varphi(k)},$

the right-hand sides being the iterated operations of Finite sums and finite products, by recursion when the values are real and of Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$ when they are natural.

Independence of the enumeration, which is the content of the definition. Let $\varphi, \psi : n \to S$ be two bijections. Then $\pi := \varphi^{-1} \circ \psi$ is a bijection $n \to n$ (Injection, surjection, bijection), and $a_{\psi(k)} = a_{\varphi(\pi(k))}$ for every $k < n$. Applying A finite sum is unchanged by a permutation of its index range: $\sum_{k<n} a_{\pi(k)} = \sum_{k<n} a_k$ for every bijection $\pi : n \to n$ to the list $c_k := a_{\varphi(k)}$ gives

$\sum_{k<n} a_{\psi(k)} = \sum_{k<n} c_{\pi(k)} = \sum_{k<n} c_k = \sum_{k<n} a_{\varphi(k)},$

and identically for products. So the value does not depend on which bijection is used, and $\sum_{i \in S} a_i$ is a single well-determined element.

No choice principle is involved. The definition does not select an enumeration: it asserts that all enumerations give the same value, and that value is what the notation names. Only one bijection is ever produced at a time, from a set already known to be nonempty.

Three clauses, recorded here because the page uses them constantly.

(a) The bridge to the old notation. Taking $S = n$ and $\varphi = \mathrm{id}_n$, which is legitimate since $\lvert n\rvert = n$, gives

$\sum_{i \in n} a_i = \sum_{k<n} a_k, \qquad \prod_{i \in n} a_i = \prod_{k<n} a_k .$

So the new notation extends the sum over an initial segment rather than competing with it, and every law proved for the latter is available for the former whenever the index set is a natural number.

(b) Reindexing along a bijection. If $h : T \to S$ is a bijection of finite sets, then $\sum_{j \in T} a_{h(j)} = \sum_{i \in S} a_i$, and likewise for products. Indeed $\lvert T\rvert = \lvert S\rvert = n$ by transport (The cardinality $\lvert A\rvert$ of a finite set), and if $\varphi : n \to S$ is a bijection then $h^{-1} \circ \varphi : n \to T$ is one, so $\sum_{j \in T} a_{h(j)} = \sum_{k<n} a_{h(h^{-1}(\varphi(k)))} = \sum_{k<n} a_{\varphi(k)} = \sum_{i \in S} a_i$.

(c) The empty index set and a constant summand. $\lvert\varnothing\rvert = 0$, so $\sum_{i \in \varnothing} a_i = 0$ and $\prod_{i \in \varnothing} a_i = 1$ by the base clause of the recursion. And for a constant $c$, clause (a) together with the constant clause of Laws of finite sums and products in $\mathbb{N}$, and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$ in $\mathbb{N}$, or clause 2 of Laws of finite sums and finite products in $\mathbb{R}$, gives

$\sum_{i \in S} c = \lvert S\rvert \cdot c \quad (c \in \mathbb{N}), \qquad \sum_{i \in S} c = \iota(\lvert S\rvert)\cdot c \quad (c \in \mathbb{R}),$

the second with $\iota$ written out because $\lvert S\rvert$ is a natural number and not an element of $\mathbb{R}$ (The canonical natural $\iota(n) = n \cdot 1_F$ of a field).

• This is a different object from $\sum_{k<n} a_k$, and the bridge is what keeps them one notion. The sum over an initial segment is indexed by a natural number and needs no well-definedness argument; the sum over a finite set is indexed by an arbitrary finite set and is well posed only because a finite sum is permutation invariant. Clause (a) is the statement that the second restricts to the first.

• Splitting the index set — the identity $\sum_{i \in S \cup T} a_i = \sum_{i \in S} a_i + \sum_{i \in T} a_i$ for disjoint finite $S$ and $T$, and its version for a finite partition — is not proved here but in The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition, the next item, whose splice bijection is exactly what such a proof needs. Keeping the two together avoids building the same bijection twice.

• Three notions of finite sum will exist in the library: over an initial segment (Finite sums and finite products, by recursion), over a finite index set (here), and in an arbitrary monoid (The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity ↗, later in the reading order). Each is introduced with its bridge to the previous one, which is what stops them drifting apart.