English
The finsupp functor defines a representation on α →₀ A by acting pointwise: (ρ.finsupp α g)(sum i a_i δ_i) = sum i (ρ g a_i) δ_i, giving a representation on the free direct sum of copies of A indexed by α.
Русский
Функционал finsupp задаёт представление на α →₀ A, действуя по точкам: (ρ.finsupp α g)(∑ i a_i δ_i) = ∑ i (ρ(g) a_i) δ_i, образуя представление на свободном прямая сумма копий A, индексируемую α.
LaTeX
$$$ (\\rho.finsupp \\ α) (g) (\\sum_{i} a_i δ_i) = \\sum_{i} (ρ(g) a_i) δ_i $$$
Lean4
/-- The representation on `α →₀ A` defined pointwise by a representation on `A`. -/
@[simps -isSimp]
noncomputable def finsupp (α : Type*) : Representation k G (α →₀ A)
where
toFun g := lsum k fun i => (lsingle i).comp (ρ g)
map_one' := lhom_ext (fun _ _ => by simp)
map_mul' _ _ := lhom_ext (fun _ _ => by simp)
