The set-multilinear projection

The variables σ of a polynomial are split into d blocks by a map blk : σ → Fin d. A monomial is set-multilinear on a set S of blocks when it is blockMonomial blk S x for a choice x of one variable from each block of S. The set-multilinear projection MvPolynomial.smProj blk S keeps the terms of a polynomial whose monomials are set-multilinear on S and drops the others ([Forbes2024, Def. 23], where it is π_{sm,S}). It is a linear map whose image consists of the set-multilinear polynomials on S and which fixes them (MvPolynomial.smProj_eq_self_iff); on the empty set of blocks it is the constant coefficient (MvPolynomial.smProj_empty).

A monomial is set-multilinear on S exactly when its block degrees, the exponent sums over the blocks, are one on S and zero elsewhere (MvPolynomial.mem_range_blockMonomial_iff). The block degrees are the weight of the monomial for the weight v ↦ single (blk v) 1, valued in Fin d →₀ ℕ, that sends each variable to the unit vector of its block. So the set-multilinear polynomials on S are the weighted homogeneous polynomials of weighted degree the indicator of S (MvPolynomial.isSetMultilinear_iff_isWeightedHomogeneous), and smProj blk S is defined as Mathlib's MvPolynomial.weightedHomogeneousComponent for this weight and degree; idempotence and orthogonality come from Mathlib. From the characterization, the projection of a product is the sum, over the ways of splitting S into disjoint parts, one for each factor, of the products of the projections of the factors on their parts (MvPolynomial.smProj_mul, MvPolynomial.smProj_prod): a set-multilinear monomial of the product comes from set-multilinear monomials of the factors on disjoint blocks. The projection commutes with renaming variables along their blocks (MvPolynomial.rename_smProj).

Main definitions

• MvPolynomial.smProj: the projection onto the set-multilinear monomials on a set of blocks, a weighted homogeneous component.
• MvPolynomial.blockSplits: the families of pairwise disjoint sets of blocks, indexed by a finite type, with a given union.

Main results

• MvPolynomial.mem_range_blockMonomial_iff: a monomial is set-multilinear on S if and only if its block degrees are the indicator of S.
• MvPolynomial.isSetMultilinear_iff_isWeightedHomogeneous: set-multilinear polynomials on S are the weighted homogeneous polynomials, for the block weight, of degree the indicator of S.
• MvPolynomial.sum_mem_range_blockMonomial_iff, MvPolynomial.add_mem_range_blockMonomial_iff: a product of monomials is set-multilinear on S exactly when the factors are set-multilinear on the parts of an ordered split of S.
• MvPolynomial.isSetMultilinear_smProj, MvPolynomial.smProj_eq_self_iff: the projection is set-multilinear and fixes exactly the set-multilinear polynomials.
• MvPolynomial.IsSetMultilinear.smProj_eq_zero, MvPolynomial.smProj_smProj: the projections on different sets of blocks are orthogonal.
• MvPolynomial.smProj_empty, MvPolynomial.smProj_C, MvPolynomial.smProj_one, MvPolynomial.smProj_X: projections of constants and variables.
• MvPolynomial.smProj_mul, MvPolynomial.smProj_prod: projections of products.
• MvPolynomial.rename_smProj: the projection commutes with renaming along the blocks.

References

• M. A. Forbes, Low-depth algebraic circuit lower bounds over any field, Definition 23, p. 31:12 (the projection π_{sm,S}), and the remark after it, p. 31:13 (π_{sm,∅}(f) = f(0)). The product formulas smProj_mul and smProj_prod are the expansion used in the proof of [Forbes2024, Lemma 26], pp. 31:13–31:14; their statement as identities of polynomials, the block-degree characterization, its weighted homogeneous form and rename_smProj are original.

theorem MvPolynomial.mem_range_blockMonomial_iff {σ : Type u_1} {d : ℕ} {blk : σ → Fin d} {S : Finset (Fin d)} {m : σ →₀ ℕ} : m ∈ Set.range (blockMonomial blk S) ↔ Finsupp.mapDomain blk m = ∑ i ∈ S, Finsupp.single i 1

Block-degree characterization. A monomial is set-multilinear on S, that is, it takes exactly one variable with exponent one from each block of S and no other variable, if and only if its block degrees are 1 on the blocks of S and 0 on the others (original).

theorem Finsupp.weight_single_one_eq_mapDomain {σ : Type u_1} {τ : Type u_3} (blk : σ → τ) (m : σ →₀ ℕ) : (weight fun (v : σ) => single (blk v) 1) m = mapDomain blk m

The weight that sends each variable to the unit vector of its block computes the block degrees of a monomial.

theorem MvPolynomial.mem_range_blockMonomial_iff_weight {σ : Type u_1} {d : ℕ} {blk : σ → Fin d} {S : Finset (Fin d)} {m : σ →₀ ℕ} : m ∈ Set.range (blockMonomial blk S) ↔ (Finsupp.weight fun (v : σ) => Finsupp.single (blk v) 1) m = ∑ i ∈ S, Finsupp.single i 1

A monomial is set-multilinear on S exactly when its weight, for the weight v ↦ single (blk v) 1 that sends each variable to the unit vector of its block, is the indicator of S.

theorem MvPolynomial.eq_of_mem_range_blockMonomial {σ : Type u_1} {d : ℕ} {blk : σ → Fin d} {S T : Finset (Fin d)} {m : σ →₀ ℕ} (hS : m ∈ Set.range (blockMonomial blk S)) (hT : m ∈ Set.range (blockMonomial blk T)) : S = T

A monomial is set-multilinear on at most one set of blocks.

theorem MvPolynomial.mapDomain_mem_range_blockMonomial_iff {σ : Type u_1} {d : ℕ} {τ : Type u_3} {blk : σ → Fin d} {blk' : τ → Fin d} (e : σ → τ) (he : ∀ (v : σ), blk' (e v) = blk v) {S : Finset (Fin d)} {m : σ →₀ ℕ} : Finsupp.mapDomain e m ∈ Set.range (blockMonomial blk' S) ↔ m ∈ Set.range (blockMonomial blk S)

Renaming the variables along their blocks preserves set-multilinearity of monomials, in both directions (original).

def MvPolynomial.blockSplits {d : ℕ} (ι : Type u_3) [Fintype ι] [DecidableEq ι] (S : Finset (Fin d)) : Finset (ι → Finset (Fin d))

The ordered splits of a set S of blocks into ι-indexed parts: the families of pairwise disjoint, possibly empty sets of blocks whose union is S.

theorem MvPolynomial.mem_blockSplits {d : ℕ} {ι : Type u_3} [Fintype ι] [DecidableEq ι] {S : Finset (Fin d)} {T : ι → Finset (Fin d)} : T ∈ blockSplits ι S ↔ Pairwise (Function.onFun Disjoint T) ∧ Finset.univ.biUnion T = S

A family is an ordered split of S exactly when its parts are pairwise disjoint with union S.

theorem MvPolynomial.sum_mem_range_blockMonomial_iff {σ : Type u_1} {d : ℕ} {ι : Type u_3} [Fintype ι] [DecidableEq ι] {blk : σ → Fin d} {S : Finset (Fin d)} (y : ι → σ →₀ ℕ) : ∑ j : ι, y j ∈ Set.range (blockMonomial blk S) ↔ ∃ T ∈ blockSplits ι S, ∀ (j : ι), y j ∈ Set.range (blockMonomial blk (T j))

A family of monomials multiplies to a set-multilinear monomial on S exactly when its members are set-multilinear on the parts of an ordered split of S (original).

theorem MvPolynomial.add_mem_range_blockMonomial_iff {σ : Type u_1} {d : ℕ} {blk : σ → Fin d} {S : Finset (Fin d)} {a b : σ →₀ ℕ} : a + b ∈ Set.range (blockMonomial blk S) ↔ ∃ T ∈ S.powerset, a ∈ Set.range (blockMonomial blk T) ∧ b ∈ Set.range (blockMonomial blk (S \ T))

Two monomials multiply to a set-multilinear monomial on S exactly when they are set-multilinear on complementary parts of S (original).

theorem MvPolynomial.isSetMultilinear_iff_isWeightedHomogeneous {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} : IsSetMultilinear blk S f ↔ IsWeightedHomogeneous (fun (v : σ) => Finsupp.single (blk v) 1) f (∑ i ∈ S, Finsupp.single i 1)

Set-multilinear polynomials are weighted homogeneous. A polynomial is set-multilinear on S exactly when it is weighted homogeneous of weighted degree the indicator of S, for the weight v ↦ single (blk v) 1 that sends each variable to the unit vector of its block (original).

noncomputable def MvPolynomial.smProj {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) : MvPolynomial σ K →ₗ[K] MvPolynomial σ K

The set-multilinear projection π_{sm,S} of [Forbes2024, Def. 23]: the linear map that keeps the terms whose monomials are set-multilinear on the set S of blocks and drops the others. It is Mathlib's weighted homogeneous component of weighted degree the indicator of S, for the weight v ↦ single (blk v) 1 that sends each variable to the unit vector of its block (MvPolynomial.isSetMultilinear_iff_isWeightedHomogeneous).

theorem MvPolynomial.smProj_eq_weightedHomogeneousComponent {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) : smProj blk S = weightedHomogeneousComponent (fun (v : σ) => Finsupp.single (blk v) 1) (∑ i ∈ S, Finsupp.single i 1)

The set-multilinear projection on S is the weighted homogeneous component, for the block weight, of weighted degree the indicator of S.

theorem MvPolynomial.coeff_smProj_of_mem {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} {m : σ →₀ ℕ} (hm : m ∈ Set.range (blockMonomial blk S)) : ((smProj blk S) f).coeff m = f.coeff m

The projection keeps the coefficients of the set-multilinear monomials on S.

theorem MvPolynomial.coeff_smProj_of_notMem {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} {m : σ →₀ ℕ} (hm : m ∉ Set.range (blockMonomial blk S)) : ((smProj blk S) f).coeff m = 0

The projection drops the coefficients of the other monomials.

theorem MvPolynomial.smProj_monomial {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} (m : σ →₀ ℕ) (a : K) [Decidable (m ∈ Set.range (blockMonomial blk S))] : (smProj blk S) ((monomial m) a) = if m ∈ Set.range (blockMonomial blk S) then (monomial m) a else 0

The projection of a monomial keeps it if it is set-multilinear on S, and is zero otherwise.

theorem MvPolynomial.isSetMultilinear_smProj {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) (f : MvPolynomial σ K) : IsSetMultilinear blk S ((smProj blk S) f)

The projection is set-multilinear on S.

theorem MvPolynomial.IsSetMultilinear.smProj_eq_self {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} (hf : IsSetMultilinear blk S f) : (smProj blk S) f = f

The projection on S fixes a set-multilinear polynomial on S.

theorem MvPolynomial.smProj_eq_self_iff {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} : (smProj blk S) f = f ↔ IsSetMultilinear blk S f

A polynomial is set-multilinear on S exactly when the projection on S fixes it.

theorem MvPolynomial.IsSetMultilinear.smProj_eq_zero {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S T : Finset (Fin d)} {f : MvPolynomial σ K} (hf : IsSetMultilinear blk S f) (hST : T ≠ S) : (smProj blk T) f = 0

The projection on T of a set-multilinear polynomial on a different set S is zero.

theorem MvPolynomial.smProj_smProj {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S T : Finset (Fin d)} {f : MvPolynomial σ K} [Decidable (T = S)] : (smProj blk T) ((smProj blk S) f) = if T = S then (smProj blk S) f else 0

Projecting twice: the projections on different sets of blocks are orthogonal, and each is idempotent.

theorem MvPolynomial.smProj_add {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f g : MvPolynomial σ K} : (smProj blk S) (f + g) = (smProj blk S) f + (smProj blk S) g

The projection is additive.

theorem MvPolynomial.smProj_C_mul {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {S : Finset (Fin d)} {f : MvPolynomial σ K} (c : K) : (smProj blk S) (C c * f) = C c * (smProj blk S) f

The projection commutes with multiplication by a constant.

theorem MvPolynomial.smProj_empty {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (f : MvPolynomial σ K) : (smProj blk ∅) f = C (constantCoeff f)

The projection on no blocks is the constant coefficient [Forbes2024, p. 31:13].

theorem MvPolynomial.smProj_C {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) (c : K) : (smProj blk S) (C c) = if S = ∅ then C c else 0

The projection of a constant is the constant on no blocks and zero otherwise.

theorem MvPolynomial.smProj_one {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) : (smProj blk S) 1 = if S = ∅ then 1 else 0

The projection of 1 is 1 on no blocks and zero otherwise.

theorem MvPolynomial.smProj_X {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) (v : σ) : (smProj blk S) (X v) = if S = {blk v} then X v else 0

The projection of a variable is the variable on its own block and zero otherwise.

theorem MvPolynomial.smProj_mul {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] (blk : σ → Fin d) (S : Finset (Fin d)) (f g : MvPolynomial σ K) : (smProj blk S) (f * g) = ∑ T ∈ S.powerset, (smProj blk T) f * (smProj blk (S \ T)) g

The projection of a product (original as stated; the expansion in the proof of [Forbes2024, Lemma 26]): the set-multilinear part of f * g on S is the sum, over the parts T ⊆ S, of the product of the part of f on T and the part of g on S \ T.

theorem MvPolynomial.smProj_prod {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (blk : σ → Fin d) (S : Finset (Fin d)) (f : ι → MvPolynomial σ K) : (smProj blk S) (∏ j : ι, f j) = ∑ T ∈ blockSplits ι S, ∏ j : ι, (smProj blk (T j)) (f j)

The projection of a finite product (original as stated; the expansion in the proof of [Forbes2024, Lemma 26]): the set-multilinear part of ∏ j, f j on S is the sum, over the ordered splits T of S into pairwise disjoint parts T j covering S, of the products of the parts of the factors f j on T j.

theorem MvPolynomial.rename_smProj {σ : Type u_1} {K : Type u_2} {d : ℕ} [CommSemiring K] {blk : σ → Fin d} {τ : Type u_3} {blk' : τ → Fin d} (e : σ → τ) (he : ∀ (v : σ), blk' (e v) = blk v) (S : Finset (Fin d)) (f : MvPolynomial σ K) : (rename e) ((smProj blk S) f) = (smProj blk' S) ((rename e) f)

The projection commutes with renaming along the blocks (original): if the renaming e sends each variable to a variable of the same block, then renaming the part of f on S gives the part on S of the renamed polynomial. The renaming need not be injective.