English
For g ∈ G, f: Fin n → G, and r ∈ k, the inverse applied to g ⊗ single f r is the lifted function: Finsupp.lift _ k G (fun a => single (a • partialProd f) r) g.
Русский
Для g ∈ G, f: Fin n → G и r ∈ k обратное к g ⊗ single f r даёт поднятую функцию: Finsupp.lift _ k G (fun a => single (a • partialProd f) r) g.
LaTeX
$$$$ (\\text{diagonalSuccIsoTensorTrivial } k\, G\, n)^{-1}.hom\\big( g \\otimes_{\\otimes} \\mathrm{single}(f,r) \\big) = \\mathrm{Finsupp.lift} \\_ k \\ G \\ (\\lambda a => \\mathrm{single} (a \\cdot \\mathrm{Fin.partialProd}(f)) \\, r) \\ g. $$$$
Lean4
theorem diagonalSuccIsoTensorTrivial_inv_hom_single_right (g : G →₀ k) (f : Fin n → G) (r : k) :
(diagonalSuccIsoTensorTrivial k G n).inv.hom (g ⊗ₜ single f r) =
Finsupp.lift _ k G (fun a => single (a • Fin.partialProd f) r) g :=
by
refine g.induction ?_ ?_
· simp only [TensorProduct.zero_tmul, map_zero]
· intro a b x _ _ hx
simpa [-Action.tensorObj_V, map_add, hx, TensorProduct.add_tmul] using
diagonalSuccIsoTensorTrivial_inv_hom_single_single ..
