Koszul flattenings: proof internals

Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.Koszul.

• u ∧ u ∧ X = 0: wedgeMatrix (p + 1) u * wedgeMatrix p u = 0. The two ways of inserting a pair {i, i'} into a p-set K carry opposite signs.
• If u i₀ ≠ 0, the rows K ∪ {i₀} and columns K with i₀ ∉ K of wedgeMatrix p u form an invertible diagonal submatrix, so its rank is at least (n - 1).choose p, where n = card α.
• Hence, by rank A + rank B ≤ card m for A * B = 0 and Pascal's rule, the rank of wedgeMatrix (p + 1) u is at most n.choose (p + 1) - (n - 1).choose p = (n - 1).choose (p + 1).
• The Koszul flattening of u ⊗ v ⊗ w factors through wedgeMatrix p u, so its rank is at most (n - 1).choose p; subadditivity and closedness of bounded-rank matrices transfer the bound to rank and border rank.

theorem Algebraic.Tensor3.Internal.sum_sum_eq_zero_of_antisymm {ι : Type u_1} [Fintype ι] (g : ι → ι → ℂ) (h : ∀ (i i' : ι), g i i' = -g i' i) : ∑ i : ι, ∑ i' : ι, g i i' = 0

theorem Algebraic.Tensor3.Internal.card_filter_insert_lt {α : Type u_1} [LinearOrder α] {i i' : α} {K : Finset α} (hi' : i' ∉ K) : {x ∈ insert i' K | x < i}.card = {x ∈ K | x < i}.card + if i' < i then 1 else 0

theorem Algebraic.Tensor3.Internal.wedgeCoeff_pair_antisymm {α : Type u_1} [LinearOrder α] (J K : Finset α) (i i' : α) : wedgeCoeff J (insert i' K) i * wedgeCoeff (insert i' K) K i' = -(wedgeCoeff J (insert i K) i' * wedgeCoeff (insert i K) K i)

The contributions of (i, i') and (i', i) to u ∧ u ∧ e_K cancel.

theorem Algebraic.Tensor3.Internal.sum_wedgeCoeff_mul {α : Type u_1} [LinearOrder α] [Fintype α] {p : ℕ} (J : Finset α) {K : Finset α} (hK : K.card = p) (i i' : α) : ∑ I : { I : Finset α // I.card = p + 1 }, wedgeCoeff J (↑I) i * wedgeCoeff (↑I) K i' = wedgeCoeff J (insert i' K) i * wedgeCoeff (insert i' K) K i'

theorem Algebraic.Tensor3.Internal.wedgeCoeff_insert_ne {α : Type u_1} [LinearOrder α] {i₀ i : α} {I : Finset α} (hne : i ≠ i₀) : wedgeCoeff (insert i₀ I) I i = 0

theorem Algebraic.Tensor3.Internal.wedgeCoeff_insert_of_ne {α : Type u_1} [LinearOrder α] {i₀ i : α} {I I' : Finset α} (hi₀ : i₀ ∉ I) (hi₀' : i₀ ∉ I') (hne : I ≠ I') : wedgeCoeff (insert i₀ I) I' i = 0

theorem Algebraic.Tensor3.Internal.wedgeMatrix_mul_wedgeMatrix {α : Type u_1} [LinearOrder α] [Fintype α] (p : ℕ) (u : α → ℂ) : wedgeMatrix (p + 1) u * wedgeMatrix p u = 0

u ∧ u ∧ X = 0.

theorem Algebraic.Tensor3.Internal.le_rank_wedgeMatrix {α : Type u_1} [LinearOrder α] [Fintype α] (p : ℕ) {u : α → ℂ} {i₀ : α} (h : u i₀ ≠ 0) : (Fintype.card α - 1).choose p ≤ (wedgeMatrix p u).rank

If u i₀ ≠ 0, then u ∧ · has rank at least (n - 1).choose p on Λ^p.

theorem Algebraic.Tensor3.Internal.rank_wedgeMatrix_le {α : Type u_1} [LinearOrder α] [Fintype α] (p : ℕ) (u : α → ℂ) : (wedgeMatrix p u).rank ≤ (Fintype.card α - 1).choose p

u ∧ · has rank at most (n - 1).choose p on Λ^p.

theorem Algebraic.Tensor3.Internal.koszulFlattening_degree_zero_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (T : Tensor3 α β γ) (i : α) (j : β) (k : γ) : koszulFlattening 0 T (⟨{i}, ⋯⟩, k) (⟨∅, ⋯⟩, j) = T i j k

theorem Algebraic.Tensor3.Internal.koszulFlattening_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (p : ℕ) (S T : Tensor3 α β γ) : koszulFlattening p (S + T) = koszulFlattening p S + koszulFlattening p T

theorem Algebraic.Tensor3.Internal.koszulFlattening_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (p : ℕ) : koszulFlattening p 0 = 0

theorem Algebraic.Tensor3.Internal.koszulFlattening_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (p : ℕ) (c : ℂ) (T : Tensor3 α β γ) : koszulFlattening p (c • T) = c • koszulFlattening p T

theorem Algebraic.Tensor3.Internal.koszulFlattening_finset_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (p : ℕ) {ι : Type u_4} (s : Finset ι) (T : ι → Tensor3 α β γ) : koszulFlattening p (∑ x ∈ s, T x) = ∑ x ∈ s, koszulFlattening p (T x)

theorem Algebraic.Tensor3.Internal.continuous_koszulFlattening {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (p : ℕ) : Continuous (koszulFlattening p)

theorem Algebraic.Tensor3.Internal.koszulFlattening_outer {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] (p : ℕ) (u : α → ℂ) (v : β → ℂ) (w : γ → ℂ) : koszulFlattening p (outer u v w) = (Matrix.of fun (Jk : { J : Finset α // J.card = p + 1 } × γ) (J : { J : Finset α // J.card = p + 1 }) => if Jk.1 = J then w Jk.2 else 0) * wedgeMatrix p u * Matrix.of fun (I : { I : Finset α // I.card = p }) (Ij : { I : Finset α // I.card = p } × β) => if I = Ij.1 then v Ij.2 else 0

The Koszul flattening of u ⊗ v ⊗ w is (u ∧ ·) ⊗ w vᵀ, factored through wedgeMatrix p u.

theorem Algebraic.Tensor3.Internal.rank_koszulFlattening_outer_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] [Fintype β] (p : ℕ) (u : α → ℂ) (v : β → ℂ) (w : γ → ℂ) : (koszulFlattening p (outer u v w)).rank ≤ (Fintype.card α - 1).choose p

The Koszul flattening of an outer product has rank at most (card α - 1).choose p.

theorem Algebraic.Tensor3.Internal.rank_koszulFlattening_le_of_rankLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] [Fintype β] (p : ℕ) {T : Tensor3 α β γ} {r : ℕ} (h : T.RankLE r) : (koszulFlattening p T).rank ≤ r * (Fintype.card α - 1).choose p

theorem Algebraic.Tensor3.Internal.rank_koszulFlattening_le_of_borderRankLE {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [Fintype α] [Fintype β] [Fintype γ] (p : ℕ) {T : Tensor3 α β γ} {r : ℕ} (h : T.BorderRankLE r) : (koszulFlattening p T).rank ≤ r * (Fintype.card α - 1).choose p