English
Given representations ρV on V and ρW on W, there is a natural representation on the direct sum V ⊕ W given by g ↦ (ρV(g), ρW(g)) acting componentwise on the pair (v,w).
Русский
Даны представления ρ_V на V и ρ_W на W; существует естественное представление на прямой сумме V ⊕ W: g действует компонентно как (ρ_V(g), ρ_W(g)) на пары (v, w).
LaTeX
$$$ (\\rho_V \\oplus \\rho_W)(g) = (\\rho_V(g), \\rho_W(g)) $ acting on (v,w) ∈ V ⊕ W by (ρ_V(g) v, ρ_W(g) w)$$
Lean4
/-- Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$
(implemented by `dualTensorHom` in `Mathlib/LinearAlgebra/Contraction.lean`).
Given representations of $G$ on $V$ and $W$,there are representations of $G$ on $V^* ⊗ W$ and on
$Hom_k(V, W)$.
This lemma says that $φ$ is $G$-linear.
-/
theorem dualTensorHom_comm (g : G) :
dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (linHom ρV ρW) g ∘ₗ dualTensorHom k V W := by ext;
simp [Module.Dual.transpose_apply]
