English
The map finsuppToCoinvariantsTensorFree sends a single i x to the coinvariant class of x ⊗ single i (1).
Русский
Отображение finsuppToCoinvariantsTensorFree отправляет элемент single i x в класс коинвариантов x ⊗ single i (1).
LaTeX
$$$finsuppToCoinvariantsTensorFree\\;A\\;α\\;single\\;i\\;x = Coinvariants.mk\\_\\; (x \\otimesₜ\\; single i (single 1 1))$$$
Lean4
/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the map
`(α →₀ A) →ₗ[k] (A ⊗ (α →₀ k[G]))_G` sending `single x a ↦ ⟦a ⊗ₜ single x 1⟧.` -/
noncomputable def finsuppToCoinvariantsTensorFree : (α →₀ A) →ₗ[k] Coinvariants (A ⊗ (free k G α)).ρ :=
((coinvariantsFunctor k G).map ((finsuppTensorRight A (leftRegular k G) α)).inv).hom ∘ₗ
(coinvariantsFinsuppLEquiv _ α ≪≫ₗ lcongr (Equiv.refl α) (coinvariantsTprodLeftRegularLEquiv A.ρ)).symm.toLinearMap
