coinvariantsToFinsupp — Mathlib

English

There is a natural linear map from Coinvariants (ρ.finsupp α) to α-indexed coinvariants that sends the class of single a to the class of v.

Русский

Существуют естественные линейные отображения от когонвариантов (ρ.finsupp α) к когонвариантам, индексируемым α, отправляющее класс ⟦single a v⟧ в класс ⟦v⟧.

LaTeX

$$coinvariantsToFinsupp : Coinvariants (ρ.finsupp α) →ₗ[k] α →₀ Coinvariants ρ$$

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 coinvariantsToFinsupp : Coinvariants (ρ.finsupp α) →ₗ[k] α →₀ Coinvariants ρ :=
  Coinvariants.lift _ (mapRange.linearMap (Coinvariants.mk _)) <| fun _ => by ext; simp

Похожие утверждения