Koszul flattenings

Let A = ℂ^α with basis a_i, where α is a finite linearly ordered type. The exterior power Λ^p A has the basis e_I = a_{i₁} ∧ ⋯ ∧ a_{i_p} indexed by the p-element subsets I = {i₁ < ⋯ < i_p} of α. Moving a_i past the factors of e_I below i gives the sign convention used here:

a_i ∧ e_I = (-1)^#{x ∈ I | x < i} e_{I ∪ {i}} if i ∉ I, and a_i ∧ e_I = 0 if i ∈ I.

• Tensor3.wedgeCoeff J I i is the coefficient of e_J in a_i ∧ e_I.
• Tensor3.wedgeMatrix p u is the matrix of X ↦ u ∧ X : Λ^p A → Λ^{p+1} A for u ∈ A; its rows are indexed by (p + 1)-subsets and its columns by p-subsets of α.
• Tensor3.koszulFlattening p T is the Koszul flattening T_A^{∧p} : Λ^p A ⊗ B^* → Λ^{p+1} A ⊗ C of T = ∑ T i j k a_i ⊗ b_j ⊗ c_k (Landsberg and Michałek, Towards finding hay in a haystack, Theory of Computing 2025, §4.1), which sends e_I ⊗ b_j^* to ∑_{i,k} T i j k (a_i ∧ e_I) ⊗ c_k. Its rows are indexed by pairs (J, k) of a (p + 1)-subset J of α and k : γ, its columns by pairs (I, j) of a p-subset I of α and j : β, and its ((J, k), (I, j)) entry is the (J, I) entry of wedgeMatrix p (T · j k).

The border-rank lower bound rank T_A^{∧p} ≤ borderRank T * (card α - 1).choose p is in Complexitylib.Algebraic.LinearAlgebra.Tensor.Koszul.

def Algebraic.Tensor3.wedgeCoeff {α : Type u_1} [LinearOrder α] (J I : Finset α) (i : α) : ℂ

The coefficient of e_J in a_i ∧ e_I: (-1)^#{x ∈ I | x < i} if i ∉ I and J = I ∪ {i}, and 0 otherwise.

Equations

• Algebraic.Tensor3.wedgeCoeff J I i = if i ∉ I ∧ insert i I = J then (-1) ^ {x ∈ I | x < i}.card else 0

def Algebraic.Tensor3.wedgeMatrix {α : Type u_1} [LinearOrder α] [Fintype α] (p : ℕ) (u : α → ℂ) : Matrix { J : Finset α // J.card = p + 1 } { I : Finset α // I.card = p } ℂ

The matrix of X ↦ u ∧ X : Λ^p ℂ^α → Λ^{p+1} ℂ^α in the bases e_I: its (J, I) entry is ∑ i, wedgeCoeff J I i * u i.

Equations

• Algebraic.Tensor3.wedgeMatrix p u = Matrix.of fun (J : { J : Finset α // J.card = p + 1 }) (I : { I : Finset α // I.card = p }) => ∑ i : α, Algebraic.Tensor3.wedgeCoeff (↑J) (↑I) i * u i

def Algebraic.Tensor3.koszulFlattening {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (p : ℕ) (T : Tensor3 α β γ) : Matrix ({ J : Finset α // J.card = p + 1 } × γ) ({ I : Finset α // I.card = p } × β) ℂ

The Koszul flattening T_A^{∧p} : Λ^p A ⊗ B^* → Λ^{p+1} A ⊗ C, e_I ⊗ b_j^* ↦ ∑_{i,k} T i j k (a_i ∧ e_I) ⊗ c_k. Its ((J, k), (I, j)) entry is ∑ i, wedgeCoeff J I i * T i j k.

Equations

• One or more equations did not get rendered due to their size.