@[reducible, inline]

abbrev GLnBuilding.Vec (k : Type u_1) (n : ℕ) : Type u_1

The ambient vector space $k^n$ realised as the function type $\mathrm{Fin}\ n \to k$.

structure GLnBuilding.FlagData : Type (max (u_2 + 1) (u_3 + 1))

Abstract data of a flag-like simplicial complex: a vertex type, a simplex type, and a function assigning to each simplex its finite set of vertices.

• vertex : Type u_2
• simplex : Type u_3
• verticesOf : self.simplex → Finset self.vertex

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

A simplex of the $\mathrm{GL}_n(k)$-building: a non-empty, strictly increasing chain of proper non-zero subspaces $0 \subsetneq V_1 \subsetneq \cdots \subsetneq V_r \subsetneq k^n$.

• chain : List (Submodule k (Vec k n))
• chain_nonempty : self.chain ≠ []
• chain_strictly_increasing : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) self.chain
• chain_proper (V : Submodule k (Vec k n)) : V ∈ self.chain → V ≠ ⊥ ∧ V ≠ ⊤

def GLnBuilding.IsChamber (k : Type u_1) [Field k] (n : ℕ) (F : SubspaceFlag k n) : Prop

A SubspaceFlag is a chamber iff its chain has length $n-1$, i.e.\ it is a maximal flag.

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

A frame of $k^n$: an ordered direct-sum decomposition $k^n = L_1 \oplus \cdots \oplus L_n$ into $n$ lines.

• lines : Fin n → Submodule k (Vec k n)
• one_dim (i : Fin n) : Module.finrank k ↥(self.lines i) = 1
• indep : iSupIndep self.lines
• spanning : ⨆ (i : Fin n), self.lines i = ⊤

def GLnBuilding.Frame.IsCompatible (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) (W : Submodule k (Vec k n)) : Prop

A subspace $W$ is compatible with the frame $F$ iff $W = \bigoplus_{i \in S} L_i$ for some $S \subseteq \{1,\dots,n\}$.

structure GLnBuilding.Apartment (k : Type u_1) [Field k] (n : ℕ) (F : Frame k n) : Type u_1

An apartment associated to the frame $F$: a flag every member of which is compatible with $F$.

• flag : SubspaceFlag k n
• compatible (V : Submodule k (Vec k n)) : V ∈ self.flag.chain → Frame.IsCompatible k n F V

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

The building axioms for the flag complex of $\mathrm{GL}_n(k)$: (i) every panel extends to two distinct chambers (thinness), (ii) any two flags lie in a common apartment, and (iii) two apartments sharing two chambers admit a compatibility-preserving isomorphism fixing both chambers.

• apartment_thin (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
• common_apartment (σ τ : SubspaceFlag k n) : ∃ (F : Frame k n), (∀ V ∈ σ.chain, Frame.IsCompatible k n F V) ∧ ∀ V ∈ τ.chain, Frame.IsCompatible k n F V
• apartment_iso (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

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

Data of a $BN$-pair for $\mathrm{GL}_n(k)$: a standard chamber, standard frame, and the subgroups $B$ and $N$ (encoded as sets of matrices).

• stdFlag : SubspaceFlag k n
• stdFlag_chamber : IsChamber k n self.stdFlag
• stdFrame : Frame k n
• B : Set (Matrix (Fin n) (Fin n) k)
• N : Set (Matrix (Fin n) (Fin n) k)

def GLnBuilding.TypeA (n : ℕ) (M : Matrix (Fin (n - 1)) (Fin (n - 1)) ℕ) : Prop

A Coxeter matrix is of type $A_{n-1}$ when its diagonal entries are $1$, off-diagonal entries lie in $\{2,3\}$, and it is symmetric.

def GLnBuilding.coxeterMatrixA (n : ℕ) : Matrix (Fin (n - 1)) (Fin (n - 1)) ℕ

The standard Coxeter matrix of type $A_{n-1}$: ones on the diagonal, threes on adjacent positions, twos elsewhere.

theorem GLnBuilding.typeA (n : ℕ) : TypeA n (coxeterMatrixA n)

The Coxeter matrix coxeterMatrixA n satisfies the type-$A$ predicate.