English
Under the diagonal successor isomorphism for the trivial tensor, a simple tensor maps to the product of the first base and a derived second base with a specified coefficient a.
Русский
При диагональном переходе в тривиальном тензоре простый тензор переходит в произведение первого базиса и производного второго базиса с заданным коэффициентом a.
LaTeX
$$$\\text{diagonalSuccIsoTensorTrivial}_{k,G,n}^{\\mathrm{hom}}(\\mathrm{single} f a) = \\mathrm{single}(f_0) \\otimes \\mathrm{single}(\\lambda i. (f(\\mathrm{castSucc} i))^{-1} * f i.\\text{succ}) a$$$
Lean4
theorem diagonalSuccIsoTensorTrivial_inv_hom_single_single (g : G) (f : Fin n → G) (a b : k) :
(diagonalSuccIsoTensorTrivial k G n).inv.hom (single g a ⊗ₜ single f b) = single (g • Fin.partialProd f) (a * b) :=
by
have := Action.diagonalSuccIsoTensorTrivial_inv_hom_apply (G := G) (n := n)
simp_all [diagonalSuccIsoTensorTrivial, ModuleCat.MonoidalCategory.tensorHom_def, tensorObj_def,
ModuleCat.MonoidalCategory.tensorObj, types_tensorObj_def, ModuleCat.hom_id (M := ((linearization k G).obj _).V),
Action.ofMulAction_V]
