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

Hypothesis: any two chambers $\sigma, \tau$ admit a common adapted frame $F$ — i.e.\ a frame compatible with every subspace appearing in either chamber's chain.

• frame_of_two_chambers (σ τ : SubspaceFlag k n) : IsChamber k n σ → IsChamber k n τ → ∃ (F : Frame k n), (∀ V ∈ σ.chain, Frame.IsCompatible k n F V) ∧ ∀ V ∈ τ.chain, Frame.IsCompatible k n F V

theorem GLnBuilding.intermediate_submodule {k : Type u_1} [Field k] {M : Type u_2} [AddCommGroup M] [Module k M] [FiniteDimensional k M] {V W : Submodule k M} (hVW : V < W) (hgap : Module.finrank k ↥V + 2 ≤ Module.finrank k ↥W) : ∃ (U : Submodule k M), V < U ∧ U < W ∧ Module.finrank k ↥U = Module.finrank k ↥V + 1

Between two subspaces $V < W$ with a dimension gap of at least $2$, there is a strictly intermediate subspace $U$ with $V < U < W$ and $\dim U = \dim V + 1$.

theorem GLnBuilding.insertIdx_eq_take_drop {α : Type u_2} (l : List α) (i : ℕ) (a : α) (hi : i ≤ l.length) : l.insertIdx i a = List.take i l ++ a :: List.drop i l

List.insertIdx decomposed as take ++ a :: drop.

theorem GLnBuilding.pairwise_insertIdx {α : Type u_2} {R : α → α → Prop} {l : List α} {a : α} {i : ℕ} (hi : i ≤ l.length) (hpw : List.Pairwise R l) (hleft : ∀ x ∈ List.take i l, R x a) (hright : ∀ x ∈ List.drop i l, R a x) : List.Pairwise R (l.insertIdx i a)

List.insertIdx preserves Pairwise R given the appropriate relations to elements before and after the insertion point.

theorem GLnBuilding.le_getLast_of_mem_pairwise {α : Type u_2} [Preorder α] {l : List α} (hpw : List.Pairwise (fun (x1 x2 : α) => x1 < x2) l) (hne : l ≠ []) {a : α} (ha : a ∈ l) : a ≤ l.getLast hne

In a pairwise strictly-increasing non-empty list, every element is $\le$ the last.

theorem GLnBuilding.head_le_of_mem_pairwise {α : Type u_2} [Preorder α] {l : List α} (hpw : List.Pairwise (fun (x1 x2 : α) => x1 < x2) l) (hne : l ≠ []) {a : α} (ha : a ∈ l) : l.head hne ≤ a

In a pairwise strictly-increasing non-empty list, the head is $\le$ every element.

theorem GLnBuilding.extend_flag_chain {k : Type u_1} [Field k] (n : ℕ) (chain : List (Submodule k (Vec k n))) (hne : chain ≠ []) (hchain : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain) (hproper : ∀ V ∈ chain, V ≠ ⊥ ∧ V ≠ ⊤) (hshort : chain.length < n - 1) : ∃ (chain' : List (Submodule k (Vec k n))), chain'.length = chain.length + 1 ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain' ∧ (∀ V ∈ chain', V ≠ ⊥ ∧ V ≠ ⊤) ∧ chain'.length ≤ n - 1 ∧ ∀ V ∈ chain, V ∈ chain'

Any non-empty strict chain of proper subspaces of length $< n-1$ can be extended by one proper subspace, either at the front, back, or in the middle, while staying a proper chain.

theorem GLnBuilding.flag_completion {k : Type u_1} [Field k] (n : ℕ) (hn : n ≥ 2) (chain : List (Submodule k (Vec k n))) (hne : chain ≠ []) (hchain : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain) (hproper : ∀ V ∈ chain, V ≠ ⊥ ∧ V ≠ ⊤) : ∃ (chain' : List (Submodule k (Vec k n))), chain'.length = n - 1 ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain' ∧ (∀ V ∈ chain', V ≠ ⊥ ∧ V ≠ ⊤) ∧ ∀ V ∈ chain, V ∈ chain'

Any non-empty chain of proper subspaces in $k^n$ ($n \ge 2$) can be completed to a maximal flag of length exactly $n-1$ containing the original chain.

noncomputable def GLnBuilding.commonApartmentFromHyps {k : Type u_1} [Field k] (n : ℕ) (hn : n ≥ 2) (h : TwoChamberFrameHyp k n) : CommonApartmentHyp k n

Combine the two-chamber frame hypothesis with flag completion to deduce the common-apartment property: any two flags $\sigma, \tau$ lie in a common apartment, by first completing each to a chamber and then applying TwoChamberFrameHyp.