p2m_TensorObj_p1

import Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.LinearAlgebra.FiniteDimensional.Basic
import Mathlib.RingTheory.TensorProduct.Finite
import Mathlib.LinearAlgebra.TensorProduct.Finiteness
import Mathlib.Logic.Basic
import Mathlib.Algebra.Module.ULift
import Mathlib.LinearAlgebra.Prod
import Mathlib.Algebra.Module.PUnit
import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.LinearAlgebra.TensorProduct.Tower

universe u v w

open BigOperators TensorProduct
open PiTensorProduct

set_option maxHeartbeats 1000000


open BigOperators TensorProduct

-- We open PiTensorProduct, but distinct names prevent clashes with the type
open PiTensorProduct

/-- `TensorObj` represents a single concrete (d)-th order tensor
  t ∈ V₁ ⊗ V₂ ⊗ ⋯ ⊗ V_d over a field K.

  Unlike a coordinate representation, this structure stores the vector spaces
  themselves and an element of their iterated tensor product.

  Arguments:
  * `K`: The base field.
  * `d`: The order of the tensor (must be greater than 1). -/
structure TensorObj (K : Type u) [Field K] (d : ℕ) [Fact (1 < d)] where
  /-- The family of vector spaces involved in the tensor product. -/
  V : Fin d → Type v
  /-- Each space must be an additive commutative group. -/
  [addCommGroup : ∀ i, AddCommGroup (V i)]
  /-- Each space must be a module over K. -/
  [module : ∀ i, Module K (V i)]
  /-- Each space must be finite-dimensional over K. -/
  [finiteDimensional : ∀ i, FiniteDimensional K (V i)]
  /-- The concrete tensor element in the iterated tensor product of the V i. -/
  t : PiTensorProduct K V

attribute [instance] TensorObj.addCommGroup TensorObj.module TensorObj.finiteDimensional

namespace TensorObj


variable {K : Type u} [Field K] {d : ℕ} [Fact (1 < d)]

noncomputable section

/-- Helper for product of LinearEquivs. -/
def prodEquiv {M M' N N' : Type*} [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid N] [AddCommMonoid N']
    [Module K M] [Module K M'] [Module K N] [Module K N']
    (e1 : M ≃ₗ[K] M') (e2 : N ≃ₗ[K] N') : (M × N) ≃ₗ[K] (M' × N') :=
  { toFun := Prod.map e1 e2
    invFun := Prod.map e1.symm e2.symm
    left_inv := fun ⟨x, y⟩ => by simp
    right_inv := fun ⟨x, y⟩ => by simp
    map_add' := fun x y => by
      cases x; cases y
      dsimp [Prod.map]
      simp only [map_add]
    map_smul' := fun c x => by
      cases x
      dsimp [Prod.map]
      simp only [map_smul] }

/-- Helper for commutativity. -/
def prodComm {M N : Type*} [AddCommMonoid M] [AddCommMonoid N] [Module K M] [Module K N] :
    (M × N) ≃ₗ[K] (N × M) :=
  { toFun := Prod.swap
    invFun := Prod.swap
    left_inv := fun ⟨x, y⟩ => by simp
    right_inv := fun ⟨x, y⟩ => by simp
    map_add' := fun x y => by simp
    map_smul' := fun c x => by simp }

/-- Helper for associativity. -/
def prodAssoc {M N P : Type*} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
    [Module K M] [Module K N] [Module K P] : ((M × N) × P) ≃ₗ[K] (M × (N × P)) :=
  { toFun := fun ⟨⟨m, n⟩, p⟩ => (m, (n, p))
    invFun := fun ⟨m, ⟨n, p⟩⟩ => ((m, n), p)
    left_inv := fun ⟨⟨m, n⟩, p⟩ => rfl
    right_inv := fun ⟨m, ⟨n, p⟩⟩ => rfl
    map_add' := fun x y => by simp
    map_smul' := fun c x => by simp }

/-- Helper for zero unit. -/
def prodZero {M : Type*} [AddCommMonoid M] [Module K M] : (PUnit × M) ≃ₗ[K] M :=
  { toFun := fun ⟨_, m⟩ => m
    invFun := fun m => (PUnit.unit, m)
    left_inv := fun ⟨u, m⟩ => by simp
    right_inv := fun m => rfl
    map_add' := fun x y => rfl
    map_smul' := fun c x => rfl }

/-- Helper for ULift equivalence. -/
def uliftEquiv : ULift.{v} K ≃ₗ[K] K :=
  { toFun := ULift.down
    invFun := ULift.up
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

/-- Helper for tensor unit. -/
def tensorOne {V : Type*} [AddCommGroup V] [Module K V] : (ULift.{v} K) ⊗[K] V ≃ₗ[K] V :=
  LinearEquiv.trans (TensorProduct.congr (uliftEquiv) (LinearEquiv.refl K V)) (TensorProduct.lid K V)

/-- Helper for tensor zero. -/
def tensorZero {V : Type*} [AddCommGroup V] [Module K V] : PUnit ⊗[K] V ≃ₗ[K] PUnit :=
  { toFun := fun _ => PUnit.unit
    invFun := fun _ => 0
    left_inv := fun x => by
       -- 0 ⊗ v = 0 = PUnit.unit from iso perspective?
       -- x : PUnit ⊗ V. PUnit is zero module. x=0.
       rw [Subsingleton.elim x 0]

    right_inv := fun x => rfl
    map_add' := fun x y => rfl
    map_smul' := fun c x => rfl }

/-- Helper for left distributivity: M ⊗ (N × P) ≃ (M ⊗ N) × (M ⊗ P). -/
def distribLeft {M N P : Type*} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
    [Module K M] [Module K N] [Module K P] : M ⊗[K] (N × P) ≃ₗ[K] (M ⊗[K] N) × (M ⊗[K] P) :=
  TensorProduct.prodRight K K M N P

/-- Helper for right distributivity: (N × P) ⊗ M ≃ (N ⊗ M) × (P ⊗ M). -/
def distribRight {M N P : Type*} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P]
    [Module K M] [Module K N] [Module K P] : (N × P) ⊗[K] M ≃ₗ[K] (N ⊗[K] M) × (P ⊗[K] M) :=
  TensorProduct.prodLeft K K N P M

/-- Functoriality of PiTensorProduct: a family of linear maps induces a map on the tensor product.
    Renamed to `liftMap` to avoid namespace conflicts. -/
def liftMap {ι : Type*} [Fintype ι] {V W : ι → Type*}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
    (f : ∀ i, V i →ₗ[K] W i) : PiTensorProduct K V →ₗ[K] PiTensorProduct K W :=
  lift <| (tprod K).compLinearMap f

/-- Functoriality of PiTensorProduct: identity map. -/
@[simp]
theorem liftMap_id (X : TensorObj K d) : liftMap (fun _ => LinearMap.id) X.t = X.t := by
  have : liftMap (fun (i : Fin d) => (LinearMap.id : X.V i →ₗ[K] X.V i)) = LinearMap.id := by
    apply PiTensorProduct.ext
    apply MultilinearMap.ext; intro v
    simp [liftMap]
  rw [this]; rfl

/-- Functoriality of PiTensorProduct: composition. -/
theorem liftMap_comp {ι : Type*} [Fintype ι] {V₁ V₂ V₃ : ι → Type*}
    [∀ i, AddCommGroup (V₁ i)] [∀ i, Module K (V₁ i)]
    [∀ i, AddCommGroup (V₂ i)] [∀ i, Module K (V₂ i)]
    [∀ i, AddCommGroup (V₃ i)] [∀ i, Module K (V₃ i)]
    (f : ∀ i, V₂ i →ₗ[K] V₃ i) (g : ∀ i, V₁ i →ₗ[K] V₂ i) (t : PiTensorProduct K V₁) :
    liftMap f (liftMap g t) = liftMap (fun i => (f i).comp (g i)) t := by
  have : liftMap f ∘ₗ liftMap g = liftMap (fun i => (f i).comp (g i)) := by
    apply PiTensorProduct.ext
    apply MultilinearMap.ext; intro v
    simp [liftMap]
  rw [← LinearMap.comp_apply, this]

/-- liftMap on a pure tensor is a pure tensor with each component mapped. -/
theorem liftMap_tprod {ι : Type*} [Fintype ι] {V W : ι → Type*}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
    (f : ∀ i, V i →ₗ[K] W i) (v : ∀ i, V i) :
    liftMap f (tprod K v) = tprod K (fun i => f i (v i)) := by
  simp only [liftMap, PiTensorProduct.lift.tprod, MultilinearMap.compLinearMap_apply]

/-- Helper to construct interchange map definition -/
def interchangeAux {ι : Type*} [Fintype ι] [DecidableEq ι] {V W : ι → Type*}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
    (v : ∀ i, V i) : MultilinearMap K W (PiTensorProduct K (fun i => V i ⊗[K] W i)) where
    toFun w := tprod K fun i => v i ⊗ₜ[K] w i
    map_update_add' w i x y := by
      -- h1: Align LHS to a Function.update that matches (tprod K).map_add input
      have h1 : (fun j => v j ⊗ₜ[K] Function.update w i (x + y) j) =
                Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] (x + y)) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      -- h2: Break down the updated value
      have h2 : Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] (x + y)) =
                Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] x + v i ⊗ₜ[K] y) := by
        simp [TensorProduct.tmul_add]

      -- h3: Align RHS term 1
      have h3 : Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] x) =
                (fun j => v j ⊗ₜ[K] Function.update w i x j) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      -- h4: Align RHS term 2
      have h4 : Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] y) =
                (fun j => v j ⊗ₜ[K] Function.update w i y j) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      calc
        (tprod K) (fun j => v j ⊗ₜ[K] (Function.update w i (x + y)) j)
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] (x + y))) := by rw [h1]
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] x + v i ⊗ₜ[K] y)) := by rw [h2]
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] x)) +
            (tprod K) (Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] y)) := by
            rw [MultilinearMap.map_update_add (tprod K) (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] x) (v i ⊗ₜ[K] y)]
        _ = (tprod K) (fun j => v j ⊗ₜ[K] (Function.update w i x) j) +
            (tprod K) (fun j => v j ⊗ₜ[K] (Function.update w i y) j) := by rw [h3, h4]

    map_update_smul' w i c x := by
      have h1 : (fun j => v j ⊗ₜ[K] Function.update w i (c • x) j) =
                Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] (c • x)) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      have h2 : Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] (c • x)) =
                Function.update (fun j => v j ⊗ₜ[K] w j) i (c • (v i ⊗ₜ[K] x)) := by
        simp [TensorProduct.tmul_smul]

      calc
        (tprod K) (fun j => v j ⊗ₜ[K] (Function.update w i (c • x)) j)
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] (c • x))) := by rw [h1]
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] w j) i (c • (v i ⊗ₜ[K] x))) := by rw [h2]
        _ = c • (tprod K) (Function.update (fun j => v j ⊗ₜ[K] w j) i (v i ⊗ₜ[K] x)) := by
            rw [MultilinearMap.map_update_smul (tprod K) (fun j => v j ⊗ₜ[K] w j) i c (v i ⊗ₜ[K] x)]
        _ = c • (tprod K) (fun j => v j ⊗ₜ[K] (Function.update w i x) j) := by
            -- Explicitly use map_smul effect on function instead of bad lemma h3
            congr 1; congr; ext j; by_cases h : j = i
            · subst h; simp
            · simp [h]

noncomputable def interchangeMap {ι : Type*} [Fintype ι] [DecidableEq ι] {V W : ι → Type*}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)] :
    MultilinearMap K V (PiTensorProduct K W →ₗ[K] PiTensorProduct K (fun i => V i ⊗[K] W i)) where
    toFun v := lift (interchangeAux v)
    map_update_add' v i x y := by
      apply _root_.PiTensorProduct.ext
      apply MultilinearMap.ext; intro m
      simp only [LinearMap.add_apply, LinearMap.compMultilinearMap_apply]

      simp only [_root_.PiTensorProduct.lift.tprod]
      dsimp [interchangeAux, MultilinearMap.coe_mk]

      have h1 : (fun j => Function.update v i (x + y) j ⊗ₜ[K] m j) =
                Function.update (fun j => v j ⊗ₜ[K] m j) i ((x + y) ⊗ₜ[K] m i) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      have h2 : Function.update (fun j => v j ⊗ₜ[K] m j) i ((x + y) ⊗ₜ[K] m i) =
                Function.update (fun j => v j ⊗ₜ[K] m j) i (x ⊗ₜ[K] m i + y ⊗ₜ[K] m i) := by
        simp [TensorProduct.add_tmul]

      have h3 : Function.update (fun j => v j ⊗ₜ[K] m j) i (x ⊗ₜ[K] m i) =
                (fun j => Function.update v i x j ⊗ₜ[K] m j) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      have h4 : Function.update (fun j => v j ⊗ₜ[K] m j) i (y ⊗ₜ[K] m i) =
                (fun j => Function.update v i y j ⊗ₜ[K] m j) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      calc
        (tprod K) (fun j => (Function.update v i (x + y)) j ⊗ₜ[K] m j)
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] m j) i ((x + y) ⊗ₜ[K] m i)) := by rw [h1]
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] m j) i (x ⊗ₜ[K] m i + y ⊗ₜ[K] m i)) := by rw [h2]
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] m j) i (x ⊗ₜ[K] m i)) +
            (tprod K) (Function.update (fun j => v j ⊗ₜ[K] m j) i (y ⊗ₜ[K] m i)) := by
            rw [MultilinearMap.map_update_add (tprod K) (fun j => v j ⊗ₜ[K] m j) i (x ⊗ₜ[K] m i) (y ⊗ₜ[K] m i)]
        _ = (tprod K) (fun j => (Function.update v i x) j ⊗ₜ[K] m j) +
            (tprod K) (fun j => (Function.update v i y) j ⊗ₜ[K] m j) := by rw [h3, h4]

    map_update_smul' v i c x := by
      apply _root_.PiTensorProduct.ext
      apply MultilinearMap.ext; intro m
      simp only [LinearMap.smul_apply, LinearMap.compMultilinearMap_apply]

      simp only [_root_.PiTensorProduct.lift.tprod]
      dsimp [interchangeAux, MultilinearMap.coe_mk]

      have h1 : (fun j => Function.update v i (c • x) j ⊗ₜ[K] m j) =
                Function.update (fun j => v j ⊗ₜ[K] m j) i ((c • x) ⊗ₜ[K] m i) := by
        ext j; by_cases h : j = i
        · subst h; simp
        · simp [h]

      have h2 : Function.update (fun j => v j ⊗ₜ[K] m j) i ((c • x) ⊗ₜ[K] m i) =
                Function.update (fun j => v j ⊗ₜ[K] m j) i (c • (x ⊗ₜ[K] m i)) := by
         simp [TensorProduct.smul_tmul]

      calc
        (tprod K) (fun j => (Function.update v i (c • x)) j ⊗ₜ[K] m j)
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] m j) i ((c • x) ⊗ₜ[K] m i)) := by rw [h1]
        _ = (tprod K) (Function.update (fun j => v j ⊗ₜ[K] m j) i (c • (x ⊗ₜ[K] m i))) := by rw [h2]
        _ = c • (tprod K) (Function.update (fun j => v j ⊗ₜ[K] m j) i (x ⊗ₜ[K] m i)) := by
            rw [MultilinearMap.map_update_smul (tprod K) (fun j => v j ⊗ₜ[K] m j) i c (x ⊗ₜ[K] m i)]
        _ = c • (tprod K) (fun j => (Function.update v i x) j ⊗ₜ[K] m j) := by
            congr 1; congr; ext j; by_cases h : j = i
            · subst h; simp
            · simp [h]


def interchange {ι : Type*} [Fintype ι] [DecidableEq ι] {V W : ι → Type*}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)] :
    PiTensorProduct K V →ₗ[K] PiTensorProduct K W →ₗ[K] PiTensorProduct K (fun i => V i ⊗[K] W i) :=
  lift interchangeMap

/-- Naturality of the interchange map. -/
@[simp]
theorem liftMap_interchange {ι : Type*} [Fintype ι] [DecidableEq ι]
    {V₁ V₂ V₃ V₄ : ι → Type*}
    [∀ i, AddCommGroup (V₁ i)] [∀ i, Module K (V₁ i)]
    [∀ i, AddCommGroup (V₂ i)] [∀ i, Module K (V₂ i)]
    [∀ i, AddCommGroup (V₃ i)] [∀ i, Module K (V₃ i)]
    [∀ i, AddCommGroup (V₄ i)] [∀ i, Module K (V₄ i)]
    (f : ∀ i, V₁ i →ₗ[K] V₃ i) (g : ∀ i, V₂ i →ₗ[K] V₄ i)
    (t₁ : PiTensorProduct K V₁) (t₂ : PiTensorProduct K V₂) :
    liftMap (fun i => TensorProduct.map (f i) (g i)) (interchange t₁ t₂) =
    interchange (liftMap f t₁) (liftMap g t₂) := by
  induction t₁ using PiTensorProduct.induction_on with
  | smul_tprod c v =>
    simp only [map_smul]
    induction t₂ using PiTensorProduct.induction_on with
    | smul_tprod c' v' =>
      simp only [map_smul]
      simp only [interchange, interchangeMap, liftMap, interchangeAux]
      simp [TensorProduct.map_tmul]
    | add x y ih1 ih2 =>
      simp only [map_add, ih1, ih2]
  | add x y ih1 ih2 =>
    simp only [map_add, LinearMap.add_apply, ih1, ih2]

/-- interchange on pure tensors gives a pure tensor of tensor products. -/
theorem interchange_tprod_K {ι : Type*} [Fintype ι] [DecidableEq ι] {V W : ι → Type*}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
    (v : ∀ i, V i) (w : ∀ i, W i) :
    interchange (tprod K v) (tprod K w) = tprod K (fun i => v i ⊗ₜ[K] w i) := by
  dsimp [interchange]
  rw [PiTensorProduct.lift.tprod]
  dsimp [interchangeMap]
  rw [PiTensorProduct.lift.tprod]
  rfl

/-- Direct sum of two tensor objects. -/
def add (X Y : TensorObj K d) : TensorObj K d where
  V := fun i => X.V i × Y.V i
  t := liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) X.t +
       liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) Y.t

/-- Tensor product of two tensor objects. -/
def mul (X Y : TensorObj K d) : TensorObj K d where
  V := fun i => X.V i ⊗[K] Y.V i
  t := interchange X.t Y.t

instance : Add (TensorObj K d) := ⟨add⟩
instance : Mul (TensorObj K d) := ⟨mul⟩

@[simp] theorem add_t (X Y : TensorObj K d) : (X + Y).t =
    liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) X.t +
    liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) Y.t := rfl

@[simp] theorem mul_t (X Y : TensorObj K d) : (X * Y).t = interchange X.t Y.t := rfl

end

end TensorObj

namespace TensorObj

variable {K : Type u} [Field K] {d : ℕ} [Fact (1 < d)]

/-- X is a restriction of Y (X ≤ Y) if there exists a family of linear maps f_i : Y.V_i → X.V_i
    such that the induced map on the tensor product sends Y.t to X.t. -/
def Restrict (X Y : TensorObj K d) : Prop :=
  ∃ f : ∀ i, Y.V i →ₗ[K] X.V i, liftMap f Y.t = X.t

theorem restrict_refl (X : TensorObj K d) : Restrict X X :=
  ⟨fun _ => LinearMap.id, liftMap_id X⟩

theorem restrict_trans {X Y Z : TensorObj K d} : Restrict X Y → Restrict Y Z → Restrict X Z := by
  rintro ⟨f, hf⟩ ⟨g, hg⟩
  exact ⟨fun i => (f i).comp (g i), by rw [← liftMap_comp, hg, hf]⟩

end TensorObj

/-- An isomorphism between two `TensorObj` K d consists of:
    1. A family of linear equivalences `equiv : X.V i ≃ₗ[K] Y.V i` for each `i`.
    2. A compatibility condition `map_t` stating that the induced map on the tensor product
       sends `X.t` to `Y.t`. -/
structure TensorIso {K : Type u} [Field K] {d : ℕ} [Fact (1 < d)]
    (X Y : TensorObj K d) where
  equiv : ∀ i : Fin d, X.V i ≃ₗ[K] Y.V i
  /-- The induced map on the tensor product must send X.t to Y.t. -/
  map_t : TensorObj.liftMap (fun i => (equiv i).toLinearMap) X.t = Y.t

namespace TensorObj

variable {K : Type u} [Field K] {d : ℕ} [Fact (1 < d)]

/-- The zero tensor object. -/
noncomputable def zeroObj : TensorObj.{u, v} K d where
  V := fun _ => PUnit
  t := 0

/-- The unit tensor object (1 ⊗ ⋯ ⊗ 1). -/
noncomputable def oneObj : TensorObj.{u, max u v} K d where
  V := fun _ => ULift.{v} K
  t := tprod K (fun _ => ULift.up 1)

/-- The equivalence relation: two tensor objects are isomorphic if there exists a `TensorIso`. -/
def Isomorphic (X Y : TensorObj K d) : Prop := Nonempty (TensorIso X Y)

/-- The isomorphism relation is an equivalence relation. -/
private theorem isomorphic_refl (X : TensorObj K d) : Isomorphic X X := by
  refine ⟨{ equiv := fun i => LinearEquiv.refl _ _, map_t := ?_ }⟩
  simp only [LinearEquiv.refl_toLinearMap]
  exact liftMap_id X

private theorem isomorphic_symm {X Y : TensorObj K d} : Isomorphic X Y → Isomorphic Y X := by
  rintro ⟨iso⟩
  refine ⟨{ equiv := fun i => (iso.equiv i).symm, map_t := ?_ }⟩
  rw [← iso.map_t, liftMap_comp]
  convert liftMap_id X using 2
  apply PiTensorProduct.ext
  apply MultilinearMap.ext; intro v
  simp

private theorem isomorphic_trans {X Y Z : TensorObj K d} : Isomorphic X Y → Isomorphic Y Z → Isomorphic X Z := by
  rintro ⟨iXY⟩ ⟨iYZ⟩
  refine ⟨{ equiv := fun i => (iXY.equiv i).trans (iYZ.equiv i), map_t := ?_ }⟩
  simp only [LinearEquiv.coe_trans]
  rw [← liftMap_comp, iXY.map_t, iYZ.map_t]

/-- The setoid structure on `TensorObj` defined by mutual restriction (X ~ Y iff X ≤ Y and Y ≤ X). -/
def tensorSetoid (K : Type u) [Field K] (d : ℕ) [Fact (1 < d)] : Setoid (TensorObj.{u, max u v} K d) where
  r X Y := TensorObj.Restrict X Y ∧ TensorObj.Restrict Y X
  iseqv := {
    refl  := fun X => ⟨restrict_refl X, restrict_refl X⟩
    symm  := fun ⟨h1, h2⟩ => ⟨h2, h1⟩
    trans := fun ⟨h1, h2⟩ ⟨h3, h4⟩ => ⟨restrict_trans h1 h3, restrict_trans h4 h2⟩
  }
end TensorObj