Tensor products with monoid algebras

This file records the standard linear identification of a tensor product with a monoid algebra as a space of finitely supported functions.

Main definitions

• TauCeti.MonoidAlgebra.tensorEquivFinsupp: the equivalence k[G] ⊗ W ≃ₗ G →₀ W.

Main results

• TauCeti.MonoidAlgebra.tensorEquivFinsupp_single_tmul and TauCeti.MonoidAlgebra.tensorEquivFinsupp_symm_single: the equivalence and its inverse on generators.

noncomputable def TauCeti.MonoidAlgebra.tensorEquivFinsupp {k : Type u} [CommSemiring k] {G : Type v} {W : Type w} [AddCommMonoid W] [Module k W] : TensorProduct k (MonoidAlgebra k G) W ≃ₗ[k] G →₀ W

The standard identification k[G] ⊗ W ≃ₗ G →₀ W.

Equations

• TauCeti.MonoidAlgebra.tensorEquivFinsupp = (TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (LinearEquiv.refl k W)).trans (TensorProduct.finsuppScalarLeft k W G)

@[simp]

theorem TauCeti.MonoidAlgebra.tensorEquivFinsupp_single_tmul {k : Type u} [CommSemiring k] {G : Type v} {W : Type w} [AddCommMonoid W] [Module k W] (g : G) (r : k) (w : W) : tensorEquivFinsupp (MonoidAlgebra.single g r ⊗ₜ[k] w) = Finsupp.single g (r • w)

The tensor/Finsupp equivalence sends a pure tensor supported at g to a Finsupp supported at g.

@[simp]

theorem TauCeti.MonoidAlgebra.tensorEquivFinsupp_symm_single {k : Type u} [CommSemiring k] {G : Type v} {W : Type w} [AddCommMonoid W] [Module k W] (g : G) (w : W) : tensorEquivFinsupp.symm (Finsupp.single g w) = MonoidAlgebra.single g 1 ⊗ₜ[k] w

The inverse of the tensor/Finsupp equivalence sends a Finsupp supported at g to a pure tensor supported at g.