structure GLnBuilding.CompleteFlag (k : Type u_2) [Field k] (n : ℕ) : Type u_2

• spaces : Fin (n + 1) → Submodule k (Vec k n)
• monotone : Monotone self.spaces
• bot_eq : self.spaces ⟨0, ⋯⟩ = ⊥
• top_eq : self.spaces ⟨n, ⋯⟩ = ⊤

def GLnBuilding.schreierCell {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (i : Fin (n + 1)) (hi : 0 < ↑i) (j : Fin (n + 1)) : Submodule k (Vec k n)

The Schreier refinement cell at row $i$ and column $j$: $\sigma_i \cap (\sigma_{i-1} + \tau_j)$, interpolating between $\sigma_{i-1}$ and $\sigma_i$ along the chain $\tau$.

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

At column $0$, the Schreier cell collapses to $\sigma_{i-1}$.

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

At the last column, the Schreier cell equals $\sigma_i$.

theorem GLnBuilding.schreierCell_mono {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (i : Fin (n + 1)) (hi : 0 < ↑i) (j j' : Fin (n + 1)) (hjj' : j ≤ j') : schreierCell σ τ i hi j ≤ schreierCell σ τ i hi j'

Monotonicity of Schreier cells in the column index $j$.