Dimension growth in a one-point filtration

This file isolates the reusable linear-algebra step in the one-point filtration used in Stepanov-style arguments. If every element of a larger subspace is congruent modulo the preceding subspace to a scalar multiple of one pivot, then adjoining that pivot generates the larger subspace. Hence a single filtration step increases dimension by at most one.

theorem BGS.HasseWeil.eq_sup_span_singleton_of_exists_sub_smul_mem {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {S T : Submodule K L} {y : L} (hST : S ≤ T) (hy : y ∈ T) (hmod : ∀ x ∈ T, ∃ (c : K), x - c • y ∈ S) : T = S ⊔ K ∙ y

If every element of T is congruent modulo S to a scalar multiple of y, then T is generated by S and y.

theorem BGS.HasseWeil.moduleFinite_of_exists_sub_smul_mem {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {S T : Submodule K L} {y : L} (hST : S ≤ T) (hy : y ∈ T) (hmod : ∀ x ∈ T, ∃ (c : K), x - c • y ∈ S) [Module.Finite K ↥S] : Module.Finite K ↥T

A one-pivot extension of a finite-dimensional subspace is again finite-dimensional.

theorem BGS.HasseWeil.finrank_le_add_one_of_exists_sub_smul_mem {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] {S T : Submodule K L} {y : L} (hST : S ≤ T) (hy : y ∈ T) (hmod : ∀ x ∈ T, ∃ (c : K), x - c • y ∈ S) [Module.Finite K ↥S] : Module.finrank K ↥T ≤ Module.finrank K ↥S + 1

A one-pivot extension increases finrank by at most one.

theorem BGS.HasseWeil.onePointFiltration_moduleFinite_and_finrank_le {K : Type u_1} {L : Type u_2} [Field K] [AddCommGroup L] [Module K L] (R : ℕ → Submodule K L) (y : ℕ → L) (hnested : ∀ (n : ℕ), R n ≤ R (n + 1)) (hpivot : ∀ (n : ℕ), y n ∈ R (n + 1)) (hmod : ∀ (n : ℕ), ∀ x ∈ R (n + 1), ∃ (c : K), x - c • y n ∈ R n) [Module.Finite K ↥(R 0)] (n : ℕ) : Module.Finite K ↥(R n) ∧ Module.finrank K ↥(R n) ≤ Module.finrank K ↥(R 0) + n

Along a nested filtration whose successive quotients are generated by one pivot, every stage is finite-dimensional and stage n has finrank at most the initial finrank plus n.