structure GLnBuilding.LatticeChainRefinementHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: any finite list of proper subspaces of $k^n$ can be refined to a maximal proper chain $V_0 < V_1 < \cdots < V_{n-1}$ of length $n-1$ containing all the original subspaces.

• refine_via_chain (subs : List (Submodule k (Vec k n))) : (∀ V ∈ subs, V ≠ ⊥ ∧ V ≠ ⊤) → ∃ (chain : List (Submodule k (Vec k n))), (∀ V ∈ subs, V ∈ chain) ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain ∧ chain.length = n - 1 ∧ ∀ V ∈ chain, V ≠ ⊥ ∧ V ≠ ⊤

structure GLnBuilding.FlagToFrameHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: any complete strict flag of length $n-1$ of proper subspaces of $k^n$ extends to a frame $F$ (decomposition into lines) compatible with every member of the flag.

• flag_to_frame (chain : List (Submodule k (Vec k n))) : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain → chain.length = n - 1 → (∀ V ∈ chain, V ≠ ⊥ ∧ V ≠ ⊤) → ∃ (F : Frame k n), ∀ V ∈ chain, Frame.IsCompatible k n F V

noncomputable def GLnBuilding.simultaneousRefinementHyp (k : Type u_1) [Field k] (n : ℕ) (hchain : LatticeChainRefinementHyp k n) (hframe : FlagToFrameHyp k n) : SimultaneousRefinementHyp k n

Combining LatticeChainRefinementHyp and FlagToFrameHyp yields the simultaneous refinement hypothesis: any finite collection of proper subspaces lies in a common apartment frame.