p2m_Flattening_p3c

import Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.RingTheory.Flat.Basic
import Mathlib.LinearAlgebra.PiTensorProduct.Basis
import Mathlib.LinearAlgebra.Basis.VectorSpace
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Logic.Function.Basic
import Mathlib.LinearAlgebra.Dual.Lemmas
import Mathlib.LinearAlgebra.Dimension.LinearMap
import Mathlib.LinearAlgebra.Contraction
import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
import Mathlib.LinearAlgebra.Dimension.Finrank
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_Spectrum
import Definitions.Def_p2m_StrassenPreorder
import Definitions.Def_p2m_Flattening_p1
import Definitions.Def_p2m_Flattening_p2
import Definitions.Def_p2m_Flattening_p3a
import Definitions.Def_p2m_Flattening_p3b

open TensorProduct PiTensorProduct BigOperators Module

universe u v w

set_option maxHeartbeats 1000000

namespace AsymptoticSpectra.Tensor

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

/-- The multilinear map M : (∀ i, V i ⊗ W i) →ₘ (⨂V) ⊗ (⨂W) that is the left inverse
    of the interchange map. Satisfies M (fun i => v i ⊗ₜ w i) = tprod v ⊗ₜ tprod w.

    Defined via Classical.choose from the existence theorem. -/
noncomputable def piTensorDistribMultilinear {ι : 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 (fun i => V i ⊗[K] W i)
      ((PiTensorProduct K V) ⊗[K] (PiTensorProduct K W)) :=
  Classical.choose (piTensorDistribMultilinear_exists (K := K))

/-- The key property of piTensorDistribMultilinear: on pure tensor inputs,
    it produces tprod v ⊗ₜ tprod w. -/
theorem piTensorDistribMultilinear_pure {ι : 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) :
    piTensorDistribMultilinear (fun i => v i ⊗ₜ[K] w i) = tprod K v ⊗ₜ[K] tprod K w :=
  Classical.choose_spec (piTensorDistribMultilinear_exists (K := K)) v w

/-- The interchange map (lifted to tensor product) is injective. -/
theorem piTensorDistribInvFun_injective {ι : Type*} [Fintype ι] [DecidableEq ι]
    {V W : ι → Type*}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)] :
    Function.Injective (TensorProduct.lift (TensorObj.interchange (K := K) (V := V) (W := W))) := by
  induction h : Fintype.card ι using Nat.strong_induction_on generalizing ι V W with
  | _ n ih =>
    cases isEmpty_or_nonempty ι with
    | inl hι =>
      haveI : IsEmpty ι := hι
      intro x y hxy
      let eV : PiTensorProduct K V ≃ₗ[K] K := PiTensorProduct.isEmptyEquiv ι
      let eW : PiTensorProduct K W ≃ₗ[K] K := PiTensorProduct.isEmptyEquiv ι
      let eVW : PiTensorProduct K (fun i => V i ⊗[K] W i) ≃ₗ[K] K :=
        PiTensorProduct.isEmptyEquiv ι
      let eTensor : (PiTensorProduct K V) ⊗[K] (PiTensorProduct K W) ≃ₗ[K] K :=
        TensorProduct.congr eV eW ≪≫ₗ TensorProduct.lid K K
      have h1 : eTensor x = eTensor y := by
        have hcomm : ∀ t, eVW (TensorProduct.lift TensorObj.interchange t) = eTensor t := by
          intro t
          induction t using TensorProduct.induction_on with
          | zero => simp
          | tmul a b =>
            simp only [TensorProduct.lift.tmul]
            induction a using PiTensorProduct.induction_on with
            | smul_tprod c v =>
              induction b using PiTensorProduct.induction_on with
              | smul_tprod c' w =>
                simp only [map_smul, LinearMap.smul_apply]
                rw [TensorObj.interchange_tprod_K]
                simp only [smul_eq_mul]
                have heVW : eVW (tprod K fun i => v i ⊗ₜ[K] w i) = 1 :=
                  PiTensorProduct.isEmptyEquiv_apply_tprod ι _
                have heV1 : eV (tprod K v) = 1 := PiTensorProduct.isEmptyEquiv_apply_tprod ι _
                have heW1 : eW (tprod K w) = 1 := PiTensorProduct.isEmptyEquiv_apply_tprod ι _
                calc c' * (c * eVW (tprod K fun i => v i ⊗ₜ[K] w i))
                    = c' * (c * 1) := by rw [heVW]
                  _ = c * c' := by ring
                  _ = eV (c • tprod K v) * eW (c' • tprod K w) := by
                      rw [LinearEquiv.map_smul, LinearEquiv.map_smul, heV1, heW1,
                          smul_eq_mul, smul_eq_mul, mul_one, mul_one]
                  _ = eV (c • tprod K v) • eW (c' • tprod K w) := by
                      rw [smul_eq_mul]
                  _ = (TensorProduct.congr eV eW ≪≫ₗ TensorProduct.lid K K)
                        ((c • tprod K v) ⊗ₜ[K] (c' • tprod K w)) := by
                      simp only [LinearEquiv.trans_apply, TensorProduct.congr_tmul,
                        TensorProduct.lid_tmul]
              | add x y ihx ihy =>
                simp only [tmul_add, map_add]
                rw [ihx, ihy]
            | add x y ihx ihy =>
              simp only [add_tmul, map_add, LinearMap.add_apply]
              rw [ihx, ihy]
          | add x y ihx ihy => simp only [map_add, ihx, ihy]
        rw [← hcomm x, ← hcomm y, hxy]
      exact eTensor.injective h1
    | inr hι =>
      haveI : Nonempty ι := hι

      let L : PiTensorProduct K (fun i => V i ⊗[K] W i) →ₗ[K]
              (PiTensorProduct K V) ⊗[K] (PiTensorProduct K W) :=
        PiTensorProduct.lift piTensorDistribMultilinear

      apply Function.LeftInverse.injective (g := L)
      intro t

      induction t using TensorProduct.induction_on with
      | zero => simp only [map_zero]
      | tmul t₁ t₂ =>
        induction t₁ using PiTensorProduct.induction_on with
        | smul_tprod c v =>
          induction t₂ using PiTensorProduct.induction_on with
          | smul_tprod c' w =>
            simp only [TensorProduct.lift.tmul, map_smul, LinearMap.smul_apply]
            rw [TensorObj.interchange_tprod_K, PiTensorProduct.lift.tprod]
            rw [piTensorDistribMultilinear_pure]
            rw [smul_smul, mul_comm, ← smul_smul]
            rw [smul_tmul', smul_tmul]
            rfl
          | add x y ihx ihy =>
            simp only [tmul_add, map_add] at ihx ihy ⊢
            rw [ihx, ihy]
        | add x y ihx ihy =>
          simp only [add_tmul, map_add] at ihx ihy ⊢
          rw [ihx, ihy]
      | add x y ihx ihy =>
        simp only [map_add, ihx, ihy]

/-- Helper lemma: interchange is surjective onto tprod of pure tensors. -/
private theorem interchange_surj_pure {ι : 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) :
    ∃ t : (PiTensorProduct K V) ⊗[K] (PiTensorProduct K W),
      TensorProduct.lift TensorObj.interchange t = tprod K (fun i => v i ⊗ₜ[K] w i) :=
  ⟨tprod K v ⊗ₜ[K] tprod K w, by simp [TensorObj.interchange_tprod_K]⟩


end AsymptoticSpectra.Tensor