English
Let f : V → W be a k-linear map between modules with a G-action that is commuting with the G-action, and assume for all g ∈ G and v ∈ V that f(g·v) = g·f(v). Then there exists a k[G]-linear map ϕ : V → W extending f, and ϕ is constructed via equivariantOfLinearOfComm. This provides a canonical extension of f to a MonoidAlgebra-linear map.
Русский
Пусть f : V → W — линейный отображение между модулями с действием G, удовлетворяющее условию: для всех g ∈ G и v ∈ V выполняется f(g·v) = g·f(v). Тогда существует линейное отображение над k[G], V → W, расширяющее f, которое строится функцией equivariantOfLinearOfComm.
LaTeX
$$$\\exists\\; \\varphi : V \\to\\_ {MonoidAlgebra k G}-linear\\, W\\;\\text{ с }\\; \\varphi|_V = f,$ \\\\ \\text{где }\\; \\varphi = \\text{equivariantOfLinearOfComm}(f,h).$$$
Lean4
/-- Build a `k[G]`-linear map from a `k`-linear map and evidence that it is `G`-equivariant. -/
def equivariantOfLinearOfComm (h : ∀ (g : G) (v : V), f (single g (1 : k) • v) = single g (1 : k) • f v) :
V →ₗ[MonoidAlgebra k G] W where
toFun := f
map_add' v v' := by simp
map_smul' c
v := by
refine Finsupp.induction c ?_ ?_
· simp
· intro g r c' _nm _nz w
dsimp at *
simp only [add_smul, f.map_add, w, single_eq_algebraMap_mul_of, ← smul_smul]
rw [algebraMap_smul (MonoidAlgebra k G) r, algebraMap_smul (MonoidAlgebra k G) r, f.map_smul, of_apply, h g v]
