Three-way tensors, tensor rank, and border rank

A 3-tensor T ∈ ℂ^α ⊗ ℂ^β ⊗ ℂ^γ is given by its coordinates T i j k in the standard bases a_i ⊗ b_j ⊗ c_k (Algebraic.Tensor3). It carries the pointwise vector-space structure and the product topology on coordinates; for finite index types this is the usual Euclidean topology of ℂ^{α × β × γ}.

• Tensor3.outer u v w is the outer product u ⊗ v ⊗ w, with coordinates u i * v j * w k.
• Tensor3.RankLE T r: T is a sum of r outer products. Zero summands are allowed, so this is monotone in r; RankLE T 1 says that T is an outer product (rank at most one).
• Tensor3.tensorRank T is the least such r.
• Tensor3.BorderRankLE T r: T lies in the closure of the set of tensors of rank at most r, that is, T is a limit of tensors of rank at most r.
• Tensor3.borderRank T is the least such r.
• Tensor3.map X Y Z T applies the matrices X, Y, Z to the three factors, the linear map X ⊗ Y ⊗ Z.
• Tensor3.subtensor T f g h reindexes T along maps of the index types: deleting, permuting, or repeating slices in each factor.

The basic facts about these notions are in Complexitylib.Algebraic.LinearAlgebra.Tensor.BorderRank.

@[reducible, inline]

abbrev Algebraic.Tensor3 (α : Type u_1) (β : Type u_2) (γ : Type u_3) : Type (max (max u_1 u_2) u_3)

A 3-tensor in ℂ^α ⊗ ℂ^β ⊗ ℂ^γ, given by its coordinates: T i j k is the coefficient of a_i ⊗ b_j ⊗ c_k.

Equations

• Algebraic.Tensor3 α β γ = (α → β → γ → ℂ)

def Algebraic.Tensor3.outer {α : Type u_1} {β : Type u_2} {γ : Type u_3} (u : α → ℂ) (v : β → ℂ) (w : γ → ℂ) : Tensor3 α β γ

The outer product u ⊗ v ⊗ w, with coordinates u i * v j * w k.

Equations

• Algebraic.Tensor3.outer u v w i j k = u i * v j * w k

def Algebraic.Tensor3.RankLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} (T : Tensor3 α β γ) (r : ℕ) : Prop

T has rank at most r: it is a sum of r outer products. Zero vectors are allowed, so T.RankLE 0 means T = 0 and T.RankLE 1 means that T is an outer product.

Equations

• T.RankLE r = ∃ (u : Fin r → α → ℂ) (v : Fin r → β → ℂ) (w : Fin r → γ → ℂ), T = ∑ s : Fin r, Algebraic.Tensor3.outer (u s) (v s) (w s)

noncomputable def Algebraic.Tensor3.tensorRank {α : Type u_1} {β : Type u_2} {γ : Type u_3} (T : Tensor3 α β γ) : ℕ

The tensor rank of T: the least r such that T is a sum of r outer products. Over finite index types such an r exists (Tensor3.rankLE_tensorRank).

Equations

• T.tensorRank = sInf {r : ℕ | T.RankLE r}

def Algebraic.Tensor3.BorderRankLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} (T : Tensor3 α β γ) (r : ℕ) : Prop

T has border rank at most r: it lies in the closure, for the product topology on coordinates, of the set of tensors of rank at most r.

Equations

• T.BorderRankLE r = (T ∈ closure {S : Algebraic.Tensor3 α β γ | S.RankLE r})

noncomputable def Algebraic.Tensor3.borderRank {α : Type u_1} {β : Type u_2} {γ : Type u_3} (T : Tensor3 α β γ) : ℕ

The border rank of T: the least r such that T is a limit of tensors of rank at most r. Over finite index types such an r exists (Tensor3.borderRankLE_borderRank).

Equations

• T.borderRank = sInf {r : ℕ | T.BorderRankLE r}

def Algebraic.Tensor3.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} [Fintype α] [Fintype β] [Fintype γ] (X : Matrix α' α ℂ) (Y : Matrix β' β ℂ) (Z : Matrix γ' γ ℂ) (T : Tensor3 α β γ) : Tensor3 α' β' γ'

The image of T under the linear map X ⊗ Y ⊗ Z, for matrices X : ℂ^α → ℂ^α', Y : ℂ^β → ℂ^β', and Z : ℂ^γ → ℂ^γ'.

Equations

• Algebraic.Tensor3.map X Y Z T i' j' k' = ∑ i : α, ∑ j : β, ∑ k : γ, X i' i * Y j' j * Z k' k * T i j k

def Algebraic.Tensor3.subtensor {α : Type u_1} {β : Type u_2} {γ : Type u_3} {α' : Type u_4} {β' : Type u_5} {γ' : Type u_6} (T : Tensor3 α β γ) (f : α' → α) (g : β' → β) (h : γ' → γ) : Tensor3 α' β' γ'

Reindex T along maps of the three index types: the (i, j, k) coordinate of the result is the (f i, g j, h k) coordinate of T. For injective maps this deletes and permutes slices.

Equations

• T.subtensor f g h i j k = T (f i) (g j) (h k)