Exact rank of polynomial convolution

Each output coefficient of polynomial multiplication occurs in some product of two input monomials. Choosing one such pair for each output gives an identity minor in the output flattening. Together with evaluation and interpolation, this proves the exact rank of C(a,b) for positive dimensions.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_identity_minor {K : Type} [Field K] {a b : ℕ} (ha : 0 < a) (hb : 0 < b) : ∃ (x : Fin (a + b - 1) → Fin a) (y : Fin (a + b - 1) → Fin b), ∀ (k l : Fin (a + b - 1)), convolution K a b (x k) (y k) l = if k = l then 1 else 0

Choosing one product for every output monomial gives an identity minor of the output flattening.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.convolution_rank_lower {K : Type} [Field K] {a b r : ℕ} (ha : 0 < a) (hb : 0 < b) (hRank : (convolution K a b).RankAtMost r) : a + b - 1 ≤ r

Every rank decomposition of convolution has at least one term per output coefficient.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.exactRank_convolution {K : Type} [Field K] [IsAlgClosed K] {a b : ℕ} (ha : 0 < a) (hb : 0 < b) : exactRank (convolution K a b) = a + b - 1

Polynomial multiplication has exact rank a+b-1 when both inputs have positive dimension.