n-fold tensor products

Stream: Is there code for X?

[Moritz Firsching]

I'm looking to use an $n$ fold tensor product of a finite family of finite dimensional vector spaces over a finite field.
So for a finite field $K$, and a vector space $V$ over $K$, I want to for instance be able to talk about the n-fold product $V \otimes V \otimes \dots \otimes V$ and induced maps.
Has this been done somewhere already?
My naive attempt didn't lead too far...

import Mathlib

variable (K : Type) [Field K] [Finite K]
variable (V : Type) [AddCommGroup V] [Module K V] [FiniteDimensional K V]
variable (W : Type) [AddCommGroup W] [Module K W] [FiniteDimensional K W]


open TensorProduct

theorem induced_map (φ :  V →ₗ[K] W) : ∃ φ' : V ⊗[K] V →ₗ[K] W ⊗[K] W,
  ∀ (t1 t2 : V) , φ' (t1 ⊗ₜ t2) = (φ t1) ⊗ₜ (φ t2) := by
  sorry

def nFoldTensorProduct : ℕ → Type
| 0 => PUnit
| 1 => V
| (n + 1) =>
  have : AddCommMonoid <| nFoldTensorProduct n := by sorry
  have : Module K <| nFoldTensorProduct n := by sorry
  (nFoldTensorProduct n) ⊗[K] V

def nFoldProduct (K : Type) [Field K] [Finite K]
  (V : Type) [AddCommGroup V] [Module K V] [FiniteDimensional K V] :
  (n : ℕ) → (Fin n → V) → (nFoldTensorProduct K V n)
| 0, f => _
| 1, f => (f 0 : nFoldTensorProduct K V 1)
| n + 1, f =>
  have : AddCommMonoid (nFoldTensorProduct K V n) := by sorry
  have : Module K (nFoldTensorProduct K V n) := by sorry
(((nFoldProduct K V n) (fun k => f k)) ⊗ₜ[K] (f n) : nFoldTensorProduct K V (n + 1))

[Joël Riou]

We have the tensor algebra (see the directory Mathlib.LinearAlgebra.TensorAlgebra), but I do not know whether the degree n components of this graded algebra have been identified to the n-fold tensor product...

Anyway, I would think that this should be developed in the more general context of (symmetric) monoidal categories. In that context, for any object V, V⊗V⊗⋯⊗Vshould be equipped with (n-1) transpositions (switching two consecutive V), then using a suitable presentation of the symmetric group (which we presumably do not have yet: this is basically saying that the symmetric group is a Coxeter group), we could deduce an action of the symmetric group on the n-fold tensor product. I do not think we have any of these, but this would be nice!

[Moritz Firsching]

Ah, cool, that made me also find TensorPower R n

[Eric Wieser]

We have the algebra isomorphism between the direct sum of the powers and the tensor algebra too