p2m_TensorObj_p4

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

universe u v w

open BigOperators TensorProduct
open PiTensorProduct

set_option maxHeartbeats 1000000

open TensorObj

namespace TensorObj

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

private theorem mul_add_restrict_fwd (X Y Z : TensorObj K d) : Restrict (X * (Y + Z)) (X * Y + X * Z) :=
  ⟨fun i => distribLeft.symm.toLinearMap, by
    simp only [mul_t, add_t]
    -- need: liftMap distribLeft.symm ((liftMap inl) (interchange X.t Y.t) + (liftMap inr) (interchange X.t Z.t))
    --     = interchange X.t ((liftMap inl) Y.t + (liftMap inr) Z.t)
    have h1 : (fun i => (distribLeft (K := K) (M := X.V i) (N := Y.V i) (P := Z.V i)).symm.toLinearMap ∘ₗ
               LinearMap.inl K (X.V i ⊗ Y.V i) (X.V i ⊗ Z.V i)) =
              fun i => TensorProduct.map LinearMap.id (LinearMap.inl K (Y.V i) (Z.V i)) := by
      funext i; apply LinearMap.ext; intro v
      induction v using TensorProduct.induction_on with
      | zero => simp
      | tmul x y =>
        simp only [LinearMap.comp_apply, LinearMap.inl_apply, distribLeft]
        change (TensorProduct.prodRight K K (X.V i) (Y.V i) (Z.V i)).symm (x ⊗ₜ[K] y, 0) = _
        rw [show (0 : X.V i ⊗[K] Z.V i) = x ⊗ₜ[K] (0 : Z.V i) by simp,
            TensorProduct.prodRight_symm_tmul]
        simp [TensorProduct.map_tmul]
      | add a b iha ihb => simp [map_add, iha, ihb]
    have h2 : (fun i => (distribLeft (K := K) (M := X.V i) (N := Y.V i) (P := Z.V i)).symm.toLinearMap ∘ₗ
               LinearMap.inr K (X.V i ⊗ Y.V i) (X.V i ⊗ Z.V i)) =
              fun i => TensorProduct.map LinearMap.id (LinearMap.inr K (Y.V i) (Z.V i)) := by
      funext i; apply LinearMap.ext; intro v
      induction v using TensorProduct.induction_on with
      | zero => simp
      | tmul x z =>
        simp only [LinearMap.comp_apply, LinearMap.inr_apply, distribLeft]
        change (TensorProduct.prodRight K K (X.V i) (Y.V i) (Z.V i)).symm (0, x ⊗ₜ[K] z) = _
        rw [show (0 : X.V i ⊗[K] Y.V i) = x ⊗ₜ[K] (0 : Y.V i) by simp,
            TensorProduct.prodRight_symm_tmul]
        simp [TensorProduct.map_tmul]
      | add a b iha ihb => simp [map_add, iha, ihb]
    have key : (liftMap (fun i => (distribLeft (K := K) (M := X.V i) (N := Y.V i) (P := Z.V i)).symm.toLinearMap))
        ((liftMap (fun i => LinearMap.inl K (X.V i ⊗ Y.V i) (X.V i ⊗ Z.V i))) ((interchange X.t) Y.t) +
         (liftMap (fun i => LinearMap.inr K (X.V i ⊗ Y.V i) (X.V i ⊗ Z.V i))) ((interchange X.t) Z.t)) =
        (interchange X.t) ((liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i))) Y.t +
         (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i))) Z.t) := by
      rw [(liftMap _).map_add, liftMap_comp, liftMap_comp, h1, h2,
          liftMap_interchange, liftMap_interchange]
      simp only [liftMap_id, ← map_add]
    exact key⟩

-- Restrict (X*Y+X*Z) (X*(Y+Z)): f : (X*(Y+Z)).V i →ₗ (X*Y+X*Z).V i = distribLeft
-- liftMap distribLeft (interchange X.t (Y+Z).t) = (X*Y+X*Z).t
theorem mul_add_isomorphic {X Y Z : TensorObj K d} :
    Restrict (X * (Y + Z)) (X * Y + X * Z) ∧ Restrict (X * Y + X * Z) (X * (Y + Z)) :=
  ⟨mul_add_restrict_fwd X Y Z,
   ⟨fun i => distribLeft.toLinearMap, by
    change liftMap (fun i => distribLeft.toLinearMap) (interchange X.t (Y + Z).t) = (X * Y + X * Z).t
    change liftMap (fun i => distribLeft.toLinearMap) (interchange X.t (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) Y.t + liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) Z.t)) = _
    rw [map_add, map_add]
    congr 1
    · have h1 : interchange X.t (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) Y.t) =
                liftMap (fun i => TensorProduct.map LinearMap.id (LinearMap.inl K (Y.V i) (Z.V i))) (interchange X.t Y.t) := by
        conv_lhs => rw [← liftMap_id X]
        rw [← liftMap_interchange]
      rw [h1, liftMap_comp]
      apply congr_arg (fun h => liftMap h _)
      funext i; apply LinearMap.ext; intro v
      simp only [LinearMap.comp_apply, distribLeft, TensorProduct.prodRight, LinearEquiv.coe_coe]
      induction v using TensorProduct.induction_on with
      | zero => simp
      | tmul x y => simp; change _ = (LinearMap.inl K (X.V i ⊗ Y.V i) (X.V i ⊗ Z.V i)) (x ⊗ₜ y); erw [LinearMap.inl_apply]
      | add a b iha ihb => simp only [map_add, iha, ihb]
    · have h1 : interchange X.t (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) Z.t) =
                liftMap (fun i => TensorProduct.map LinearMap.id (LinearMap.inr K (Y.V i) (Z.V i))) (interchange X.t Z.t) := by
        conv_lhs => rw [← liftMap_id X]
        rw [← liftMap_interchange]
      rw [h1, liftMap_comp]
      apply congr_arg (fun h => liftMap h _)
      funext i; apply LinearMap.ext; intro v
      simp only [LinearMap.comp_apply, distribLeft, TensorProduct.prodRight, LinearEquiv.coe_coe]
      induction v using TensorProduct.induction_on with
      | zero => simp
      | tmul x z => simp; change _ = (LinearMap.inr K (X.V i ⊗ Y.V i) (X.V i ⊗ Z.V i)) (x ⊗ₜ z); erw [LinearMap.inr_apply]
      | add a b iha ihb => simp only [map_add, iha, ihb]⟩⟩

theorem add_mul_isomorphic {X Y Z : TensorObj K d} :
    Restrict ((X + Y) * Z) (X * Z + Y * Z) ∧ Restrict (X * Z + Y * Z) ((X + Y) * Z) :=
  let hc1 := mul_comm_isomorphic (X := X + Y) (Y := Z)
  let hma := mul_add_isomorphic (X := Z) (Y := X) (Z := Y)
  let hcX := mul_comm_isomorphic (X := Z) (Y := X)
  let hcY := mul_comm_isomorphic (X := Z) (Y := Y)
  let hadd := add_isomorphic hcX hcY
  ⟨restrict_trans hc1.1 (restrict_trans hma.1 hadd.1),
   restrict_trans hadd.2 (restrict_trans hma.2 hc1.2)⟩

theorem zero_mul_isomorphic {X : TensorObj K d} :
    Restrict (zeroObj * X) zeroObj ∧ Restrict zeroObj (zeroObj * X) :=
  -- Both zeroObj.t and (zeroObj * X).t are 0, so liftMap of any f applied to 0 = 0
  have hzm : (zeroObj * X).t = 0 := by
    simp only [mul_t, zeroObj]
    exact (interchange (0 : PiTensorProduct K (fun _ : Fin d => PUnit))).map_zero
  ⟨⟨fun _ => 0, by simp only [show (zeroObj : TensorObj K d).t = 0 from rfl, map_zero, hzm]⟩,
   ⟨fun _ => 0, by simp only [hzm, map_zero, show (zeroObj : TensorObj K d).t = 0 from rfl]⟩⟩

end TensorObj