Bases adapted to a finite descending filtration

A finite descending filtration of a finite-dimensional vector space admits a basis with positive integer weights: its k-th term consists exactly of vectors whose coordinates of weight at most k vanish. Equivalently, it is spanned by the basis vectors of weight greater than k.

This supplies adapted bases for filtrations such as the lower central series of a nilpotent Lie algebra. The construction uses Mathlib's Module.Basis.sumQuot to combine an adapted basis of the first positive-index term with a basis of its quotient. Repeated terms and the zero space are allowed.

theorem TauCeti.exists_basis_weight_of_antitone {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (F : ℕ → Submodule K V) (hF : Antitone F) (hzero : F 0 = ⊤) (N : ℕ) (hN : F N = ⊥) : ∃ (ι : Type) (x : Fintype ι) (b : Module.Basis ι K V) (w : ι → ℕ), (∀ (i : ι), 0 < w i ∧ w i ≤ N) ∧ ∀ (k : ℕ) (x : V), x ∈ F k ↔ ∀ (i : ι), w i ≤ k → (b.repr x) i = 0

A finite descending filtration admits a finite basis with positive bounded weights, in which membership in a filtration term is equivalent to the vanishing of all lower-weight coordinates.