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

The standard isotropic flag complex of $(V, B)$: simplices are finite chains $W_1 \le W_2 \le \cdots$ of totally isotropic subspaces with respect to the bilinear form $B$.

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

The standard apartments of the isometry building, indexed by hyperbolic frames of $(V,B)$ of rank $n$. Each apartment carries the full set of isotropic chains as its simplices.

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

Hypothesis: for any two isotropic simplices $\sigma_1, \sigma_2$ in the standard complex, there exists a standard apartment containing both.

• find_common (σ₁ : Finset (Submodule k V)) : σ₁ ∈ (standardComplex B).simplices → ∀ σ₂ ∈ (standardComplex B).simplices, ∃ A ∈ standardApartments B n, σ₁ ∈ A.simplices ∧ σ₂ ∈ A.simplices

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

Hypothesis: whenever two apartments $A_1, A_2$ share a chamber $C$, there is a bijection $f : A_1 \to A_2$ of their simplices fixing every simplex in $A_1 \cap A_2$.

• exchange (A₁ : Apartment B n) : A₁ ∈ standardApartments B n → ∀ A₂ ∈ standardApartments B n, ∀ 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 σ = σ

noncomputable def IsometryBuilding.isometryIsBuilding {k : Type u_1} [CommRing k] {V : Type u_2} [AddCommGroup V] [Module k V] (B : LinearMap.BilinForm k V) (n : ℕ) (h_common : CommonIsotropicApartmentHyp B n) (h_exchange : ApartmentExchangeHyp B n) : IsBuilding B n

The isometry building: assembles standardComplex and standardApartments into an IsBuilding structure, given the common-apartment and apartment-exchange hypotheses.