def IsometryBuilding.IsotropicSubspace {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (W : Submodule k V) : Prop

A subspace $W \le V$ is totally isotropic for the bilinear form $B$ if $B(v,w) = 0$ for all $v, w \in W$.

structure IsometryBuilding.IsotropicFlag {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Type u_2

An isotropic flag for $B$: a strictly increasing chain $W_1 \subsetneq W_2 \subsetneq \cdots \subsetneq W_{\text{len}}$ of totally isotropic subspaces.

• len : ℕ
• chain : Fin self.len → Submodule k V
• chain_strictMono : StrictMono self.chain
• chain_isotropic (i : Fin self.len) : IsotropicSubspace B (self.chain i)

structure IsometryBuilding.IsotropicFlagComplex {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Type u_2

An isotropic flag complex: an abstract simplicial complex whose simplices are finite chains of totally isotropic subspaces of $(V, B)$, closed under nonempty subsets.

• simplices : Set (Finset (Submodule k V))
• simplex_isotropic (σ : Finset (Submodule k V)) : σ ∈ self.simplices → ∀ W ∈ σ, IsotropicSubspace B W
• simplex_chain (σ : Finset (Submodule k V)) : σ ∈ self.simplices → ∀ W₁ ∈ σ, ∀ W₂ ∈ σ, W₁ ≤ W₂ ∨ W₂ ≤ W₁
• face_closed (σ : Finset (Submodule k V)) : σ ∈ self.simplices → ∀ τ ⊆ σ, τ.Nonempty → τ ∈ self.simplices

structure IsometryBuilding.HyperbolicPair {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) : Type u_2

A hyperbolic pair $(e, e')$ for $B$: two isotropic vectors with $B(e, e') = 1$, spanning a hyperbolic plane.

• e : V
• e' : V
• pairing : (B self.e) self.e' = 1
• e_isotropic : (B self.e) self.e = 0
• e'_isotropic : (B self.e') self.e' = 0

structure IsometryBuilding.HyperbolicFrame {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

A hyperbolic frame of rank $n$ for $B$: $n$ pairwise-orthogonal hyperbolic pairs $\{(e_i, e_i')\}_{i < n}$ giving a Witt decomposition of an isotropic-rich subspace.

• pairs : Fin n → HyperbolicPair B
• orthogonal_ee (i j : Fin n) : i ≠ j → (B (self.pairs i).e) (self.pairs j).e = 0
• orthogonal_ee' (i j : Fin n) : i ≠ j → (B (self.pairs i).e) (self.pairs j).e' = 0
• orthogonal_e'e' (i j : Fin n) : i ≠ j → (B (self.pairs i).e') (self.pairs j).e' = 0

structure IsometryBuilding.Apartment {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

An apartment of rank $n$ in the isometry building: a hyperbolic frame together with the set of simplices it carries.

• frame : HyperbolicFrame B n
• simplices : Set (Finset (Submodule k V))

structure IsometryBuilding.IsBuilding {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

The data of a building structure on the isotropic flag complex of $(V,B)$: a family of apartments satisfying the common-apartment and apartment-exchange axioms (B1 and B2).

• complex : IsotropicFlagComplex B
• apartments : Set (Apartment B n)
• apartment_subcomplex (A : Apartment B n) : A ∈ self.apartments → A.simplices ⊆ self.complex.simplices
• common_apartment (σ₁ : Finset (Submodule k V)) : σ₁ ∈ self.complex.simplices → ∀ σ₂ ∈ self.complex.simplices, ∃ A ∈ self.apartments, σ₁ ∈ A.simplices ∧ σ₂ ∈ A.simplices
• apartment_exchange (A₁ : Apartment B n) : A₁ ∈ self.apartments → ∀ A₂ ∈ self.apartments, ∀ C ∈ A₁.simplices, C ∈ A₂.simplices → ∃ (f : Finset (Submodule k V) → Finset (Submodule k V)), Function.Bijective f ∧ (∀ σ ∈ A₁.simplices, f σ ∈ A₂.simplices) ∧ ∀ σ ∈ A₁.simplices ∩ A₂.simplices, f σ = σ

def IsometryBuilding.IsThick {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (bldg : IsBuilding B n) : Prop

A building is thick if every panel (codim-$1$ face of a chamber) is contained in at least three distinct chambers.

def IsometryBuilding.StronglyTransitive {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (bldg : IsBuilding B n) : Prop

A building is strongly transitive under the isometry group if for any two apartments $A_1, A_2$ and chambers $C_1 \in A_1$, $C_2 \in A_2$ there is an isometry of $(V,B)$ sending $A_1$ to $A_2$ and $C_1$ to $C_2$.

structure IsometryBuilding.IsometryBNPair {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) : Type u_2

A (B,N)-pair in the isometry group of $(V,B)$: data of a Borel-type subgroup stabilising a maximal isotropic flag, a frame-stabiliser playing the role of $N$, and a torus $T = B \cap N$, satisfying the standard compatibility properties.

• borel : Subgroup (V ≃ₗ[k] V)
• maxFlag : IsotropicFlag B
• borel_isometry (g : V ≃ₗ[k] V) : g ∈ self.borel → ∀ (v₁ v₂ : V), (B (g v₁)) (g v₂) = (B v₁) v₂
• borel_stabilizes (g : V ≃ₗ[k] V) : g ∈ self.borel → ∀ (i : Fin self.maxFlag.len), Submodule.map (↑g) (self.maxFlag.chain i) = self.maxFlag.chain i
• frameStab : Subgroup (V ≃ₗ[k] V)
• frame : HyperbolicFrame B n
• frameStab_isometry (g : V ≃ₗ[k] V) : g ∈ self.frameStab → ∀ (v₁ v₂ : V), (B (g v₁)) (g v₂) = (B v₁) v₂
• frameStab_permutes (g : V ≃ₗ[k] V) : g ∈ self.frameStab → ∀ (i : Fin n), ∃ (j : Fin n), g (self.frame.pairs i).e = (self.frame.pairs j).e ∨ g (self.frame.pairs i).e = (self.frame.pairs j).e'
• frameStab_permutes_e' (g : V ≃ₗ[k] V) : g ∈ self.frameStab → ∀ (i : Fin n), ∃ (j : Fin n), g (self.frame.pairs i).e' = (self.frame.pairs j).e ∨ g (self.frame.pairs i).e' = (self.frame.pairs j).e'
• torus : Subgroup (V ≃ₗ[k] V)
• torus_eq : ↑self.torus = ↑self.borel ∩ ↑self.frameStab

def IsometryBuilding.TypeCn (n : ℕ) (M : CoxeterMatrix (Fin n)) : Prop

The Coxeter matrix $M$ is of type $C_n$: diagonal entries are $1$, consecutive simple reflections satisfy $m_{i,i+1} = 3$ except the last pair which has $m_{n-2, n-1} = 4$, and all non-adjacent pairs commute ($m_{ij} = 2$).