English
The image of a simple tensor under the hom of the left-regular trivial-tensor is the tensor of single g with a coefficient packaged as a double single.
Русский
Образ простого тензора под отображением левого регулярного тривиального тензора есть тензор из единицы на g и пары единиц на i с соответствующим коэффициентом.
LaTeX
$$$\\text{(hom of leftRegularTensorTrivialIsoFree)}( single\\ g\\ r \\otimes_{k} single\\ i\\ s ) = single\\ i (single\\ g (r s))$$$
Lean4
@[simp]
theorem leftRegularTensorTrivialIsoFree_inv_hom_single_single (i : α) (g : G) (r : k) :
DFunLike.coe (F := (α →₀ G →₀ k) →ₗ[k] ↑(ModuleCat.of k (G →₀ k) ⊗ ModuleCat.of k (α →₀ k)))
(leftRegularTensorTrivialIsoFree k G α).inv.hom.hom (single i (single g r)) =
single g r ⊗ₜ[k] single i 1 :=
by
simp [leftRegularTensorTrivialIsoFree, finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, tensorObj_def,
ModuleCat.MonoidalCategory.tensorObj]
