English
A fundamental equality of twofold sums over representations holds, equating two nested tensor decompositions.
Русский
Основное равенство двух свёрток по представлениям, равное двум вложенным распаковкам тензорного произведения.
LaTeX
$$$\\sum_{i \\in \\mathrm{repr}.index} \\sum_{j \\in (a_2 i).index} f(\\mathrm{repr.left}(i)) \\otimes (g((a_2 i).left(j)) \\otimes h((a_2 i).right(j))) = \\sum_{i \\in \\mathrm{repr}.index} \\sum_{j \\in (a_1 i).index} f((a_1 i).left(j)) \\otimes (g((a_1 i).right(j)) \\otimes h(\\mathrm{repr.right}(i))).$$$
Lean4
theorem sum_map_tmul_tmul_eq {B : Type*} [AddCommMonoid B] [Module R B] {F : Type*} [FunLike F A B]
[LinearMapClass F R A B] (f g h : F) (a : A) {repr : Repr R a} {a₁ : (i : repr.ι) → Repr R (repr.left i)}
{a₂ : (i : repr.ι) → Repr R (repr.right i)} :
∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ (g ((a₂ i).left j) ⊗ₜ h ((a₂ i).right j)) =
∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i)) :=
by
have := sum_tmul_tmul_eq repr a₁ a₂
apply_fun TensorProduct.map (f : A →ₗ[R] B) (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this
simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_coe]
