theorem GLnBuilding.isChain_getElem_lt {α : Type u_2} [Preorder α] {l : List α} (hc : List.IsChain (fun (x1 x2 : α) => x1 < x2) l) {i j : ℕ} (hi : i < l.length) (hj : j < l.length) (hij : i < j) : l[i] < l[j]

In a strictly increasing list, indexed elements at strictly increasing positions are strictly increasing.

noncomputable def GLnBuilding.chamberToCompleteFlag {k : Type u_1} [Field k] {n : ℕ} (σ : SubspaceFlag k n) (hchamber : IsChamber k n σ) (hn : n ≥ 2) : CompleteFlag k n

Convert a chamber (maximal SubspaceFlag) into the corresponding CompleteFlag indexed by $\mathrm{Fin}(n+1)$, where $\mathrm{spaces}\ 0 = \bot$ and $\mathrm{spaces}\ n = \top$.

theorem GLnBuilding.chamberToCompleteFlag_isStrictFlag {k : Type u_1} [Field k] {n : ℕ} (σ : SubspaceFlag k n) (hchamber : IsChamber k n σ) (hn : n ≥ 2) : (chamberToCompleteFlag σ hchamber hn).IsStrictFlag

The complete flag produced from a chamber is strict: $\dim_k(\mathrm{spaces}\ i) = i$ for every $i \in \mathrm{Fin}(n+1)$.

theorem GLnBuilding.chamberToCompleteFlag_contains {k : Type u_1} [Field k] {n : ℕ} (σ : SubspaceFlag k n) (hchamber : IsChamber k n σ) (hn : n ≥ 2) (V : Submodule k (Vec k n)) (hV : V ∈ σ.chain) : ∃ (i : Fin (n + 1)), (chamberToCompleteFlag σ hchamber hn).spaces i = V

Every subspace appearing in the chamber's chain appears as spaces i of the associated complete flag.

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

Symmetry of Schreier cell increments: swapping $(σ,τ)$ with $(τ,σ)$ and $(i,j)$ with $(j,i)$ preserves the dimension increment $\dim(\mathrm{cell}_{ij}) - \dim(\mathrm{cell}_{i,j-1})$.

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

The jump-column function transposes under swapping the two flags: a jump at position $(i,j)$ in $(σ,τ)$ corresponds to a jump at $(j+1,i-1)$ in $(τ,σ)$.

theorem GLnBuilding.jumpCol_injective {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) : Function.Injective fun (i : Fin n) => jumpCol σ τ hσ hτ ⟨↑i + 1, ⋯⟩ ⋯

The jump-column map $i \mapsto \mathrm{jumpCol}(i+1)$ from $\mathrm{Fin}\ n$ to $\mathrm{Fin}\ n$ is injective; the Jordan–Hölder lines are indexed bijectively.

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

If $\mathrm{jumpCol}(i+1) + 1 \le j$, then the Jordan–Hölder line $\mathrm{jhLine}\ i$ already lies inside $τ.\mathrm{spaces}\ j$.

noncomputable def GLnBuilding.tauWitness {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (j : Fin (n + 1)) : Finset (Fin n)

The set of indices $i$ whose Jordan–Hölder line lies inside $τ.\mathrm{spaces}\ j$, defined via $\mathrm{jumpCol}(i+1) < j$.

theorem GLnBuilding.card_tauWitness_eq {k : Type u_1} [Field k] {n : ℕ} (σ τ : CompleteFlag k n) (hσ : σ.IsStrictFlag) (hτ : τ.IsStrictFlag) (j : Fin (n + 1)) : (tauWitness σ τ hσ hτ j).card = ↑j

The cardinality $|\mathrm{tauWitness}\ \sigma\ \tau\ j| = j$, by bijectivity of the jump-column map.

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

The Jordan–Hölder frame is compatible with every $τ.\mathrm{spaces}\ j$, i.e.
$τ.\mathrm{spaces}\ j = \bigoplus_{i \in \mathrm{tauWitness}\ j} \mathrm{jhLine}\ i$.

theorem GLnBuilding.no_proper_nonzero_subspace_of_le_one' {k : Type u_1} [Field k] {n : ℕ} (hn : n ≤ 1) (V : Submodule k (Vec k n)) (hbot : V ≠ ⊥) (htop : V ≠ ⊤) : False

If $n \le 1$, then $k^n$ has no proper non-zero subspaces.

theorem GLnBuilding.subspaceFlag_empty_of_le_one' {k : Type u_1} [Field k] {n : ℕ} (hn : n ≤ 1) (σ : SubspaceFlag k n) : False

If $n \le 1$, no SubspaceFlag k n exists (the chain would require a proper non-zero subspace, which is impossible).

noncomputable def GLnBuilding.twoChamberFrameHypUnconditional (k : Type u_1) [Field k] (n : ℕ) (hn : n ≥ 2) : TwoChamberFrameHyp k n

Main: any two chambers $σ, τ$ admit a common frame, namely the Jordan–Hölder frame of their associated complete flags.

noncomputable def GLnBuilding.commonApartmentHypUnconditional (k : Type u_1) [Field k] (n : ℕ) : CommonApartmentHyp k n

The common-apartment property holds unconditionally for $\mathrm{GL}_n(k)$: any two flags lie in the apartment of some frame. The case $n \le 1$ is vacuous.