Pointwise products of two stable subspaces span everything

Let K be an infinite field, ι a finite set and Γ a group acting transitively on ι and on ι → K by signed permutations, (γ • f) i = ε γ i * f (γ⁻¹ • i). If V, W ≤ ι → K are Γ-stable (possibly with different signs εV, εW, as long as εV γ i * εW γ i = 1) and dim V + dim W > |ι|, then the pointwise products v * w span ι → K. This is a statement of Cauchy–Davenport type.

The proof: the orthogonal U of the span S for ∑ x_i y_i is stable under the unsigned translations; if S ≠ ⊤ then U ≠ 0, and since a vector space over an infinite field is not a finite union of proper subspaces (Mathlib's Subspace.exists_eq_top_of_iUnion_eq_univ), U contains a vector u with full support; v ↦ u * v embeds V into the orthogonal of W.

Main results

• ConjeturaC.span_mul_eq_top: the statement above.

References

• C. Marín, Where the character values of Sp(2m) at a torsion element fail to generate the ring of integers, Zenodo (2026), doi:10.5281/zenodo.22813216 (Proposition prop:mono, complementary layers).

def ConjeturaC.dotB {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] : LinearMap.BilinForm K (ι → K)

The standard symmetric bilinear form Σ x_i y_i.

Equations

• ConjeturaC.dotB = dotProductBilin K K

theorem ConjeturaC.dotB_apply {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] (x y : ι → K) : (dotB x) y = ∑ i : ι, x i * y i

theorem ConjeturaC.dotB_nondegenerate {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] : dotB.Nondegenerate

theorem ConjeturaC.finrank_add_finrank_orth {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] (W : Submodule K (ι → K)) : Module.finrank K ↥W + Module.finrank K ↥(dotB.orthogonal W) = Fintype.card ι

dim W + dim Wᗮ = |ι|.

def ConjeturaC.transl {K : Type u_1} {ι : Type u_2} {Γ : Type u_3} [Field K] [Group Γ] [MulAction Γ ι] (γ : Γ) : (ι → K) →ₗ[K] ι → K

Unsigned translation f ↦ f ∘ (γ⁻¹ • ·) as a linear map.

Equations

• ConjeturaC.transl γ = LinearMap.funLeft K K fun (i : ι) => γ⁻¹ • i

theorem ConjeturaC.transl_apply {K : Type u_1} {ι : Type u_2} {Γ : Type u_3} [Field K] [Group Γ] [MulAction Γ ι] (γ : Γ) (f : ι → K) (i : ι) : (transl γ) f i = f (γ⁻¹ • i)

theorem ConjeturaC.dotB_transl {K : Type u_1} {ι : Type u_2} {Γ : Type u_3} [Field K] [Fintype ι] [Group Γ] [MulAction Γ ι] (γ : Γ) (s u : ι → K) : (dotB s) ((transl γ) u) = (dotB ((transl γ⁻¹) s)) u

theorem ConjeturaC.span_mul_eq_top {K : Type u_1} {ι : Type u_2} {Γ : Type u_3} [Field K] [Fintype ι] [Group Γ] [MulAction Γ ι] [Infinite K] [MulAction.IsPretransitive Γ ι] (εV εW : Γ → ι → K) (hε : ∀ (γ : Γ) (i : ι), εV γ i * εW γ i = 1) (V W : Submodule K (ι → K)) (hV : ∀ (γ : Γ), ∀ v ∈ V, (fun (i : ι) => εV γ i * v (γ⁻¹ • i)) ∈ V) (hW : ∀ (γ : Γ), ∀ w ∈ W, (fun (i : ι) => εW γ i * w (γ⁻¹ • i)) ∈ W) (hdim : Fintype.card ι < Module.finrank K ↥V + Module.finrank K ↥W) : Submodule.span K {f : ι → K | ∃ v ∈ V, ∃ w ∈ W, f = v * w} = ⊤

If V, W are stable under signed translations with dim V + dim W > |ι|, the pointwise products v * w span ι → K.