def GLnBuilding.CompleteFlag.IsStrictFlag {k : Type u_1} [Field k] {n : ℕ} (σ : CompleteFlag k n) : Prop

A strict flag: a complete flag $\sigma$ in which each subspace $V_j$ has dimension exactly $j$, i.e., $\dim V_j = j$ for all $j$.

theorem GLnBuilding.CompleteFlag.IsStrictFlag.finrank_succ {k : Type u_1} [Field k] {n : ℕ} {σ : CompleteFlag k n} (hσ : σ.IsStrictFlag) (j : Fin n) : Module.finrank k ↥(σ.spaces ⟨↑j + 1, ⋯⟩) = Module.finrank k ↥(σ.spaces ⟨↑j, ⋯⟩) + 1

Consecutive subspaces in a strict flag differ by one dimension: $\dim V_{j+1} = \dim V_j + 1$.

theorem GLnBuilding.schreierCell_eq_sup {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (i : Fin (n + 1)) (hi : 0 < ↑i) (j : Fin (n + 1)) : schreierCell σ τ i hi j = σ.spaces ⟨↑i - 1, ⋯⟩ ⊔ σ.spaces i ⊓ τ.spaces j

Decomposition of the Schreier cell: $C_{i,j} = V_{i-1} + (V_i \cap W_j)$.

theorem GLnBuilding.schreierCell_finrank_step {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hτ : τ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) (j : Fin n) : Module.finrank k ↥(schreierCell σ τ i hi ⟨↑j + 1, ⋯⟩) ≤ Module.finrank k ↥(schreierCell σ τ i hi ⟨↑j, ⋯⟩) + 1

Step bound: along each column of the Schreier refinement, the dimension increases by at most $1$ when moving from $W_j$ to $W_{j+1}$.

theorem GLnBuilding.schreierCell_row_total {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (i : Fin (n + 1)) (hi : 0 < ↑i) : Module.finrank k ↥(schreierCell σ τ i hi ⟨n, ⋯⟩) = Module.finrank k ↥(schreierCell σ τ i hi ⟨0, ⋯⟩) + 1

Total row jump: in each row $i$ of the Schreier refinement, the dimension increases by exactly $1$ from the leftmost cell ($V_{i-1}$) to the rightmost ($V_i$).