English
The image of a simple tensor class under coinvariantsTensorFreeToFinsupp is the corresponding finsupp element given by r • ρ(g⁻¹) x at index i.
Русский
Образ класса простого тензора через coinvariantsTensorFreeToFinsupp равен соответствующему элементу finsupp: на позиции i стоит r • ρ(g⁻¹) x.
LaTeX
$$$coinvariantsTensorFreeToFinsupp_mk_tmul_single\\; (x)\\; (i)\\; (g)\\; (r) = single i (r \\cdot A.ρ g^{-1} x)$$$
Lean4
/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the linear equivalence
`(A ⊗ (α →₀ k[G]))_G ≃ₗ[k] (α →₀ A)` sending
`⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)).` -/
@[simps! symm_apply]
noncomputable abbrev coinvariantsTensorFreeLEquiv : Coinvariants (A ⊗ free k G α).ρ ≃ₗ[k] (α →₀ A) :=
LinearEquiv.ofLinear (coinvariantsTensorFreeToFinsupp A α) (finsuppToCoinvariantsTensorFree A α)
(lhom_ext fun i x => by
simp [finsuppToCoinvariantsTensorFree_single i, coinvariantsTensorFreeToFinsupp_mk_tmul_single x]) <|
Coinvariants.hom_ext <|
TensorProduct.ext <|
LinearMap.ext fun a =>
lhom_ext' fun i =>
lhom_ext fun g r => by
simp [coinvariantsTensorFreeToFinsupp_mk_tmul_single a, finsuppToCoinvariantsTensorFree_single (A := A) i,
TensorProduct.smul_tmul]
