coinvariantsTprodLeftRegularLEquiv

English

There is a canonical linear equivalence between the coinvariants of ρ.tprod(leftRegular) and V.

Русский

Существует каноническое линейное эквивалентное отображение между когонвариантами ρ.tprod(leftRegular) и V.

LaTeX

$$coinvariantsTprodLeftRegularLEquiv : Coinvariants (ρ.tprod (leftRegular k G)) ≃ₗ[k] V$$

Lean4

/-- Given a `k`-linear `G`-representation `(V, ρ)`, this is the linear equivalence
`(V ⊗ k[G])_G ≃ₗ[k] V` sending `⟦v ⊗ single g r⟧ ↦ r • ρ(g⁻¹)(v)`. -/
@[simps! symm_apply]
noncomputable def coinvariantsTprodLeftRegularLEquiv : Coinvariants (ρ.tprod (leftRegular k G)) ≃ₗ[k] V :=
  LinearEquiv.ofLinear (ofCoinvariantsTprodLeftRegular ρ)
    (Coinvariants.mk _ ∘ₗ (TensorProduct.mk k V (G →₀ k)).flip (single 1 1)) (by ext; simp) (by ext; simp)

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