theorem GLnBuilding.CompleteFlag.IsStrictFlag.spaces_lt {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (i : Fin n) : σ.spaces ⟨↑i, ⋯⟩ < σ.spaces ⟨↑i + 1, ⋯⟩

Strict flags are strictly increasing: $V_i \subsetneq V_{i+1}$.

noncomputable def GLnBuilding.CompleteFlag.IsStrictFlag.gapVector {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (i : Fin n) : Vec k n

Choice of a gap vector at step $i$ of a strict flag: a vector in $V_{i+1} \setminus V_i$.

theorem GLnBuilding.CompleteFlag.IsStrictFlag.gapVector_mem {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (i : Fin n) : hσ.gapVector i ∈ σ.spaces ⟨↑i + 1, ⋯⟩

The gap vector lies in $V_{i+1}$.

theorem GLnBuilding.CompleteFlag.IsStrictFlag.gapVector_not_mem {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (i : Fin n) : hσ.gapVector i ∉ σ.spaces ⟨↑i, ⋯⟩

The gap vector does not lie in $V_i$.

theorem GLnBuilding.CompleteFlag.IsStrictFlag.gapVector_ne_zero {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (i : Fin n) : hσ.gapVector i ≠ 0

The gap vector is nonzero.

theorem GLnBuilding.CompleteFlag.IsStrictFlag.gapVector_mem_of_le {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (i : Fin n) (j : Fin (n + 1)) (hij : ↑i + 1 ≤ ↑j) : hσ.gapVector i ∈ σ.spaces j

Monotonicity: if $i + 1 \le j$ then the $i$-th gap vector lies in $V_j$.

theorem GLnBuilding.CompleteFlag.IsStrictFlag.linearIndependent_gapVectors {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) : LinearIndependent k fun (i : Fin n) => hσ.gapVector i

The $n$ gap vectors $\{v_i\}_{i < n}$ of a strict flag are linearly independent.

theorem GLnBuilding.CompleteFlag.IsStrictFlag.span_gapVectors_eq_top {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) [FiniteDimensional k (Vec k n)] : Submodule.span k (Set.range fun (i : Fin n) => hσ.gapVector i) = ⊤

The gap vectors span all of $k^n$, hence form a basis.

noncomputable def GLnBuilding.refinementFrame {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) [FiniteDimensional k (Vec k n)] : Frame k n

The refinement frame of a strict flag: the apartment frame whose lines are spanned by the gap vectors $v_i$, giving an apartment containing $\sigma$ as a chamber.

noncomputable def GLnBuilding.refinementFrameFromPair {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (_hτ : τ.IsStrictFlag) [FiniteDimensional k (Vec k n)] : Frame k n

Wrapper: the refinement frame of a strict flag $\sigma$, ignoring a second flag $\tau$.