[proofplan] Both isomorphisms are instances of the universal properties of the direct sum: the codomain $V_1 \oplus V_2$ has a universal property dual to that of the domain $V_1 \oplus V_2$ as a coproduct. For (1) we use the projections $\pi_i: V_1 \oplus V_2 \to V_i$ to split a homomorphism into the codomain into a pair of homomorphisms; the inverse builds a homomorphism into a direct sum from a pair of homomorphisms. For (2) we use the inclusions $\iota_i: V_i \to V_1 \oplus V_2$ to split a homomorphism out of the direct sum into a pair, with inverse using the projections. In each case both maps are $\mathbb{F}$-linear and $G$-equivariance is preserved because $\pi_i, \iota_i$ are $G$-linear. [/proofplan] [step:Set up the projections and inclusions of $V_1 \oplus V_2$] Recall the direct sum $V_1 \oplus V_2$ is the $\mathbb{F}$-vector space of pairs $(v_1, v_2)$ with $v_i \in V_i$, with $G$-action $g(v_1, v_2) := (gv_1, gv_2)$. Define the canonical $\mathbb{F}$-linear maps \begin{align*} \pi_i : V_1 \oplus V_2 &\to V_i, & (v_1, v_2) &\mapsto v_i, \\ \iota_i : V_i &\to V_1 \oplus V_2, & v_i &\mapsto (0, \ldots, v_i, \ldots, 0) \quad (\text{$v_i$ in slot $i$}), \end{align*} for $i \in \{1, 2\}$. These are $G$-equivariant by the componentwise definition of the $G$-action: $\pi_i(g(v_1, v_2)) = \pi_i(gv_1, gv_2) = gv_i = g\pi_i(v_1, v_2)$, and $\iota_1(gv_1) = (gv_1, 0) = (gv_1, g \cdot 0) = g(v_1, 0) = g\iota_1(v_1)$ (similarly for $\iota_2$). The projections and inclusions satisfy \begin{align*} \pi_i \iota_i = \iota_{V_i}, \quad \pi_i \iota_j = 0 \text{ for } i \neq j, \quad \iota_1 \pi_1 + \iota_2 \pi_2 = \iota_{V_1 \oplus V_2}. \end{align*} [guided] The direct sum $V_1 \oplus V_2$ comes equipped with both projections and inclusions, all of them $G$-linear because the $G$-action on $V_1 \oplus V_2$ is defined componentwise. The relations $\pi_i \iota_j = \delta_{ij} \iota_{V_i}$ and $\sum \iota_i \pi_i = \iota_{V_1 \oplus V_2}$ are the defining algebraic identities of a direct sum. They will be used repeatedly to verify that the maps we construct are mutual inverses. Both isomorphisms (1) and (2) come from the same package — the universal property of the biproduct — but applied in different directions. (1) uses projections from the codomain; (2) uses projections (or, more directly, restrictions to the inclusions) from the domain. [/guided] [/step] [step:Construct the isomorphism for $\operatorname{Hom}_G(V, V_1 \oplus V_2)$] Define \begin{align*} \Phi_1 : \operatorname{Hom}_G(V, V_1 \oplus V_2) &\to \operatorname{Hom}_G(V, V_1) \oplus \operatorname{Hom}_G(V, V_2) \\ \varphi &\mapsto (\pi_1 \varphi, \pi_2 \varphi). \end{align*} **$\Phi_1$ is well-defined.** Each component $\pi_i \varphi$ is the composition of two $G$-linear maps ($\varphi$ is $G$-linear by hypothesis, $\pi_i$ is $G$-linear by the previous step), hence $G$-linear: $\pi_i \varphi \in \operatorname{Hom}_G(V, V_i)$. **$\Phi_1$ is $\mathbb{F}$-linear.** For $\varphi, \varphi' \in \operatorname{Hom}_G(V, V_1 \oplus V_2)$ and $\alpha, \beta \in \mathbb{F}$, $\pi_i (\alpha \varphi + \beta \varphi') = \alpha \pi_i \varphi + \beta \pi_i \varphi'$ by linearity of composition. Define the candidate inverse \begin{align*} \Psi_1 : \operatorname{Hom}_G(V, V_1) \oplus \operatorname{Hom}_G(V, V_2) &\to \operatorname{Hom}_G(V, V_1 \oplus V_2) \\ (\psi_1, \psi_2) &\mapsto \iota_1 \psi_1 + \iota_2 \psi_2. \end{align*} **$\Psi_1$ is well-defined.** For each $v \in V$, $(\iota_1 \psi_1 + \iota_2 \psi_2)(v) = (\psi_1(v), \psi_2(v)) \in V_1 \oplus V_2$, and the resulting map is $\mathbb{F}$-linear and $G$-linear by linearity and $G$-equivariance of each summand. **$\Phi_1$ and $\Psi_1$ are mutually inverse.** Using the relations from the previous step: \begin{align*} (\Phi_1 \circ \Psi_1)(\psi_1, \psi_2) &= (\pi_1(\iota_1 \psi_1 + \iota_2 \psi_2), \pi_2(\iota_1 \psi_1 + \iota_2 \psi_2)) \\ &= (\pi_1 \iota_1 \psi_1 + \pi_1 \iota_2 \psi_2, \pi_2 \iota_1 \psi_1 + \pi_2 \iota_2 \psi_2) \\ &= (\psi_1 + 0, 0 + \psi_2) = (\psi_1, \psi_2), \end{align*} and \begin{align*} (\Psi_1 \circ \Phi_1)(\varphi) = \iota_1 \pi_1 \varphi + \iota_2 \pi_2 \varphi = (\iota_1 \pi_1 + \iota_2 \pi_2)\varphi = \iota_{V_1 \oplus V_2} \varphi = \varphi. \end{align*} Hence $\Phi_1$ is an $\mathbb{F}$-linear bijection, i.e., an $\mathbb{F}$-linear isomorphism, between $\operatorname{Hom}_G(V, V_1 \oplus V_2)$ and $\operatorname{Hom}_G(V, V_1) \oplus \operatorname{Hom}_G(V, V_2)$, proving (1). [guided] **Setup of the forward map.** A $G$-homomorphism $\varphi: V \to V_1 \oplus V_2$ has two coordinate components $\pi_1 \varphi: V \to V_1$ and $\pi_2 \varphi: V \to V_2$. Both are $G$-linear: $\varphi$ is by hypothesis, and $\pi_i$ is by the componentwise $G$-action. Thus $\Phi_1: \varphi \mapsto (\pi_1 \varphi, \pi_2 \varphi)$ is well-defined into the right target. **Setup of the candidate inverse.** Going backwards, given $(\psi_1, \psi_2)$, build a map into $V_1 \oplus V_2$ by sending $v$ to the pair $(\psi_1(v), \psi_2(v))$ — this is exactly $\iota_1 \psi_1(v) + \iota_2 \psi_2(v)$. This map is $G$-linear because each summand is. **Mutual inversion.** Compute $\Phi_1 \circ \Psi_1$: \begin{align*} \Phi_1 \Psi_1(\psi_1, \psi_2) = (\pi_1 \iota_1 \psi_1 + \pi_1 \iota_2 \psi_2,\, \pi_2 \iota_1 \psi_1 + \pi_2 \iota_2 \psi_2) = (\psi_1, \psi_2), \end{align*} using $\pi_i \iota_j = \delta_{ij} \iota_{V_i}$. Compute $\Psi_1 \circ \Phi_1$: \begin{align*} \Psi_1 \Phi_1(\varphi) = \iota_1 \pi_1 \varphi + \iota_2 \pi_2 \varphi = (\iota_1 \pi_1 + \iota_2 \pi_2)\varphi = \varphi, \end{align*} using $\iota_1 \pi_1 + \iota_2 \pi_2 = \iota_{V_1 \oplus V_2}$. Both compositions are the identity, so $\Phi_1$ is a bijection. Linearity over $\mathbb{F}$ on both sides means $\Phi_1$ is an $\mathbb{F}$-linear isomorphism. This establishes (1). [/guided] [/step] [step:Construct the isomorphism for $\operatorname{Hom}_G(V_1 \oplus V_2, V)$] Define \begin{align*} \Phi_2 : \operatorname{Hom}_G(V_1 \oplus V_2, V) &\to \operatorname{Hom}_G(V_1, V) \oplus \operatorname{Hom}_G(V_2, V) \\ \varphi &\mapsto (\varphi \iota_1, \varphi \iota_2), \end{align*} i.e., $\varphi \mapsto (\varphi|_{V_1}, \varphi|_{V_2})$ once we identify $V_i$ with its image $\iota_i(V_i) \subseteq V_1 \oplus V_2$. **$\Phi_2$ is well-defined.** Each component $\varphi \iota_i$ is the composition of $G$-linear maps, hence $G$-linear: $\varphi \iota_i \in \operatorname{Hom}_G(V_i, V)$. $\mathbb{F}$-linearity of $\Phi_2$ follows from linearity of composition. Define the candidate inverse \begin{align*} \Psi_2 : \operatorname{Hom}_G(V_1, V) \oplus \operatorname{Hom}_G(V_2, V) &\to \operatorname{Hom}_G(V_1 \oplus V_2, V) \\ (\psi_1, \psi_2) &\mapsto \psi_1 \pi_1 + \psi_2 \pi_2. \end{align*} **$\Psi_2$ is well-defined.** For $(v_1, v_2) \in V_1 \oplus V_2$, $(\psi_1 \pi_1 + \psi_2 \pi_2)(v_1, v_2) = \psi_1(v_1) + \psi_2(v_2) \in V$, an $\mathbb{F}$-linear and $G$-linear function of the input. **$\Phi_2$ and $\Psi_2$ are mutually inverse.** Using $\pi_i \iota_j = \delta_{ij} \iota_{V_i}$: \begin{align*} (\Phi_2 \circ \Psi_2)(\psi_1, \psi_2) &= ((\psi_1 \pi_1 + \psi_2 \pi_2)\iota_1, (\psi_1 \pi_1 + \psi_2 \pi_2)\iota_2) \\ &= (\psi_1 \pi_1 \iota_1 + \psi_2 \pi_2 \iota_1, \psi_1 \pi_1 \iota_2 + \psi_2 \pi_2 \iota_2) \\ &= (\psi_1 + 0, 0 + \psi_2) = (\psi_1, \psi_2), \end{align*} and using $\iota_1 \pi_1 + \iota_2 \pi_2 = \iota_{V_1 \oplus V_2}$: \begin{align*} (\Psi_2 \circ \Phi_2)(\varphi) = \varphi \iota_1 \pi_1 + \varphi \iota_2 \pi_2 = \varphi(\iota_1 \pi_1 + \iota_2 \pi_2) = \varphi \iota_{V_1 \oplus V_2} = \varphi. \end{align*} Hence $\Phi_2$ is an $\mathbb{F}$-linear isomorphism, proving (2). This completes the proof. [guided] **Setup of the forward map.** A $G$-homomorphism out of a direct sum $\varphi: V_1 \oplus V_2 \to V$ has two natural restrictions: $\varphi \iota_i: V_i \to V$ obtained by precomposing with the inclusion of the $i$th summand. Both are $G$-linear. Thus $\Phi_2: \varphi \mapsto (\varphi \iota_1, \varphi \iota_2)$ is well-defined. **Setup of the candidate inverse.** Going backwards, given $(\psi_1, \psi_2)$, build a map from $V_1 \oplus V_2$ to $V$ by sending $(v_1, v_2)$ to $\psi_1(v_1) + \psi_2(v_2)$, i.e., $(\psi_1 \pi_1 + \psi_2 \pi_2)(v_1, v_2)$. This is $G$-linear because each summand is. **Mutual inversion.** The verifications use exactly the same identities as in Step 2, with the roles of $\pi$ and $\iota$ swapped (now $\pi$ is on the right of the composition, $\iota$ on the left of $\varphi$). Compute $\Phi_2 \circ \Psi_2$: \begin{align*} \Phi_2 \Psi_2(\psi_1, \psi_2) = ((\psi_1 \pi_1 + \psi_2 \pi_2)\iota_1, (\psi_1 \pi_1 + \psi_2 \pi_2)\iota_2) = (\psi_1, \psi_2), \end{align*} using $\pi_i \iota_j = \delta_{ij} \iota_{V_i}$. Compute $\Psi_2 \circ \Phi_2$: \begin{align*} \Psi_2 \Phi_2(\varphi) = (\varphi \iota_1)\pi_1 + (\varphi \iota_2)\pi_2 = \varphi (\iota_1 \pi_1 + \iota_2 \pi_2) = \varphi. \end{align*} **Why the two parts are dual.** Part (1) uses the universal property of the direct sum **as a product**: morphisms into the product are pairs of morphisms into the factors. Part (2) uses the same direct sum **as a coproduct**: morphisms out of the coproduct are pairs of morphisms out of the summands. In the category of $\mathbb{F}[G]$-modules (or $G$-vector spaces) the finite direct sum is simultaneously a product and a coproduct (a biproduct), which is why both isomorphisms hold. The relations $\pi_i \iota_j = \delta_{ij}$ and $\sum \iota_i \pi_i = \iota_{V_1 \oplus V_2}$ encode this biproduct structure. [/guided] [/step]