English
There is a linear map from α →₀ A to Coinvariants(A ⊗ free k G α), given by mapping a finsupp to the corresponding simple tensor image.
Русский
Существует линейное отображение из α →₀ A в коинварианты (A ⊗ free k G α), отображающее простейшее тензорное вложение для базисной функции.
LaTeX
$$$finsuppToCoinvariantsTensorFree : (α \\rightarrow₀ A) \\rightarrowₗ[k] Coinvariants (A ⊗ free k G α).ρ$$$
Lean4
@[simp]
theorem coinvariantsTensorFreeToFinsupp_mk_tmul_single (x : A) (i : α) (g : G) (r : k) :
DFunLike.coe (F := (A.ρ.tprod (Representation.free k G α)).Coinvariants →ₗ[k] α →₀ A.V)
(coinvariantsTensorFreeToFinsupp A α) (Coinvariants.mk _ (x ⊗ₜ single i (single g r))) =
single i (r • A.ρ g⁻¹ x) :=
by
simp [tensorObj_def, ModuleCat.MonoidalCategory.tensorObj, coinvariantsTensorFreeToFinsupp, Coinvariants.map,
finsuppTensorRight, TensorProduct.finsuppRight]