ofCoinvariantsTprodLeftRegular — Mathlib

English

There is a canonical linear map from (α →₀ Coinvariants ρ) to Coinvariants (ρ.finsupp α) that sends the basis element ⟦a⟧ to ⟦v⟧ in the appropriate fiber.

Русский

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

LaTeX

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

Lean4

/-- Given a `k`-linear `G`-representation `V, ρ`, this is the map `(V ⊗ k[G])_G →ₗ[k] V` sending
`⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`. -/
noncomputable def ofCoinvariantsTprodLeftRegular : Coinvariants (ρ.tprod (leftRegular k G)) →ₗ[k] V :=
  Coinvariants.lift _
    (TensorProduct.lift (Finsupp.linearCombination _ fun g => ρ g⁻¹) ∘ₗ (TensorProduct.comm _ _ _).toLinearMap) fun _ =>
    by ext; simp

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