English
There is a canonical linear map from the coinvariants of A ⊗ free k G α to α →₀ A, given by the prescribed formula on simple tensors.
Русский
Существует каноническое линейное отображение из коинвариантов A ⊗ свободный k G α в α →₀ A, задаваемое на простых тензорах указанной формулой.
LaTeX
$$$coinvariantsTensorFreeToFinsupp : (A \\otimes \\\\mathrm{free} \\\\ k \\\\ G \\\\ α).ρ.\\text{Coinvariants} \\\\rightarrow (α \\rightarrow₀ A)$$$
Lean4
/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the map
`(A ⊗ (α →₀ k[G]))_G →ₗ[k] (α →₀ A)` sending
`⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)).` -/
noncomputable def coinvariantsTensorFreeToFinsupp : (A ⊗ free k G α).ρ.Coinvariants →ₗ[k] (α →₀ A) :=
(coinvariantsFinsuppLEquiv _ α ≪≫ₗ lcongr (Equiv.refl α) (coinvariantsTprodLeftRegularLEquiv A.ρ)).toLinearMap ∘ₗ
((coinvariantsFunctor k G).map (finsuppTensorRight A (leftRegular k G) α).hom).hom
