p2m_Flattening_p4

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
import Definitions.Def_p2m_Flattening_p3c

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))

/-- For any f : ∀ i, V i ⊗ W i, there exists a unique preimage under the interchange map. -/
private theorem piTensorDistribAux_exists_unique {ι : Type*} [Fintype ι] [DecidableEq ι]
    {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) :
    ∃! t : (PiTensorProduct K V) ⊗[K] (PiTensorProduct K W),
      TensorProduct.lift TensorObj.interchange t = tprod K f := by
  refine ⟨?wit, ?prop, ?unique⟩
  case wit =>
      exact Classical.epsilon (fun t => TensorProduct.lift TensorObj.interchange t = tprod K f)
  case prop =>
    have h_exists : ∃ t, TensorProduct.lift TensorObj.interchange t = tprod K f := by
      have h_surj : Function.Surjective (TensorProduct.lift
          (TensorObj.interchange (K := K) (V := V) (W := W))) := by
        rw [← LinearMap.range_eq_top, eq_top_iff]
        intro x _
        induction x using PiTensorProduct.induction_on with
        | smul_tprod c g =>
          apply Submodule.smul_mem
          have h_pure : ∀ (v : ∀ i, V i) (w : ∀ i, W i),
              tprod K (fun i => v i ⊗ₜ[K] w i) ∈ LinearMap.range (TensorProduct.lift
                (TensorObj.interchange (K := K) (V := V) (W := W))) := by
            intro v w
            exact ⟨tprod K v ⊗ₜ[K] tprod K w, by simp [TensorObj.interchange_tprod_K]⟩
          let R := LinearMap.range (TensorProduct.lift
                (TensorObj.interchange (K := K) (V := V) (W := W)))
          suffices h_main : ∀ g' : ∀ i, V i ⊗[K] W i, tprod K g' ∈ R by exact h_main g
          intro g'
          revert g'
          have h_ind : ∀ S : Finset ι, ∀ g' : ∀ i, V i ⊗[K] W i,
              (∀ i, i ∉ S → ∃ v w, g' i = v ⊗ₜ[K] w) → tprod K g' ∈ R := by
            intro S
            induction S using Finset.induction with
            | empty =>
              intro g' h_all_pure
              have h_pure_all : ∀ i, ∃ v w, g' i = v ⊗ₜ[K] w := fun i =>
                h_all_pure i (by simp)
              choose v w hg using h_pure_all
              have : g' = fun i => v i ⊗ₜ[K] w i := funext hg
              rw [this]
              exact h_pure v w
            | insert i₀ S' hi₀ ih =>
              intro g' h_pure_outside
              have h_submod : ∀ t : V i₀ ⊗[K] W i₀,
                  tprod K (Function.update g' i₀ t) ∈ R := by
                intro t
                induction t using TensorProduct.induction_on with
                | zero =>
                  convert Submodule.zero_mem R
                  have : (Function.update g' i₀ 0) i₀ = 0 := Function.update_self i₀ 0 g'
                  exact MultilinearMap.map_coord_zero (tprod K) i₀ this
                | tmul v w =>
                  apply ih
                  intro i hi_not_in_S'
                  by_cases h : i = i₀
                  · subst h
                    refine ⟨v, w, ?_⟩
                    simp only [Function.update_self]
                  · rw [Function.update_of_ne h]
                    apply h_pure_outside
                    simp only [Finset.mem_insert, not_or]
                    exact ⟨h, hi_not_in_S'⟩
                | add x y ihx ihy =>
                  have h_eq : tprod K (Function.update g' i₀ (x + y)) =
                      tprod K (Function.update g' i₀ x) +
                      tprod K (Function.update g' i₀ y) :=
                    MultilinearMap.map_update_add (tprod K) g' i₀ x y
                  rw [h_eq]
                  exact Submodule.add_mem R ihx ihy
              convert h_submod (g' i₀) using 2
              simp only [Function.update_eq_self]
          intro g'
          apply h_ind Finset.univ g'
          intro i hi
          exact absurd (Finset.mem_univ i) hi
        | add x y ihx ihy =>
          exact Submodule.add_mem _ (ihx trivial) (ihy trivial)
      exact h_surj (tprod K f)
    exact Classical.epsilon_spec h_exists
  case unique =>
    intro y hy
    have h_exists' : ∃ t, TensorProduct.lift TensorObj.interchange t = tprod K f := ⟨y, hy⟩
    have h_wit : TensorProduct.lift TensorObj.interchange
        (Classical.epsilon (fun t => TensorProduct.lift TensorObj.interchange t = tprod K f)) =
        tprod K f := Classical.epsilon_spec h_exists'
    have h_eq : TensorProduct.lift TensorObj.interchange y =
        TensorProduct.lift TensorObj.interchange
          (Classical.epsilon (fun t => TensorProduct.lift TensorObj.interchange t = tprod K f)) :=
      hy.trans h_wit.symm
    exact piTensorDistribInvFun_injective h_eq

/-- Auxiliary multilinear map for the distributivity construction.

Given a family of elements `t : ∀ i, V i ⊗[K] W i`, we want to produce an element of
`(⨂[K] i, V i) ⊗[K] (⨂[K] i, W i)`.

The map is multilinear in the sense that it's linear in each `t i` component.
On pure tensors `t i = v i ⊗ w i`, it gives `(⊗ᵢ v i) ⊗ (⊗ᵢ w i)`.

The key insight is that the map `(v, w) ↦ (tprod v) ⊗ (tprod w)` is multilinear
in both v and w. For each index i, fixing the other components, the map
`(vᵢ, wᵢ) ↦ result` is bilinear, hence factors through `Vᵢ ⊗ Wᵢ`.

The construction uses the universal property of PiTensorProduct combined with
TensorProduct.lift at each index. -/
private noncomputable def piTensorDistribAux {ι : 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)) where
  toFun f :=
    -- For f : ∀ i, V i ⊗[K] W i, we define the result as the unique preimage
    -- of tprod K f under the interchange map.
    (piTensorDistribAux_exists_unique f).choose
  map_update_add' f i x y := by
    -- We need to show linearity in the i-th slot.
    -- By uniqueness, it suffices to show that the sum of preimages maps to the
    -- sum of the tprod values.
    have h_unique_sum := (piTensorDistribAux_exists_unique (Function.update f i (x + y))).choose_spec
    have h_unique_x := (piTensorDistribAux_exists_unique (Function.update f i x)).choose_spec
    have h_unique_y := (piTensorDistribAux_exists_unique (Function.update f i y)).choose_spec
    have h_add : tprod K (Function.update f i (x + y)) =
        tprod K (Function.update f i x) + tprod K (Function.update f i y) :=
      MultilinearMap.map_update_add (tprod K) f i x y
    -- The sum of preimages maps to the sum of images
    have h_sum_maps : TensorProduct.lift TensorObj.interchange
        ((piTensorDistribAux_exists_unique (Function.update f i x)).choose +
         (piTensorDistribAux_exists_unique (Function.update f i y)).choose) =
        tprod K (Function.update f i (x + y)) := by
      rw [map_add, h_unique_x.1, h_unique_y.1, ← h_add]
    -- By uniqueness, the preimage of the sum equals the sum of preimages
    exact (piTensorDistribAux_exists_unique (Function.update f i (x + y))).unique
      h_unique_sum.1 h_sum_maps
  map_update_smul' f i c x := by
    have h_unique_smul := (piTensorDistribAux_exists_unique (Function.update f i (c • x))).choose_spec
    have h_unique_x := (piTensorDistribAux_exists_unique (Function.update f i x)).choose_spec
    have h_smul : tprod K (Function.update f i (c • x)) =
        c • tprod K (Function.update f i x) :=
      MultilinearMap.map_update_smul (tprod K) f i c x
    have h_smul_maps : TensorProduct.lift TensorObj.interchange
        (c • (piTensorDistribAux_exists_unique (Function.update f i x)).choose) =
        tprod K (Function.update f i (c • x)) := by
      rw [map_smul, h_unique_x.1, ← h_smul]
    exact (piTensorDistribAux_exists_unique (Function.update f i (c • x))).unique
      h_unique_smul.1 h_smul_maps

/-- The auxiliary multilinear map applied to pure tensors gives the expected result.

This is the defining property of `piTensorDistribAux`. The construction ensures
that this holds by definition. -/
private theorem piTensorDistribAux_apply {ι : 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) :
    piTensorDistribAux (fun i => v i ⊗ₜ[K] w i) = tprod K v ⊗ₜ[K] tprod K w := by
  -- By uniqueness, it suffices to show that tprod K v ⊗ₜ tprod K w maps to
  -- tprod K (fun i => v i ⊗ₜ w i) under the interchange map
  have h_exists := piTensorDistribAux_exists_unique (fun i => v i ⊗ₜ[K] w i)
  have h_maps : TensorProduct.lift TensorObj.interchange (tprod K v ⊗ₜ[K] tprod K w) =
      tprod K (fun i => v i ⊗ₜ[K] w i) := by
    simp only [TensorProduct.lift.tmul, TensorObj.interchange_tprod_K]
  exact h_exists.unique h_exists.choose_spec.1 h_maps

/-- The interchange map followed by piTensorDistribAux returns to tprod.

This is the key property that piTensorDistribAux is a right-inverse of the
interchange map (lifted to tensor products). -/
private theorem piTensorDistribInvFun_piTensorDistribAux {ι : Type*} [Fintype ι] [DecidableEq ι]
    {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) :
    TensorProduct.lift TensorObj.interchange (piTensorDistribAux f) = tprod K f := by
  -- This follows directly from the construction: piTensorDistribAux f is defined as
  -- the .choose of piTensorDistribAux_exists_unique, which satisfies this property
  exact (piTensorDistribAux_exists_unique f).choose_spec.1

/-- The forward direction of the distributivity map:
    `⨂[K] i, (V i ⊗ W i) → (⨂[K] i, V i) ⊗ (⨂[K] i, W i)`.

This is built using the universal property of PiTensorProduct.

The key insight is that while we can't decompose an arbitrary element of `V i ⊗ W i`,
we can use the fact that the pi-tensor product is generated by pure tensors
`⊗ᵢ (vᵢ ⊗ wᵢ)`, and these map to `(⊗ᵢ vᵢ) ⊗ (⊗ᵢ wᵢ)`.

The construction proceeds by building a multilinear map that, when all inputs
are pure tensors `vᵢ ⊗ wᵢ`, gives `(⊗ᵢ vᵢ) ⊗ (⊗ᵢ wᵢ)`. This extends by
multilinearity to all of `⨂[K] i, (V i ⊗ W i)`. -/
private noncomputable def piTensorDistribToFun {ι : 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 (fun i => V i ⊗[K] W i) →ₗ[K]
    (PiTensorProduct K V) ⊗[K] (PiTensorProduct K W) :=
  PiTensorProduct.lift piTensorDistribAux

/-- The backward direction of the distributivity map:
    `(⨂[K] i, V i) ⊗ (⨂[K] i, W i) → ⨂[K] i, (V i ⊗ W i)`.

This is the interchange map. -/
private noncomputable def piTensorDistribInvFun {ι : 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) :=
  TensorProduct.lift (TensorObj.interchange)

/-- The inverse distributivity map on pure tensors. -/
private theorem piTensorDistribInvFun_tprod {ι : 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) :
    piTensorDistribInvFun ((tprod K v) ⊗ₜ[K] (tprod K w)) = tprod K (fun i => v i ⊗ₜ[K] w i) := by
  simp only [piTensorDistribInvFun, TensorProduct.lift.tmul, TensorObj.interchange_tprod_K]

/-- The distributivity isomorphism: `⨂[K] i, (V i ⊗ W i) ≃ (⨂[K] i, V i) ⊗ (⨂[K] i, W i)`.

This isomorphism is canonical and arises from the universal property of tensor products.
It sends `⊗ᵢ (vᵢ ⊗ wᵢ)` to `(⊗ᵢ vᵢ) ⊗ (⊗ᵢ wᵢ)`.

The inverse is the interchange map. -/
noncomputable def piTensorDistrib {ι : 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 (fun i => V i ⊗[K] W i) ≃ₗ[K]
    (PiTensorProduct K V) ⊗[K] (PiTensorProduct K W) := by
  refine LinearEquiv.ofLinear piTensorDistribToFun piTensorDistribInvFun ?_ ?_
  · apply TensorProduct.ext
    apply LinearMap.ext; intro t₁
    apply LinearMap.ext; intro t₂
    change piTensorDistribToFun (piTensorDistribInvFun (t₁ ⊗ₜ[K] t₂)) = t₁ ⊗ₜ[K] 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 [piTensorDistribInvFun, TensorProduct.lift.tmul, map_smul, LinearMap.smul_apply]
        rw [TensorObj.interchange_tprod_K]
        simp only [piTensorDistribToFun, PiTensorProduct.lift.tprod]
        rw [piTensorDistribAux_apply]
        rw [smul_tmul', tmul_smul]
      | add x y ihx ihy =>
        simp only [tmul_add, map_add, ihx, ihy]
    | add x y ihx ihy =>
      simp only [add_tmul, map_add, ihx, ihy]
  · apply PiTensorProduct.ext
    apply MultilinearMap.ext; intro f
    simp only [LinearMap.compMultilinearMap_apply, LinearMap.comp_apply, LinearMap.id_apply]
    simp only [piTensorDistribToFun, PiTensorProduct.lift.tprod]
    exact piTensorDistribInvFun_piTensorDistribAux f

/-- The distributivity isomorphism applied to a pure tensor. -/
theorem piTensorDistrib_tprod {ι : 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) :
    piTensorDistrib (tprod K (fun i => v i ⊗ₜ[K] w i)) = tprod K v ⊗ₜ[K] tprod K w := by
  simp only [piTensorDistrib, LinearEquiv.ofLinear_apply, piTensorDistribToFun,
    PiTensorProduct.lift.tprod, piTensorDistribAux_apply]

/-- The interchange map followed by distributivity equals the tensor of the identity maps.

The proof uses that for pure tensors:
  `piTensorDistrib (interchange (tprod K v) (tprod K w)) = tprod K v ⊗ₜ tprod K w`
and extends by linearity. -/
theorem piTensorDistrib_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)]
    (t₁ : PiTensorProduct K V) (t₂ : PiTensorProduct K W) :
    piTensorDistrib (TensorObj.interchange t₁ t₂) = t₁ ⊗ₜ[K] t₂ := by
  induction t₁ using PiTensorProduct.induction_on with
  | smul_tprod c v =>
    induction t₂ using PiTensorProduct.induction_on with
    | smul_tprod c' w =>
      simp only [map_smul, LinearMap.smul_apply]
      rw [TensorObj.interchange_tprod_K, piTensorDistrib_tprod]
      rw [smul_tmul', tmul_smul]
    | add x y ihx ihy =>
      simp only [map_add, ihx, ihy, tmul_add]
  | add x y ihx ihy =>
    rw [map_add, LinearMap.add_apply, map_add, ihx, ihy, add_tmul]

/-- The rearrangement isomorphism for tensor products.

This isomorphism rearranges `(A ⊗ B) ⊗ (C ⊗ D)` to `(A ⊗ C) ⊗ (B ⊗ D)`.
It is built from associativity and commutativity of tensor products. -/
noncomputable def tensorFourRearrange (A B C D : Type*)
    [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B]
    [AddCommGroup C] [Module K C] [AddCommGroup D] [Module K D] :
    (A ⊗[K] B) ⊗[K] (C ⊗[K] D) ≃ₗ[K] (A ⊗[K] C) ⊗[K] (B ⊗[K] D) :=
  -- (A ⊗ B) ⊗ (C ⊗ D) → A ⊗ (B ⊗ (C ⊗ D)) → A ⊗ ((B ⊗ C) ⊗ D)
  -- → A ⊗ ((C ⊗ B) ⊗ D) → A ⊗ (C ⊗ (B ⊗ D)) → (A ⊗ C) ⊗ (B ⊗ D)
  (TensorProduct.assoc K A B (C ⊗[K] D)).trans <|
  (LinearEquiv.lTensor A (TensorProduct.assoc K B C D).symm).trans <|
  (LinearEquiv.lTensor A (LinearEquiv.rTensor D (TensorProduct.comm K B C))).trans <|
  (LinearEquiv.lTensor A (TensorProduct.assoc K C B D)).trans <|
  (TensorProduct.assoc K A C (B ⊗[K] D)).symm

@[simp]
theorem tensorFourRearrange_tmul (A B C D : Type*)
    [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B]
    [AddCommGroup C] [Module K C] [AddCommGroup D] [Module K D]
    (a : A) (b : B) (c : C) (d : D) :
    tensorFourRearrange A B C D ((a ⊗ₜ[K] b) ⊗ₜ[K] (c ⊗ₜ[K] d)) = (a ⊗ₜ[K] c) ⊗ₜ[K] (b ⊗ₜ[K] d) := by
  simp only [tensorFourRearrange, LinearEquiv.trans_apply, TensorProduct.assoc_tmul,
    LinearEquiv.lTensor_tmul, TensorProduct.assoc_symm_tmul, LinearEquiv.rTensor_tmul,
    TensorProduct.comm_tmul]
variable {V : Fin d → Type v} [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]

omit [Fact (1 < d)] in
/-- Helper lemma: splitTensorEquiv applied to a pure tensor product. -/
private theorem splitTensorEquiv_tprod (v : (i : Fin d) → V i) :
    splitTensorEquiv σ (tprod K v) =
      tprod K (fun (i : σ.S) => v i) ⊗ₜ[K] tprod K (fun (i : Sc σ) => v i) := by
  dsimp [splitTensorEquiv]
  erw [PiTensorProduct.reindex_tprod]
  simp
  erw [PiTensorProduct.tmulEquivDep_symm_apply]
  congr


omit [Fact (1 < d)] in
/-- Split tensor equiv commutes with interchange via distributivity.

This shows that splitting the product tensor `(X * Y).t = interchange X.t Y.t`
is equivalent to taking the tensor product of the splits after rearranging
via the distributivity isomorphism.

Specifically, for tensors `t₁ : ⨂[K] V` and `t₂ : ⨂[K] W`, we have:
  `splitTensorEquiv σ (interchange t₁ t₂)`
is equivalent (up to associativity and commutativity isomorphisms) to:
  `(splitTensorEquiv σ t₁) ⊗ (splitTensorEquiv σ t₂)`
after applying the distributivity isomorphisms to each factor. -/
theorem splitTensorEquiv_interchange
    {V W : Fin d → Type v}
    [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
    (t₁ : PiTensorProduct K V) (t₂ : PiTensorProduct K W) :
    splitTensorEquiv σ (TensorObj.interchange t₁ t₂) =
      TensorProduct.map piTensorDistribInvFun piTensorDistribInvFun
        (tensorFourRearrange
          (PiTensorProduct K (fun i : σ.S => V i))
          (PiTensorProduct K (fun i : Sc σ => V i))
          (PiTensorProduct K (fun i : σ.S => W i))
          (PiTensorProduct K (fun i : Sc σ => W i))
          ((splitTensorEquiv σ t₁) ⊗ₜ[K] (splitTensorEquiv σ t₂))) := by
  -- Both sides are bilinear in (t₁, t₂), so it suffices to check on pure tensors
  induction t₁ using PiTensorProduct.induction_on with
  | smul_tprod c v =>
    induction t₂ using PiTensorProduct.induction_on with
    | smul_tprod c' w =>
      simp only [map_smul, LinearMap.smul_apply]
      rw [TensorObj.interchange_tprod_K]
      rw [splitTensorEquiv_tprod]
      rw [splitTensorEquiv_tprod, splitTensorEquiv_tprod]
      simp only [smul_tmul']
      rw [tensorFourRearrange_tmul]
      rw [TensorProduct.map_tmul]
      -- LHS: (⨂ i:S, v i ⊗ w i) ⊗ (⨂ j:Sc, v j ⊗ w j)
      -- RHS: piTensorDistribInvFun ((⨂ i:S, v i) ⊗ (⨂ i:S, w i)) ⊗
      --      piTensorDistribInvFun ((⨂ j:Sc, v j) ⊗ (⨂ j:Sc, w j))
      -- Use piTensorDistribInvFun_tprod to simplify the RHS
      congr 1
      · -- Goal: c' • c • tprod ... = piTensorDistribInvFun ((c • tprod ...) ⊗ (c' • tprod ...))
        symm
        rw [TensorProduct.smul_tmul_smul, mul_smul, map_smul, map_smul,
          piTensorDistribInvFun_tprod, smul_comm]
      · -- Goal: tprod ... = piTensorDistribInvFun (tprod ... ⊗ tprod ...)
        rw [piTensorDistribInvFun_tprod]
    | add x y ihx ihy =>
      simp only [map_add, tmul_add, ihx, ihy]
  | add x y ihx ihy =>
    simp only [LinearMap.add_apply, map_add, add_tmul, ihx, ihy]

/-- The finrank of a tensor product of finite-dimensional spaces equals the product of finranks. -/
theorem finrank_tensorProduct
    {A B : Type*}
    [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B]
    [FiniteDimensional K A] [FiniteDimensional K B] :
    finrank K (A ⊗[K] B) = finrank K A * finrank K B :=
  Module.finrank_tensorProduct

/-- `tensorToDualHom` of a rearranged tensor product corresponds to the Kronecker product of
    the `tensorToDualHom`s, precomposed with the dual distribution isomorphism. -/
theorem tensorToDualHom_tensorFourRearrange {A B C D : Type*}
    [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B]
    [AddCommGroup C] [Module K C] [AddCommGroup D] [Module K D]
    [FiniteDimensional K A] [FiniteDimensional K C]
    (t1 : A ⊗[K] B) (t2 : C ⊗[K] D) :
    tensorToDualHom K (A ⊗[K] C) (B ⊗[K] D) (tensorFourRearrange A B C D (t1 ⊗ₜ[K] t2)) =
    (TensorProduct.map (tensorToDualHom K A B t1) (tensorToDualHom K C D t2)).comp
      (TensorProduct.dualDistribEquiv K A C).symm.toLinearMap := by
  induction t1 using TensorProduct.induction_on with
  | zero =>
    simp only [map_zero, tensorFourRearrange, LinearEquiv.trans_apply]
    rw [TensorProduct.zero_tmul]
    simp
  | tmul a b =>
    induction t2 using TensorProduct.induction_on with
    | zero =>
      simp only [TensorProduct.tmul_zero, map_zero, LinearMap.zero_comp,
        TensorProduct.map_zero_right]
    | tmul c d =>
      ext f
      let e := TensorProduct.dualDistribEquiv K A C
      let g := e.symm f
      have hf : f = e g := (e.apply_symm_apply f).symm
      rw [hf]
      simp only [LinearMap.comp_apply, LinearEquiv.coe_coe]
      induction g using TensorProduct.induction_on with
      | zero => simp
      | tmul u v =>
        simp only [tensorFourRearrange_tmul, tensorToDualHom_tmul, TensorProduct.dualDistribEquiv]
        have hsymm : (TensorProduct.dualDistribEquivOfBasis (Free.chooseBasis K A)
            (Free.chooseBasis K C)).symm (e (u ⊗ₜ[K] v)) = u ⊗ₜ[K] v := by
          simp only [e, TensorProduct.dualDistribEquiv, LinearEquiv.symm_apply_apply]
        rw [hsymm, TensorProduct.map_tmul, tensorToDualHom_tmul, tensorToDualHom_tmul,
          TensorProduct.smul_tmul_smul]
        -- Goal: (e (u ⊗ₜ v)) (a ⊗ₜ c) • b ⊗ₜ d = (u a * v c) • b ⊗ₜ d
        -- Show (e (u ⊗ₜ v)) (a ⊗ₜ c) = u a * v c
        have he_apply : (e (u ⊗ₜ[K] v)) (a ⊗ₜ[K] c) = u a * v c := by
          simp only [e, TensorProduct.dualDistribEquiv, TensorProduct.dualDistribEquivOfBasis,
            LinearEquiv.ofLinear_apply, TensorProduct.dualDistrib_apply]
        rw [he_apply]
      | add x y ihx ihy =>
        simp only [map_add, ihx, ihy]
    | add x y ihx ihy =>
      simp only [TensorProduct.tmul_add, map_add, ihx, ihy, TensorProduct.map_add_right,
        LinearMap.add_comp]
  | add x y ihx ihy =>
    simp only [TensorProduct.add_tmul, map_add, ihx, ihy, TensorProduct.map_add_left,
      LinearMap.add_comp]


/-- Multiplicativity of flattening rank.

The proof requires establishing:
1. `splitTensorEquiv` commutes with `interchange` via distributivity isomorphisms:
   - There exist canonical isomorphisms `⨂[K] i, (V i ⊗ W i) ≃ (⨂[K] i, V i) ⊗ (⨂[K] i, W i)`
   - These make the split of `X * Y` equivalent to a tensor product of splits

2. The flattening map factors: `flatteningMap σ (X * Y)` corresponds to the Kronecker product
   of `flatteningMap σ X` and `flatteningMap σ Y` (after the distributivity isomorphisms)

3. Rank is multiplicative for Kronecker products: `rank(A ⊗ B) = rank(A) * rank(B)`
   This is the key linear algebra fact: the range of a tensor product of linear maps
   is the tensor product of the ranges, and `finrank(U ⊗ V) = finrank(U) * finrank(V)`. -/
theorem flatteningRank_mul
    (x y : Tensor K d) :
    flatteningRank σ (x * y)
      = flatteningRank σ x
      * flatteningRank σ y := by
  induction x using Quotient.inductionOn with | _ X =>
  induction y using Quotient.inductionOn with | _ Y =>

  haveI := X.finiteDimensional
  haveI := Y.finiteDimensional

  change flatteningRank σ (Tensor.mul (Tensor.toTensor X) (Tensor.toTensor Y)) =
         flatteningRank σ (Tensor.toTensor X) * flatteningRank σ (Tensor.toTensor Y)
  simp only [Tensor.mul, flatteningRank_mk]

  let AS := PiTensorProduct K (fun i : σ.S => X.V i)
  let BS := PiTensorProduct K (fun i : Sc σ => X.V i)
  let AT := PiTensorProduct K (fun i : σ.S => Y.V i)
  let BT := PiTensorProduct K (fun i : Sc σ => Y.V i)

  -- Manually provide FiniteDimensional instances using the basis
  haveI : FiniteDimensional K AS :=
    Module.Finite.of_basis (Basis.piTensorProduct (fun i => Module.Free.chooseBasis K (X.V i)))
  haveI : FiniteDimensional K BS :=
    Module.Finite.of_basis (Basis.piTensorProduct (fun i => Module.Free.chooseBasis K (X.V i)))
  haveI : FiniteDimensional K AT :=
    Module.Finite.of_basis (Basis.piTensorProduct (fun i => Module.Free.chooseBasis K (Y.V i)))
  haveI : FiniteDimensional K BT :=
    Module.Finite.of_basis (Basis.piTensorProduct (fun i => Module.Free.chooseBasis K (Y.V i)))

  let tX := splitTensorEquiv σ X.t
  let tY := splitTensorEquiv σ Y.t

  -- The flattening map of X*Y
  let fXY := flatteningMap σ (X * Y)

  -- tXY is related to tX ⊗ tY via splitTensorEquiv_interchange
  have h_tXY_eq : splitTensorEquiv σ (TensorObj.interchange X.t Y.t) =
      TensorProduct.map
        (piTensorDistrib (K := K) (ι := σ.S)).symm.toLinearMap
        (piTensorDistrib (K := K) (ι := Sc σ)).symm.toLinearMap
        (tensorFourRearrange AS BS AT BT (tX ⊗ₜ[K] tY)) := by
    rw [splitTensorEquiv_interchange]
    rfl

  -- Now express fXY using tensorToDualHom naturality
  have h_fXY : flatteningMap σ (X * Y) =
      (piTensorDistrib (K := K)).symm.toLinearMap.comp
      ((tensorToDualHom K (AS ⊗[K] AT) (BS ⊗[K] BT)
        (tensorFourRearrange AS BS AT BT (tX ⊗ₜ[K] tY))).comp
        (piTensorDistrib (K := K)).symm.toLinearMap.dualMap) := by
      change flatteningMap σ (X * Y) = _
      dsimp [flatteningMap, TensorObj.mul]
      -- Replace splitTensorEquiv with mapped version using h_tXY_eq
      have eq1 : splitTensorEquiv σ (TensorObj.interchange X.t Y.t) =
        TensorProduct.map (piTensorDistrib (K := K) (ι := σ.S)).symm.toLinearMap
                          (piTensorDistrib (K := K) (ι := Sc σ)).symm.toLinearMap
                          (tensorFourRearrange AS BS AT BT (tX ⊗ₜ[K] tY)) := by
         rw [h_tXY_eq]
      erw [eq1]
      -- Now apply naturality
      ext phi
      -- The goal follows from tensorToDualHom_naturality:
      -- tensorToDualHom (map eA eB t) phi = eB (tensorToDualHom t (phi ∘ eA))
      -- where eA = piTensorDistrib.symm (on σ.S), eB = piTensorDistrib.symm (on Sc σ)
      -- and t = tensorFourRearrange AS BS AT BT (tX ⊗ₜ tY)
      -- Note: (X * Y).V i = X.V i ⊗ Y.V i by definition of TensorObj.mul
      simp only [HMul.hMul, Mul.mul, TensorObj.mul]
      convert tensorToDualHom_naturality K piTensorDistrib.symm piTensorDistrib.symm
        (tensorFourRearrange AS BS AT BT (tX ⊗ₜ[K] tY)) phi using 2

  -- The rest of the proof uses h_fXY to factor the flattening map and apply rank multiplicativity
  -- Key steps:
  -- 1. Use h_fXY to rewrite flatteningMap σ (X * Y)
  -- 2. Apply finrank_range_comp_equiv for the outer equivalence
  -- 3. Apply tensorToDualHom_tensorFourRearrange to factor as tensor product of maps
  -- 4. Use finrank_range_map for multiplicativity of rank under tensor products

  -- First simplify the LHS: flatteningRank σ (X * Y) = finrank K (range (flatteningMap σ (X * Y)))
  -- The quotient on the LHS simplifies to the tensor product TensorObj
  change AsymptoticSpectra.flatteningRank σ (X * Y) = _
  unfold AsymptoticSpectra.flatteningRank

  -- Rewrite using h_fXY
  conv_lhs => rw [h_fXY]

  -- Simplify using finrank_range_comp_equiv for the outer piTensorDistrib.symm
  -- The map is: piTensorDistrib.symm ∘ (tensorToDualHom ... ∘ piTensorDistrib.symm.dualMap)
  erw [finrank_range_comp_equiv]

  -- Now apply tensorToDualHom_tensorFourRearrange to factor the tensorToDualHom
  rw [tensorToDualHom_tensorFourRearrange]

  -- The map is now: ((map fX fY) ∘ dualDistribEquiv.symm) ∘ piTensorDistrib.symm.dualMap
  -- where fX = tensorToDualHom K AS BS tX and fY = tensorToDualHom K AT BT tY
  -- Need to show that dualDistribEquiv.symm ∘ piTensorDistrib.symm.dualMap is an equivalence
  -- Build the equivalence explicitly
  -- piTensorDistrib : ⨂[K] (i : σ.S), X.V ↑i ⊗[K] Y.V ↑i ≃ AS ⊗ AT
  -- piTensorDistrib.symm : AS ⊗ AT ≃ ⨂[K] (i : σ.S), X.V ↑i ⊗[K] Y.V ↑i
  -- (piTensorDistrib.symm).dualMap : Dual K (⨂...) → Dual K (AS ⊗ AT)
  -- But we need LinearEquiv, not LinearMap. Use LinearEquiv.dualMap:
  -- LinearEquiv.dualMap piTensorDistrib.symm : Dual K (AS ⊗ AT) ≃ Dual K (⨂...)
  -- So we need the inverse: (LinearEquiv.dualMap piTensorDistrib.symm).symm : Dual K (⨂...) ≃ Dual K (AS ⊗ AT)
  -- Note: LinearEquiv.dualMap e : Dual M₂ ≃ Dual M₁ when e : M₁ ≃ M₂
  let piTD := piTensorDistrib (K := K) (ι := σ.S) (V := fun i => X.V ↑i) (W := fun i => Y.V ↑i)
  -- piTD : ⨂[K] ... ≃ AS ⊗ AT
  -- piTD.symm : AS ⊗ AT ≃ ⨂[K] ...
  -- LinearEquiv.dualMap piTD.symm : Dual K (⨂...) ≃ Dual K (AS ⊗ AT)
  let e1 : Dual K (⨂[K] (i : σ.S), X.V ↑i ⊗[K] Y.V ↑i) ≃ₗ[K] Dual K (AS ⊗[K] AT) :=
    LinearEquiv.dualMap piTD.symm
  let e2 : (Dual K AS ⊗[K] Dual K AT) ≃ₗ[K] Dual K (AS ⊗[K] AT) :=
    TensorProduct.dualDistribEquiv K AS AT
  let e_comp : Dual K (⨂[K] (i : σ.S), X.V ↑i ⊗[K] Y.V ↑i) ≃ₗ[K] (Dual K AS ⊗[K] Dual K AT) :=
    e1.trans e2.symm
  have h_equiv : ((TensorProduct.dualDistribEquiv K AS AT).symm.toLinearMap.comp
                  piTD.symm.toLinearMap.dualMap) = e_comp.toLinearMap := by
    ext phi
    simp only [e_comp, e1, e2, piTD, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe,
               LinearEquiv.trans_apply]
    rfl
  rw [LinearMap.comp_assoc, h_equiv]

  -- Now we have f ∘ e_comp where e_comp is an equivalence
  -- Composing with equivalence on the right preserves the range
  have h_range_eq : (TensorProduct.map (tensorToDualHom K AS BS tX) (tensorToDualHom K AT BT tY) ∘ₗ
                     e_comp.toLinearMap).range =
                    (TensorProduct.map (tensorToDualHom K AS BS tX) (tensorToDualHom K AT BT tY)).range := by
    ext x
    simp only [LinearMap.mem_range, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe]
    constructor
    · rintro ⟨y, rfl⟩
      exact ⟨e_comp y, rfl⟩
    · rintro ⟨y, rfl⟩
      exact ⟨e_comp.symm y, by simp⟩
  have h_finrank_eq : finrank K ↥(TensorProduct.map ((tensorToDualHom K AS BS) tX) ((tensorToDualHom K AT BT) tY) ∘ₗ e_comp.toLinearMap).range =
      finrank K ↥(TensorProduct.map ((tensorToDualHom K AS BS) tX) ((tensorToDualHom K AT BT) tY)).range :=
    LinearEquiv.finrank_eq (LinearEquiv.ofEq _ _ (by
      rw [LinearMap.range_comp, LinearEquiv.range, Submodule.map_top]))
  refine h_finrank_eq.trans ?_

  -- Now we have: finrank K (range (map fX fY)) = finrank K (range fX) * finrank K (range fY)
  -- where fX = tensorToDualHom K AS BS tX : Dual K AS →ₗ[K] BS
  --       fY = tensorToDualHom K AT BT tY : Dual K AT →ₗ[K] BT
  -- Use finrank_range_map
  rw [finrank_range_map]

  -- Now we need to relate back to flatteningMap
  -- flatteningMap σ X = tensorToDualHom K AS BS (splitTensorEquiv σ X.t) = tensorToDualHom K AS BS tX
  -- and similarly for Y
  rfl

theorem flatteningRank_zero :
    flatteningRank σ (0 : Tensor K d) = 0 := by
  have : (0 : Tensor K d) = Tensor.toTensor TensorObj.zeroObj := rfl
  rw [this, flatteningRank_mk]
  unfold AsymptoticSpectra.flatteningRank flatteningMap
  have h_zero : (TensorObj.zeroObj : TensorObj K d).t = 0 := rfl
  rw [h_zero]
  rw [map_zero, map_zero]
  rw [LinearMap.range_zero, finrank_bot]



/-- A dual functional on `⨂[K] i, ULift K` that evaluates to the product of the components. -/
private noncomputable def tprodOneDual {ι : Type*} [Fintype ι] [DecidableEq ι] :
    Dual K (PiTensorProduct K (fun _ : ι => ULift K)) :=
  PiTensorProduct.lift
    { toFun := fun v => ∏ i, (v i).down
      map_update_add' := fun v i x y => by
        rw [Fintype.prod_eq_prod_compl_mul (a := i) (f := fun j => (Function.update v i (x + y) j).down),
            Fintype.prod_eq_prod_compl_mul (a := i) (f := fun j => (Function.update v i x j).down),
            Fintype.prod_eq_prod_compl_mul (a := i) (f := fun j => (Function.update v i y j).down)]
        simp only [Function.update_self, ULift.add_down]
        have h : ∀ z : ULift K, ∏ j ∈ {i}ᶜ, (Function.update v i z j).down = ∏ j ∈ {i}ᶜ, (v j).down := by
          intro z
          apply Finset.prod_congr rfl; intro j hj
          simp only [Finset.mem_compl, Finset.mem_singleton] at hj
          rw [Function.update_of_ne hj]
        rw [h (x + y), h x, h y]
        ring
      map_update_smul' := fun v i c x => by
        rw [Fintype.prod_eq_prod_compl_mul (a := i) (f := fun j => (Function.update v i (c • x) j).down),
            Fintype.prod_eq_prod_compl_mul (a := i) (f := fun j => (Function.update v i x j).down)]
        simp only [Function.update_self, ULift.smul_down, smul_eq_mul]
        have h : ∀ z : ULift K, ∏ j ∈ {i}ᶜ, (Function.update v i z j).down = ∏ j ∈ {i}ᶜ, (v j).down := by
          intro z
          apply Finset.prod_congr rfl; intro j hj
          simp only [Finset.mem_compl, Finset.mem_singleton] at hj
          rw [Function.update_of_ne hj]
        rw [h (c • x), h x]
        ring }

private theorem tprodOneDual_apply {ι : Type*} [Fintype ι] [DecidableEq ι]
    (v : ι → ULift K) :
    tprodOneDual (tprod K v) = ∏ i, (v i).down := by
  simp only [tprodOneDual, PiTensorProduct.lift.tprod]
  rfl

private theorem tprodOneDual_apply_one {ι : Type*} [Fintype ι] [DecidableEq ι] :
    tprodOneDual (tprod K (fun (_ : ι) => ULift.up (1 : K))) = (1 : K) := by
  rw [tprodOneDual_apply]
  simp

private theorem tprodOne_ne_zero {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι] :
    tprod K (fun (_ : ι) => ULift.up (1 : K)) ≠ (0 : PiTensorProduct K (fun _ : ι => ULift K)) := by
  intro h
  have := congr_arg tprodOneDual h
  simp only [map_zero] at this
  rw [tprodOneDual_apply_one] at this
  exact one_ne_zero this

theorem flatteningRank_one :
    flatteningRank σ (1 : Tensor K d) = 1 := by
  have : (1 : Tensor K d) = Tensor.toTensor TensorObj.oneObj := rfl
  rw [this, flatteningRank_mk]
  unfold AsymptoticSpectra.flatteningRank flatteningMap
  have h_split : splitTensorEquiv σ TensorObj.oneObj.t =
      tprod K (fun (_ : σ.S) => ULift.up (1 : K)) ⊗ₜ[K] tprod K (fun (_ : Sc σ) => ULift.up (1 : K)) := by
    have := @splitTensorEquiv_tprod K _ d σ (fun _ => ULift K)
      (fun _ => inferInstance) (fun _ => inferInstance) (fun _ => ULift.up 1)
    convert this using 2
  rw [h_split]
  let vS := tprod K (fun (_ : σ.S) => ULift.up (1 : K))
  let vSc := tprod K (fun (_ : Sc σ) => ULift.up (1 : K))
  change finrank K (LinearMap.range (tensorToDualHom K _ _ (vS ⊗ₜ[K] vSc))) = 1
  haveI : Nonempty σ.S := σ.hS.to_subtype
  haveI : Nonempty (Sc σ) := σ.hSc.to_subtype
  have hS_ne_zero : vS ≠ 0 := tprodOne_ne_zero
  have hSc_ne_zero : vSc ≠ 0 := tprodOne_ne_zero
  have h_range : LinearMap.range (tensorToDualHom K _ _ (vS ⊗ₜ[K] vSc)) = Submodule.span K {vSc} := by
    ext x
    constructor
    · rintro ⟨f, rfl⟩
      rw [tensorToDualHom_tmul]
      exact Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self _)
    · intro hx
      rw [Submodule.mem_span_singleton] at hx
      obtain ⟨c, rfl⟩ := hx
      use c • tprodOneDual
      rw [tensorToDualHom_tmul, LinearMap.smul_apply, tprodOneDual_apply]
      simp only [Finset.prod_const_one, smul_one_smul]
  rw [h_range, finrank_span_singleton hSc_ne_zero]

noncomputable def FlatteningRankPoint
    (P : SemiringPreorder (Tensor K d))
    (h_mono : ∀ {x y : Tensor K d}, P.le x y → flatteningRankReal σ x ≤ flatteningRankReal σ y) :
    SemiringSpectrumPoint (Tensor K d) P where
  toFun := flatteningRankReal σ
  map_zero' := by
    simp only [flatteningRankReal]
    rw [AsymptoticSpectra.Tensor.flatteningRank_zero σ]
    simp only [Nat.cast_zero]
  map_one' := by
    simp only [flatteningRankReal]
    rw [AsymptoticSpectra.Tensor.flatteningRank_one σ]
    simp only [Nat.cast_one]
  map_add' x y := by
    simp only [flatteningRankReal]
    rw [flatteningRank_add]
    push_cast
    rfl
  map_mul' x y := by
    simp only [flatteningRankReal]
    rw [flatteningRank_mul]
    push_cast
    rfl
  monotone' := h_mono


end AsymptoticSpectra.Tensor