A linear Cauchy–Davenport bound over a full constant field

This file proves the specialization of the Hou–Leung–Xiang linear Kneser theorem needed for Clifford's theorem. If every element of K algebraic over k is constant, then nonzero finite dimensional k-subspaces A, B ⊆ K satisfy

finrank A + finrank B ≤ finrank (A * B) + 1.

The proof is the Dyson e-transform induction from Hou–Leung–Xiang. The full-constant-field hypothesis makes the stabilizer-field step direct and avoids a separate finite/infinite base-field split.

theorem FunctionField.exists_dyson_step (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsFullConstantField k K] (A B : Submodule k K) [FiniteDimensional k ↥B] (hA1 : 1 ∈ A) (hB1 : 1 ∈ B) (hAdim : 1 < Module.finrank k ↥A) : ∃ e ∈ B, e ≠ 0 ∧ A ⊓ Submodule.comap (LinearMap.mulRight k e) B ≠ A

If a finite-dimensional subspace A containing 1 has dimension bigger than one, some nonzero e ∈ B makes the Dyson intersection A ∩ B e⁻¹ proper.

theorem FunctionField.dyson_step (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsFullConstantField k K] (A B : Submodule k K) [FiniteDimensional k ↥A] [FiniteDimensional k ↥B] (hA1 : 1 ∈ A) (hB1 : 1 ∈ B) (hAdim : 1 < Module.finrank k ↥A) : ∃ (A' : Submodule k K) (B' : Submodule k K), 1 ∈ A' ∧ 1 ∈ B' ∧ A' < A ∧ A'.FG ∧ B'.FG ∧ Module.finrank k ↥A' + Module.finrank k ↥B' = Module.finrank k ↥A + Module.finrank k ↥B ∧ A' * B' ≤ A * B

One Dyson e-transform preserves the sum of dimensions, strictly decreases the first subspace, and does not enlarge the product space.

theorem FunctionField.normalized_mul_finrank (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsFullConstantField k K] (A B : Submodule k K) [FiniteDimensional k ↥A] [FiniteDimensional k ↥B] (hA1 : 1 ∈ A) (hB1 : 1 ∈ B) : Module.finrank k ↥A + Module.finrank k ↥B ≤ Module.finrank k ↥(A * B) + 1

The normalized linear Cauchy–Davenport bound, for subspaces containing 1.

theorem FunctionField.mul_finrank (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsFullConstantField k K] (A B : Submodule k K) [FiniteDimensional k ↥A] [FiniteDimensional k ↥B] (hA : A ≠ ⊥) (hB : B ≠ ⊥) : Module.finrank k ↥A + Module.finrank k ↥B ≤ Module.finrank k ↥(A * B) + 1

Linear Cauchy–Davenport over a full constant field. Nonzero finite-dimensional subspaces of K have product dimension at least the sum of their dimensions minus one.