Sparsifying images of product maps

Let π : A → B → X be a map of finite sets. Suppose a function space V on X pulls back to sums of matrices whose columns lie in U and matrices whose rows lie in W. Then the image of π is covered by the images of a small collection of rows and columns. The number of selected inputs is at most dim U + dim W + (|X| - dim V).

The proof selects enough coordinates to determine U and W. A function in V supported on the uncovered outputs must vanish: its pullback vanishes on the selected rows and columns, which determine every matrix in the slice space. The coordinate space on the uncovered outputs is therefore disjoint from V, bounding the number of exceptions by its codimension.

This is a general linear-algebra argument. The application to Boolean sumsets uses low-degree polynomial spaces, but neither polynomials nor a group operation appear in this module.

Main definitions

• Cslib.ImageSparsification.sliceSpace: sums of column-constrained and row-constrained matrices.
• Cslib.ImageSparsification.HasSliceDecomposition: a product map pulls an output space back into a specified slice space.

Main results

• Cslib.ImageSparsification.mul_mem_sliceSpace_left, Cslib.ImageSparsification.mul_mem_sliceSpace_right: build separable slices from either factor.
• Cslib.ImageSparsification.hasSliceDecomposition_span: check the pullback condition on generators.
• Cslib.ImageSparsification.HasSliceDecomposition.comp: restrict or reparameterize either input.
• Cslib.ImageSparsification.exists_image_cover_with_exceptions: separate dimension budgets for selected rows, selected columns, and exceptional outputs.
• Cslib.ImageSparsification.exists_image_cover: absorb the exceptions to obtain an exact cover.

def Cslib.ImageSparsification.sliceSpace {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] (U : Submodule K (A → K)) (W : Submodule K (B → K)) : Submodule K (A → B → K)

The space of matrices that are sums of a matrix with columns in U and a matrix with rows in W. This is the concrete finite-function version of U ⊗ Kᴮ + Kᴬ ⊗ W.

@[simp]

theorem Cslib.ImageSparsification.sliceSpace_bot_bot {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] : sliceSpace ⊥ ⊥ = ⊥

With zero column and row spaces, the slice space consists only of the zero matrix.

theorem Cslib.ImageSparsification.mul_mem_sliceSpace_left {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] {U : Submodule K (A → K)} (W : Submodule K (B → K)) {u : A → K} (hu : u ∈ U) (r : B → K) : (fun (a : A) (b : B) => u a * r b) ∈ sliceSpace U W

A separable matrix belongs to the slice space when its left factor belongs to U.

theorem Cslib.ImageSparsification.mul_mem_sliceSpace_right {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] (U : Submodule K (A → K)) {W : Submodule K (B → K)} (l : A → K) {w : B → K} (hw : w ∈ W) : (fun (a : A) (b : B) => l a * w b) ∈ sliceSpace U W

A separable matrix belongs to the slice space when its right factor belongs to W.

def Cslib.ImageSparsification.HasSliceDecomposition {K : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Field K] (π : A → B → X) (U : Submodule K (A → K)) (W : Submodule K (B → K)) (V : Submodule K (X → K)) : Prop

Pulling back every function in V along π gives a matrix in sliceSpace U W.

theorem Cslib.ImageSparsification.hasSliceDecomposition_span {K : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Field K] {ι : Type u_5} (π : A → B → X) (U : Submodule K (A → K)) (W : Submodule K (B → K)) (v : ι → X → K) (h : ∀ (i : ι), (fun (a : A) (b : B) => v i (π a b)) ∈ sliceSpace U W) : HasSliceDecomposition π U W (Submodule.span K (Set.range v))

It suffices to establish the slice decomposition for generators of the output space.

theorem Cslib.ImageSparsification.HasSliceDecomposition.comp {K : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Field K] {π : A → B → X} {U : Submodule K (A → K)} {W : Submodule K (B → K)} {V : Submodule K (X → K)} (h : HasSliceDecomposition π U W V) {A' : Type u_5} {B' : Type u_6} (f : A' → A) (g : B' → B) : HasSliceDecomposition (fun (a : A') (b : B') => π (f a) (g b)) (Submodule.map (LinearMap.funLeft K K f) U) (Submodule.map (LinearMap.funLeft K K g) W) V

A slice decomposition remains valid after restricting or reparameterizing either input.

theorem Cslib.ImageSparsification.exists_image_cover_with_exceptions {K : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Field K] [Finite A] [Finite B] [Fintype X] {π : A → B → X} {U : Submodule K (A → K)} {W : Submodule K (B → K)} {V : Submodule K (X → K)} (h : HasSliceDecomposition π U W V) : ∃ (s : Finset A) (t : Finset B) (e : Finset X), s.card ≤ Module.finrank K ↥U ∧ t.card ≤ Module.finrank K ↥W ∧ e.card ≤ Fintype.card X - Module.finrank K ↥V ∧ (∀ x ∈ e, ∃ (a : A) (b : B), π a b = x) ∧ ∀ (a : A) (b : B), π a b ∈ e ∨ (∃ a' ∈ s, ∃ (b' : B), π a' b' = π a b) ∨ ∃ b' ∈ t, ∃ (a' : A), π a' b' = π a b

Select at most dim U rows and dim W columns. Their images cover every output except for at most |X| - dim V outputs, each of which is still in the image of π.

theorem Cslib.ImageSparsification.exists_image_cover {K : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} [Field K] [Finite A] [Finite B] [Fintype X] {π : A → B → X} {U : Submodule K (A → K)} {W : Submodule K (B → K)} {V : Submodule K (X → K)} (h : HasSliceDecomposition π U W V) : ∃ (s : Finset A) (t : Finset B), s.card + t.card ≤ Module.finrank K ↥U + Module.finrank K ↥W + (Fintype.card X - Module.finrank K ↥V) ∧ ∀ (a : A) (b : B), (∃ a' ∈ s, ∃ (b' : B), π a' b' = π a b) ∨ ∃ b' ∈ t, ∃ (a' : A), π a' b' = π a b

Image sparsification. If the output function space pulls back into a two-sided slice space, the image is covered by rows and columns with total budget dim U + dim W + (|X| - dim V). All selected coordinates are actual inputs of π.

The construction is nonuniform: each exceptional output is absorbed by choosing one of its preimages. No algorithm for finding the selected coordinates is asserted.