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

Hypothesis: every panel (codimension-1 flag) extends to two distinct chambers, both containing the panel — i.e.\ the apartment is thin.

• extend_panel (F : Frame k n) (panel : SubspaceFlag k n) : (∀ V ∈ panel.chain, Frame.IsCompatible k n F V) → panel.chain.length = n - 2 → ∃ (C₁ : SubspaceFlag k n) (C₂ : SubspaceFlag k n), IsChamber k n C₁ ∧ IsChamber k n C₂ ∧ C₁ ≠ C₂ ∧ (∀ V ∈ panel.chain, V ∈ C₁.chain) ∧ (∀ V ∈ panel.chain, V ∈ C₂.chain) ∧ ∀ V ∈ panel.chain, V ∈ C₁.chain ∧ V ∈ C₂.chain

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

Hypothesis: any two flags $\sigma,\tau$ lie inside the apartment of a common frame $F$.

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

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

Hypothesis: two apartments containing a common pair of chambers $C_1,C_2$ admit a bijective compatibility-preserving map fixing every member of $C_1.\mathrm{chain}$ and $C_2.\mathrm{chain}$.

• iso_apartments (F₁ F₂ : Frame k n) (C₁ C₂ : SubspaceFlag k n) : IsChamber k n C₁ → IsChamber k n C₂ → (∀ V ∈ C₁.chain, Frame.IsCompatible k n F₁ V) → (∀ V ∈ C₂.chain, Frame.IsCompatible k n F₁ V) → (∀ V ∈ C₁.chain, Frame.IsCompatible k n F₂ V) → (∀ V ∈ C₂.chain, Frame.IsCompatible k n F₂ V) → ∃ (f : Submodule k (Vec k n) → Submodule k (Vec k n)), Function.Bijective f ∧ (∀ (V : Submodule k (Vec k n)), Frame.IsCompatible k n F₁ V → Frame.IsCompatible k n F₂ (f V)) ∧ (∀ V ∈ C₁.chain, f V = V) ∧ ∀ V ∈ C₂.chain, f V = V

noncomputable def GLnBuilding.glnIsBuilding (k : Type u_1) [Field k] (n : ℕ) (h_thin : ThinApartmentHyp k n) (h_common : CommonApartmentHyp k n) (h_iso : ApartmentIsoHyp k n) : IsBuilding k n

Assembling the three hypotheses (thin apartments, common apartment, apartment iso) into the building structure for $\mathrm{GL}_n(k)$.