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

The $i$-th Jordan-Hölder line vector for two complete strict flags $\sigma, \tau$: a nonzero vector representing the gap $V_{i+1}/V_i$ in the Schreier refinement of $\sigma$ by $\tau$.

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

The Jordan-Hölder line vector $\ell_i$ lies in $V_{i+1}$ of the flag $\sigma$.

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

The Jordan-Hölder line vector $\ell_i$ does not lie in $V_i$, i.e., it realizes a genuine dimension jump.

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

Each Jordan-Hölder line vector is nonzero.

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

Monotonicity: if $i + 1 \le j$ then $\ell_i \in V_j$.

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

The Jordan-Hölder line vectors $\{\ell_i\}_{i < n}$ are linearly independent in $k^n$.

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

The span of the $n$ Jordan-Hölder line vectors equals all of $k^n$.

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

The Jordan-Hölder frame of two complete flags $\sigma, \tau$: the apartment frame whose lines are spanned by the Jordan-Hölder gap vectors $\ell_i$, simultaneously refining both flags.

theorem GLnBuilding.jordanHolderFrame_compatible_sigma {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) [FiniteDimensional k (Vec k n)] (i : Fin (n + 1)) : Frame.IsCompatible k n (jordanHolderFrame σ τ hσ hτ) (σ.spaces i)

The Jordan-Hölder frame is compatible with the flag $\sigma$: each subspace $V_i$ of $\sigma$ is a sum of frame lines, namely $V_i = \bigoplus_{j < i} k \cdot \ell_j$.