p2m_Tensor_quot

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

import Definitions.Def_p2m_TensorObj_p1
import Definitions.Def_p2m_TensorObj_p2
import Definitions.Def_p2m_TensorObj_p3
import Definitions.Def_p2m_TensorObj_p4

universe u v w


/-- The quotient of `TensorObj` by linear isomorphism. -/
def Tensor (K : Type u) [Field K] (d : ℕ) [Fact (1 < d)] :=
  Quotient (TensorObj.tensorSetoid.{u, max u v} K d)

namespace Tensor

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

/-- Decategorification map. -/
def toTensor (X : TensorObj.{u, max u v} K d) : Tensor.{u, v} K d :=
  Quotient.mk (tensorSetoid.{u, max u v} K d) X

/-- Zero and One objects (minimal placeholders). -/
noncomputable def zeroObj : TensorObj.{u, max u v} K d := TensorObj.zeroObj
noncomputable def oneObj : TensorObj.{u, max u v} K d := TensorObj.oneObj

noncomputable instance : Zero (Tensor.{u, v} K d) := ⟨toTensor zeroObj⟩
noncomputable instance : One (Tensor.{u, v} K d) := ⟨toTensor oneObj⟩

/-- Lift addition to the quotient. -/
noncomputable def add (x y : Tensor K d) : Tensor K d :=
  Quotient.liftOn₂ x y
    (fun X Y => toTensor (X + Y))
    (fun _ _ _ _ hab hcd => Quotient.sound (add_isomorphic hab hcd))

/-- Lift multiplication to the quotient. -/
noncomputable def mul (x y : Tensor K d) : Tensor K d :=
  Quotient.liftOn₂ x y
    (fun X Y => toTensor (X * Y))
    (fun _ _ _ _ hab hcd => Quotient.sound (mul_isomorphic hab hcd))

noncomputable instance : Add (Tensor.{u, v} K d) := ⟨add⟩
noncomputable instance : Mul (Tensor.{u, v} K d) := ⟨mul⟩

section QuotientHelpers

variable {X Y Z : TensorObj.{u, max u v} K d}

/-- Helper to lift a unary operation equality proof from TensorObj to Tensor. -/
theorem lift_unary_iso {f g : Tensor K d → Tensor K d} {F G : TensorObj K d → TensorObj K d}
    (h_lift_f : ∀ X, f (toTensor X) = toTensor (F X))
    (h_lift_g : ∀ X, g (toTensor X) = toTensor (G X))
    (h_iso : ∀ X, Restrict (F X) (G X) ∧ Restrict (G X) (F X)) : ∀ x, f x = g x := by
  intro x
  induction x using Quotient.inductionOn with | h X =>
  change f (toTensor X) = g (toTensor X)
  rw [h_lift_f, h_lift_g]
  exact Quotient.sound (h_iso X)

/-- Helper to lift a binary operation equality proof from TensorObj to Tensor. -/
theorem lift_binary_iso {f g : Tensor K d → Tensor K d → Tensor K d}
    {F G : TensorObj K d → TensorObj K d → TensorObj K d}
    (h_lift_f : ∀ X Y, f (toTensor X) (toTensor Y) = toTensor (F X Y))
    (h_lift_g : ∀ X Y, g (toTensor X) (toTensor Y) = toTensor (G X Y))
    (h_iso : ∀ X Y, Restrict (F X Y) (G X Y) ∧ Restrict (G X Y) (F X Y)) : ∀ x y, f x y = g x y := by
  intro x y
  induction x using Quotient.inductionOn with | h X =>
  induction y using Quotient.inductionOn with | h Y =>
  change f (toTensor X) (toTensor Y) = g (toTensor X) (toTensor Y)
  rw [h_lift_f, h_lift_g]
  exact Quotient.sound (h_iso X Y)

/-- Helper to lift a ternary operation equality proof from TensorObj to Tensor. -/
theorem lift_ternary_iso {f g : Tensor K d → Tensor K d → Tensor K d → Tensor K d}
    {F G : TensorObj K d → TensorObj K d → TensorObj K d → TensorObj K d}
    (h_lift_f : ∀ X Y Z, f (toTensor X) (toTensor Y) (toTensor Z) = toTensor (F X Y Z))
    (h_lift_g : ∀ X Y Z, g (toTensor X) (toTensor Y) (toTensor Z) = toTensor (G X Y Z))
    (h_iso : ∀ X Y Z, Restrict (F X Y Z) (G X Y Z) ∧ Restrict (G X Y Z) (F X Y Z)) : ∀ x y z, f x y z = g x y z := by
  intro x y z
  induction x using Quotient.inductionOn with | h X =>
  induction y using Quotient.inductionOn with | h Y =>
  induction z using Quotient.inductionOn with | h Z =>
  change f (toTensor X) (toTensor Y) (toTensor Z) = g (toTensor X) (toTensor Y) (toTensor Z)
  rw [h_lift_f, h_lift_g]
  exact Quotient.sound (h_iso X Y Z)

end QuotientHelpers

section Isomorphisms

variable {X Y Z : TensorObj.{u, max u v} K d}

theorem add_comm (x y : Tensor K d) : x + y = y + x :=
  lift_binary_iso (f := Tensor.add) (g := fun a b => b + a) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => add_comm_isomorphic) x y

theorem add_assoc (x y z : Tensor K d) : x + y + z = x + (y + z) :=
  lift_ternary_iso (f := fun a b c => a + b + c) (g := fun a b c => a + (b + c))
    (fun _ _ _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ => add_assoc_isomorphic) x y z

theorem zero_add (x : Tensor K d) : 0 + x = x :=
  lift_unary_iso (f := fun a => 0 + a) (g := id)
    (fun _ => rfl) (fun _ => rfl) (fun _ => zero_add_isomorphic) x

theorem add_zero (x : Tensor K d) : x + 0 = x :=
  lift_unary_iso (f := fun a => a + 0) (g := id)
    (fun _ => rfl) (fun _ => rfl) (fun _ => add_zero_isomorphic) x

theorem mul_comm (x y : Tensor K d) : x * y = y * x :=
  lift_binary_iso (f := Tensor.mul) (g := fun a b => b * a)
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => mul_comm_isomorphic) x y

theorem mul_assoc (x y z : Tensor K d) : x * y * z = x * (y * z) :=
  lift_ternary_iso (f := fun a b c => a * b * c) (g := fun a b c => a * (b * c))
    (fun _ _ _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ => mul_assoc_isomorphic) x y z

theorem one_mul (x : Tensor K d) : 1 * x = x :=
  lift_unary_iso (f := fun a => 1 * a) (g := id)
    (fun _ => rfl) (fun _ => rfl) (fun _ => one_mul_isomorphic) x

theorem mul_one (x : Tensor K d) : x * 1 = x :=
  lift_unary_iso (f := fun a => a * 1) (g := id)
    (fun _ => rfl) (fun _ => rfl) (fun _ => mul_one_isomorphic) x

theorem mul_add (x y z : Tensor K d) : x * (y + z) = x * y + x * z :=
  lift_ternary_iso (f := fun a b c => a * (b + c)) (g := fun a b c => a * b + a * c)
    (fun _ _ _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ => mul_add_isomorphic) x y z

theorem add_mul (x y z : Tensor K d) : (x + y) * z = x * z + y * z :=
  lift_ternary_iso (f := fun a b c => (a + b) * c) (g := fun a b c => a * c + b * c)
    (fun _ _ _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ => add_mul_isomorphic) x y z

theorem zero_mul (x : Tensor K d) : 0 * x = 0 :=
  lift_unary_iso (f := fun a => 0 * a) (g := fun _ => 0)
    (fun _ => rfl) (fun _ => rfl) (fun _ => zero_mul_isomorphic) x

theorem mul_zero (x : Tensor K d) : x * 0 = 0 :=
  by rw [mul_comm, zero_mul]

private noncomputable def natCast (n : ℕ) : Tensor K d := nsmulRec n 1

end Isomorphisms

noncomputable instance : CommSemiring (Tensor.{u, v} K d) where
  add := add
  zero := 0
  mul := mul
  one := 1
  add_assoc := add_assoc
  zero_add := zero_add
  add_zero := add_zero
  add_comm := add_comm
  mul_assoc := mul_assoc
  one_mul := one_mul
  mul_one := mul_one
  mul_comm := mul_comm
  left_distrib := mul_add
  right_distrib := add_mul
  zero_mul := zero_mul

  mul_zero := mul_zero
  nsmul := nsmulRec
  npow := npowRec
  natCast := natCast
  natCast_zero := rfl
  natCast_succ n := by
    simp only [natCast, nsmulRec, add_comm]

end Tensor