English
Inverse on a pure tensor of a G-element and a Fin n→G yields a lifted single with base a.
Русский
Обратное на чистый тензор элемента G и функции Fin n → G даёт поднятый одиночный элемент с основанием a.
LaTeX
$$$$ (\\text{diagonalSuccIsoFree } k\, G\, n).inv.hom (\\mathrm{single} g r) = \\mathrm{lift} _ k G (\\lambda a => \\mathrm{single} (a • \\mathrm{partialProd} f) 1) g. $$$$
Lean4
/-- Given a `k`-linear `G`-representation `A`, `diagonalHomEquiv` is a `k`-linear isomorphism of
the set of representation morphisms `Hom(k[Gⁿ⁺¹], A)` with `Fun(Gⁿ, A)`. This lemma says that this
sends a morphism of representations `f : k[Gⁿ⁺¹] ⟶ A` to the function
`(g₁, ..., gₙ) ↦ f(1, g₁, g₁g₂, ..., g₁g₂...gₙ).` -/
theorem diagonalHomEquiv_apply (f : Rep.diagonal k G (n + 1) ⟶ A) (x : Fin n → G) :
diagonalHomEquiv n A f x = f.hom (Finsupp.single (Fin.partialProd x) 1) := by
simp [diagonalHomEquiv, Linear.homCongr_apply, diagonalSuccIsoFree_inv_hom_single_single (k := k)]
