Exercise A0.III.6.05

Proposition

Let $R$ be a ring and let $A_1$ and $A_2$ be sets. Then

$$(R^{\oplus A_1})^{\oplus A_2} \cong R^{\oplus (A_1 \times A_2)}.$$

Proof

Note that the elements of $(R^{\oplus A_1})^{\oplus A_2}$ are finite support functions from $A_2$ to the space of finite support functions $R^{\oplus A_1}$, which contains functions from $A_1$ to $R.$

Let $f$ be any element of $R^{\oplus (A_1 \times A_2)}$ and consider the map $f' : A_2 \to R^{\oplus A_1}$ given by $a_2 \mapsto g,$ where $g : A_1 \to R$ is given by $a_1 \mapsto f (a_1, a_2).$ We’ll use $c$ to denote this procedure mapping $f$ to $f'$.

Let $h$ be any element of $(R^{\oplus A_1})^{\oplus A_2}$ and consider the map $h' : A_1 \times A_2 \to R$ given by $(a_1, a_2) \mapsto h(a_2)(a_1).$ We’ll use $u$ to denote this procedure mapping $h$ to $h'.$

We can verify that $u$ and $c$ are two-sided inverses of each other by

$$u(c(f))(a_1,a_2) = c(f)(a_2)(a_1) = f(a_1,a_2),$$

and

$$c(u(h))(a_1)(a_2) = u(h)(a_1,a_2) = h(a_2)(a_1).$$

Note also that they preserve finite support property, since they bijectively reindex a finite support function.

We’ll check that $u$ is an $R$-module homomorphism. For any $h \in (R^{\oplus A_1})^{\oplus A_2}$ and $r \in R$ note that

$$u(rh)(a_1,a_2) = (rh)(a_2)(a_1) = r \cdot h(a_2)(a_1)$$

and also, for any $h, k \in (R^{\oplus A_1})^{\oplus A_2}$ we have

$$\begin{align*}u(h+k)(a_1,a_2) &= (h+k)(a_2)(a_1) \\ &= (h(a_2)+k(a_2))(a_1) \\ &= h(a_2)(a_1)+k(a_2)(a_1).\end{align*}$$

Since $u$ is an $R$-module homomorphism with an inverse, it’s an isomorphism.

$\blacksquare$

NOTE

This is simply the curry/uncurry isomorphism.

curry :: ((a1, a2) -> r) -> (a2 -> (a1 -> r))
curry f a2 a1 = f (a1, a2)
 
uncurry :: (a2 -> (a1 -> r)) -> ((a1, a2) -> r)
uncurry f (a1, a2) = f a2 a1