p2m_MM

import Mathlib.LinearAlgebra.TensorProduct.Pi
import Definitions.Def_p2m_TensorObj_p1
import Definitions.Def_p2m_TensorObj_p2
import Definitions.Def_p2m_TensorObj_p3
import Definitions.Def_p2m_TensorObj_p4
import Definitions.Def_p2m_Tensor_quot
import Definitions.Def_p2m_Restriction

universe u

open TensorObj PiTensorProduct BigOperators TensorProduct

namespace Tensor

variable {K : Type u} [Field K]

instance instFact13 : Fact (1 < 3) := ⟨by norm_num⟩

/-! ## Matrix multiplication tensors -/

/-- The three mode spaces for `MM n m p`, indexed by `Fin 3`. -/
@[reducible] private def MMSpace (K : Type u) (n m p : ℕ) : Fin 3 → Type u
  | ⟨0, _⟩ => Fin n × Fin m → K
  | ⟨1, _⟩ => Fin m × Fin p → K
  | ⟨2, _⟩ => Fin p × Fin n → K

@[reducible] private instance MMSpace_addCommGroup (n m p : ℕ) (i : Fin 3) :
    AddCommGroup (MMSpace K n m p i) :=
  match i with
  | ⟨0, _⟩ => Pi.addCommGroup
  | ⟨1, _⟩ => Pi.addCommGroup
  | ⟨2, _⟩ => Pi.addCommGroup

@[reducible] private instance MMSpace_module (n m p : ℕ) (i : Fin 3) :
    Module K (MMSpace K n m p i) :=
  match i with
  | ⟨0, _⟩ => Pi.module _ _ _
  | ⟨1, _⟩ => Pi.module _ _ _
  | ⟨2, _⟩ => Pi.module _ _ _

private instance MMSpace_finiteDimensional (n m p : ℕ) (i : Fin 3) :
    FiniteDimensional K (MMSpace K n m p i) :=
  match i with
  | ⟨0, _⟩ => inferInstance
  | ⟨1, _⟩ => inferInstance
  | ⟨2, _⟩ => inferInstance

/-- The pure tensor `e_{ij} ⊗ e_{jk} ⊗ e_{ki}` for indices `(i,j,k)`. -/
private noncomputable def MMPureTensor (n m p : ℕ) (i : Fin n) (j : Fin m) (k : Fin p) :
    PiTensorProduct K (MMSpace K n m p) :=
  tprod K (fun (s : Fin 3) =>
    match s with
    | ⟨0, _⟩ => (Pi.single (i, j) 1 : Fin n × Fin m → K)
    | ⟨1, _⟩ => (Pi.single (j, k) 1 : Fin m × Fin p → K)
    | ⟨2, _⟩ => (Pi.single (k, i) 1 : Fin p × Fin n → K))

/-- The matrix multiplication TensorObj `⟨n, m, p⟩`:
    mode spaces are `Fin n × Fin m → K`, `Fin m × Fin p → K`, `Fin p × Fin n → K`,
    with tensor element `∑ i j k, e_{ij} ⊗ e_{jk} ⊗ e_{ki}`. -/
@[reducible] noncomputable def MMObj (n m p : ℕ) : TensorObj.{u, u} K 3 where
  V := MMSpace K n m p
  addCommGroup := MMSpace_addCommGroup n m p
  module := MMSpace_module n m p
  finiteDimensional := MMSpace_finiteDimensional n m p
  t := ∑ i : Fin n, ∑ j : Fin m, ∑ k : Fin p, MMPureTensor n m p i j k

@[simp] theorem MMObj_V (n m p : ℕ) : (MMObj (K := K) n m p).V = MMSpace K n m p := rfl

@[simp] theorem MMObj_t (n m p : ℕ) : (MMObj (K := K) n m p).t =
    ∑ i : Fin n, ∑ j : Fin m, ∑ k : Fin p, MMPureTensor n m p i j k := rfl

/-- The matrix multiplication tensor `MM n m p` as an element of `Tensor K 3`. -/
noncomputable def MM (n m p : ℕ) : Tensor K 3 := toTensor (MMObj n m p)

end Tensor