Pivot spaces of a subspace of a product

For a subspace V of Fin r → M, the i-th pivot space consists of the i-th coordinates of the vectors of V that vanish in all coordinates below i. This is the block-echelon form of V used by Bourgain for affine extractors [Bou07] and by Ben-Sasson and Kopparty [BenSassonKopparty2012, Lemma 7.1]: choosing for each pivot vector a lift in V that vanishes below its block presents V in block-triangular form, and the dimensions of the pivot spaces add up to the dimension of V.

Main definitions

• Cslib.pivotSpace: the i-th pivot space of a subspace of Fin r → M.

Main results

• Cslib.mem_pivotSpace: pivot vectors lift to vectors of V vanishing below their block.
• Cslib.sum_finrank_pivotSpace: the dimensions of the pivot spaces add up to the dimension of V.

References

• J. Bourgain, On the construction of affine extractors
• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials

def Cslib.pivotSpace {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] {r : ℕ} (V : Submodule K (Fin r → M)) (i : Fin r) : Submodule K M

The i-th pivot space of V ≤ Fin r → M: the i-th coordinates of the vectors of V that vanish in every coordinate below i.

theorem Cslib.mem_pivotSpace {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] {r : ℕ} {V : Submodule K (Fin r → M)} {i : Fin r} {y : M} : y ∈ pivotSpace V i ↔ ∃ v ∈ V, (∀ j < i, v j = 0) ∧ v i = y

y lies in the i-th pivot space of V exactly when some v ∈ V vanishing in every coordinate below i has v i = y.

theorem Cslib.sum_finrank_pivotSpace {K : Type u_1} {M : Type u_2} [Field K] [AddCommGroup M] [Module K M] {r : ℕ} [FiniteDimensional K M] (V : Submodule K (Fin r → M)) : ∑ i : Fin r, Module.finrank K ↥(pivotSpace V i) = Module.finrank K ↥V

The dimensions of the pivot spaces of V add up to the dimension of V.