Properties of the Cartesian product of indexed sets

Question

Given the indexed sets $(X_i)_{i\in I}$, one usually defines their Cartesian product as: $$\prod_{i\in I} X_i =_\text{def}\; \left\{ f: f\in \left(\bigcup_{i\in I} X_i\right)^I \wedge\; \forall i \in I\; f(i)\in X_i\right\} \label{cart1}\tag{1}$$

For $I=\{1,2\}$, it seems natural to set: $$ X_1\times X_2 =_\text{def}\; \prod_{i\in \{1,2\}} X_i $$

Then one expects, for $I=\{1\ldots n\}$: $$\prod_{i=1}^{n} X_i = \left(\prod_{i=1}^{n-1} X_i\right) \times X_n \label{cart2}\tag{2}$$

I am unable to derive \ref{cart2}. In fact, the generic element of $ \prod\limits_{i=1}^{3} X_i $ is:

$$ \{(1, f(1)), (2, f(2)), (3, f(3))\}, \text{ where $f$ is a function in } \left(\bigcup_{i\in \{1,2,3\}} X_i\right)^{\{1,2,3\}}\;; $$

while the generic element of: $$ \left(\prod_{i=1}^{2} X_i\right) \times X_3 $$ is:

$$ \{(1, f(1)), (2, f(2))\}, \text{ where $f$ is a function in } \left( \left(\prod_{i=1}^{2} X_i\right) \cup X_3\right)^{\{1,2\}}\;. $$

So: $$ \prod_{i=1}^{3} X_i \neq \left(\prod_{i=1}^{2} X_i\right) \times X_3 \label{cart3}\tag{3} $$

If that is correct, it extends to the Cartesian power: $$ X^{n+1} = X^{n} \times X $$

If \ref{cart3} is wrong, please, tell me how to prove the equality.
If \ref{cart3} is correct, can we properly define \ref{cart1} a Cartesian product, given that the standard/expected Cartesian product properties are missing?

UPDATE

The point of my question is:
since the infinite CP is a generalisation of the ordinary CP, for a finite index set:

$$\prod_{i\in \{1\ldots n\}} X_i = X_1\times\ldots X_n$$

In words: the finite versions of the infinite CP should work like the ordinary finite version. This might happen with a proper definition of $\times$ for the generalised CP, and apparently not mine above.

In a similar question, @StefanH, wants a CP construction which observes the following properties:

i) it is associative;

ii) $A^0 \times A^n = A^n$

iii) gives a natural choice for $A_0$.

Making the generalised $\times$ associative is the opposite of what I am looking for, because the standard finite CP is not associative. As for ii) and iii), there is no $A^0$ in the standard CP and so no standard behaviour to generalise.

As noted: if the generalised CP (as defined in $\ref{cart1}$) does not share the essential properties enjoyed by the standard CP, then the name 'generalised CP' might be a misnomer.

Answer 1

The equality $$\prod_{i=1}^{n} X_i = \left(\prod_{i=1}^{n-1} X_i\right) \times X_n$$ is simply not true in general (the counter example you provided is valid).

What people usually do is to implicitly identify those two sets using the natural bijection $F : \prod_{i=1}^{n} X_i \longrightarrow \left(\prod_{i=1}^{n-1} X_i\right) \times X_n $ defined as $$ F(f) = \left\{(1, f_{\big|\left\{ k \right\}_{k=1}^{n-1}}), (2, f(n))\right\}$$

You have exactly the same problem if you define the cartesian product as set of ordered pairs, namely it's not associative. Furthermore the ordered pairs definition and functional definition are strictly different according to the standard notion of set equality.

However for the most part this is always ignored (by abuse of notation) since those sets being isomoprphic is good enough for most people using them.

Answer 2

Note that your definition of $X_1\times X_2$ to mean $\prod_{i\in\{1,2\}} X_i$ is at odds with the usual definition in a standard development of set theory, where $$ X_1\times X_2 = \{ \langle x,y\rangle \mid x\in X_1, y\in X_2 \} $$ You may now try to fix that up by defining that $\langle x,y\rangle$ actually means the function that maps $1$ to $x$ and $2$ to $y$, such that the two definitions agree.

However, a function itself will usually have been defined as a set of ordered pairs already, so this gives us, for example $$ \langle 2,1\rangle = \{ \langle 1,2\rangle, \langle 2,1\rangle \} $$ which is ill-founded.

It's like straightening out a kink in a carpet -- you need to have one (ugly? limited?) concept of ordered pair before you can begin building a (nicer? more general?) theory of indexed products.

The best you can achieve in standard mathematics is to make each you "$=$" into a natural bijection between the sets which you'll need to keep track of.

---

There are some active research movements that seek to remedy this, or at least find a somewhat less awkward way it can play out. For example, under my imperfect understanding, the homotopy type theory program attempts a move away from strict equality into a weaker concept under which $X_1\times X_2 = \prod_{i\in\{1,2\}}X_i$ is "just as good as any other equality you should ever want to care about" because every $=$ comes with a semi-invisible bijection attached.