English
The inverse of diagonal-free maps single f a to single (g • partialProd f) a.
Русский
Обратное диагонального свободного отображения переводит одиночный элемент single f a в single (g • partialProd f) a.
LaTeX
$$$$ (\\text{diagonalSuccIsoFree } k\, G\, n).inv.hom (\\mathrm{single} f (\\mathrm{single} g a)) = \\mathrm{single} (g • \\mathrm{partialProd} f) a. $$$$
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 the
inverse map sends a function `f : Gⁿ → A` to the representation morphism sending
`(g₀, ... gₙ) ↦ ρ(g₀)(f(g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ))`, where `ρ` is the representation attached
to `A`. -/
theorem diagonalHomEquiv_symm_apply (f : (Fin n → G) → A) (x : Fin (n + 1) → G) :
((diagonalHomEquiv n A).symm f).hom (Finsupp.single x 1) =
A.ρ (x 0) (f fun i : Fin n => (x (Fin.castSucc i))⁻¹ * x i.succ) :=
by simp [diagonalHomEquiv, Linear.homCongr_symm_apply, diagonalSuccIsoFree_hom_hom_single (k := k)]
