English
There is a canonical linear map from (α →₀ Coinvariants ρ) to Coinvariants (ρ.finsupp α) that sends the basis element ⟦a⟧ to ⟦v⟧ in the corresponding fiber.
Русский
Существует каноническое линейное отображение от (α →₀ Cogонвариантов ρ) к когонвариантам (ρ.finsupp α), отправляющее базисный элемент ⟦a⟧ в соответствующий элемент ⟦v⟧.
LaTeX
$$finsuppToCoinvariants : (α →₀ Coinvariants ρ) →ₗ[k] Coinvariants (ρ.finsupp α)$$
Lean4
/-- Given a `G`-representation `(V, ρ)` and a type `α`, this is the map `(α →₀ V_G) →ₗ (α →₀ V)_G`
sending `single a ⟦v⟧ ↦ ⟦single a v⟧`. -/
noncomputable def finsuppToCoinvariants : (α →₀ Coinvariants ρ) →ₗ[k] Coinvariants (ρ.finsupp α) :=
lsum (R := k) k fun a =>
Coinvariants.lift _ (Coinvariants.mk _ ∘ₗ lsingle a) fun g =>
LinearMap.ext fun x => (mk_eq_iff _).2 <| mem_ker_of_eq g (single a x) _ <| by simp
