noncomputable def GLnBuilding.stdFlagSubspace (k : Type u_1) [Field k] (n : ℕ) (i : Fin (n - 1)) : Submodule k (Vec k n)

The $i$-th subspace of the standard flag: the span of the first $i+1$ standard basis vectors in $k^n$.

theorem GLnBuilding.stdFlagSubspace_generators_linIndep (k : Type u_1) [Field k] (n : ℕ) (i : Fin (n - 1)) : LinearIndependent k fun (j : Fin (↑i + 1)) => (Pi.basisFun k (Fin n)) ⟨↑j, ⋯⟩

The chosen generators of stdFlagSubspace k n i are linearly independent.

theorem GLnBuilding.stdFlagSubspace_finrank (k : Type u_1) [Field k] (n : ℕ) (i : Fin (n - 1)) : Module.finrank k ↥(stdFlagSubspace k n i) = ↑i + 1

$\dim_k(\mathrm{stdFlagSubspace}\ k\ n\ i) = i + 1$.

theorem GLnBuilding.stdFlagSubspace_mono (k : Type u_1) [Field k] (n : ℕ) {i j : Fin (n - 1)} (h : i ≤ j) : stdFlagSubspace k n i ≤ stdFlagSubspace k n j

Standard flag subspaces are monotone in the index.

theorem GLnBuilding.stdFlagSubspace_strictMono (k : Type u_1) [Field k] (n : ℕ) {i j : Fin (n - 1)} (h : i < j) : stdFlagSubspace k n i < stdFlagSubspace k n j

Standard flag subspaces are strictly monotone in the index.

theorem GLnBuilding.stdFlagSubspace_ne_bot (k : Type u_1) [Field k] (n : ℕ) (i : Fin (n - 1)) : stdFlagSubspace k n i ≠ ⊥

Each standard flag subspace is non-zero.

theorem GLnBuilding.stdFlagSubspace_ne_top (k : Type u_1) [Field k] (n : ℕ) (i : Fin (n - 1)) : stdFlagSubspace k n i ≠ ⊤

Each standard flag subspace is a proper subspace of $k^n$.

noncomputable def GLnBuilding.stdFlagChain (k : Type u_1) [Field k] (n : ℕ) : List (Submodule k (Vec k n))

The complete standard flag in $k^n$ as a list of subspaces of length $n-1$.

theorem GLnBuilding.stdFlagChain_length (k : Type u_1) [Field k] (n : ℕ) : (stdFlagChain k n).length = n - 1

The standard flag chain has length $n-1$.

theorem GLnBuilding.stdFlagChain_isChain (k : Type u_1) [Field k] (n : ℕ) : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) (stdFlagChain k n)

The standard flag chain is strictly increasing.

theorem GLnBuilding.stdFlagChain_proper (k : Type u_1) [Field k] (n : ℕ) (V : Submodule k (Vec k n)) : V ∈ stdFlagChain k n → V ≠ ⊥ ∧ V ≠ ⊤

Every subspace in the standard flag chain is proper and non-zero.

noncomputable def GLnBuilding.baseFlagHyp (k : Type u_1) [Field k] (n : ℕ) : BaseFlagHyp k n

The standard flag witnesses the existence of a BaseFlagHyp k n, providing a fixed maximal flag to which we may refine arbitrary subspaces.