English
The δ transformation for the linearization is represented by the opposite of the finsupp-tensor map: (δ (linearization k G) X Y).hom = ModuleCat.ofHom (finsuppTensorFinsupp' k X.V Y.V).symm.toLinearMap.
Русский
δ-перенос линейлизации задаётся через обратное отображение finsupp-tensor: (δ (linearization k G) X Y).hom = ModuleCat.ofHom (finsuppTensorFinsupp' k X.V Y.V).symm.toLinearMap.
LaTeX
$$$(\delta (\mathrm{linearization}\ k\ G) X Y).\mathrm{hom} = \mathrm{ModuleCat}.ofHom (\mathrm{finsuppTensorFinsupp'} k X.V Y.V).\mathrm{symm}.toLinearMap$$$
Lean4
@[simp]
theorem linearization_δ_hom (X Y : Action (Type u) G) :
(δ (linearization k G) X Y).hom = ModuleCat.ofHom (finsuppTensorFinsupp' k X.V Y.V).symm.toLinearMap :=
rfl
