English
For g ∈ G, f: Fin n → G, and r ∈ k, the inverse of the diagonal-tensor trivial isomorphism applied to single g r ⊗ f equals a lifted finite-supported function applied to f: Finsupp.lift ... f.
Русский
Для g ∈ G, f: Fin n → G и r ∈ k обратное диагонального тензорного тривиального изоморфа на single g r ⊗ f равно поднятой функции с опорой на f: Finsupp.lift ... f.
LaTeX
$$$$ (\\text{diagonalSuccIsoTensorTrivial } k\, G\, n)^{-1}.hom\\big(\\mathrm{single}(g,r) \\otimes_{\\otimes} f\\big) = \\mathrm{Finsupp.lift} \\, ((\\mathrm Fin (n+1) \\to G) \\to_0 k) \\\\; k \\; (\\mathrm{Fin}\\, n \\to G)\\; (\\lambda f \\; \\mapsto \\mathrm{single}(g \\cdot \\mathrm{Fin.partialProd}(f))\\; r)\\; f. $$$$
Lean4
theorem diagonalSuccIsoTensorTrivial_inv_hom_single_left (g : G) (f : (Fin n → G) →₀ k) (r : k) :
(diagonalSuccIsoTensorTrivial k G n).inv.hom (single g r ⊗ₜ f) =
Finsupp.lift ((Fin (n + 1) → G) →₀ k) k (Fin n → G) (fun f => single (g • Fin.partialProd f) r) f :=
by
refine f.induction ?_ ?_
· simp only [TensorProduct.tmul_zero, map_zero]
· intro a b x _ _ hx
simpa [-Action.tensorObj_V, TensorProduct.tmul_add, map_add, mul_comm b, hx] using
diagonalSuccIsoTensorTrivial_inv_hom_single_single ..
