def AffineIsometryBuilding.IwahoriSubgroupIsometry (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) : Set C.GL_n_k

The Iwahori subgroup of the isometry group $\mathrm{Isom}(B) \subseteq GL_n(k)$: isometries that lie in $GL_n(\mathfrak{o})$ with unit diagonal entries and strictly-below-diagonal entries in $\mathfrak{m}$.

def AffineIsometryBuilding.IsAffineCn (numGen : ℕ) (m : Fin numGen → Fin numGen → ℕ) : Prop

Combinatorial characterisation of an affine Coxeter matrix of type $\tilde C_n$: symmetric matrix with diagonal $1$, edges of label $3$ along the interior of the diagram and label $4$ at both ends, all other pairs labelled $2$.

def AffineIsometryBuilding.IsAffineDn (numGen : ℕ) (m : Fin numGen → Fin numGen → ℕ) : Prop

Combinatorial characterisation of an affine Coxeter matrix of type $\tilde D_n$: symmetric matrix with diagonal $1$ and all off-diagonal labels in $\{2, 3\}$.

def AffineIsometryBuilding.IsAffineBn (numGen : ℕ) (m : Fin numGen → Fin numGen → ℕ) : Prop

Combinatorial characterisation of an affine Coxeter matrix of type $\tilde B_n$: symmetric, diagonal $1$, with at least one entry equal to $4$ and all off-diagonal labels in $\{2, 3, 4\}$.

def AffineIsometryBuilding.affineCnMatrix (n : ℕ) (_hn : n ≥ 2) : Fin (n + 1) → Fin (n + 1) → ℕ

Explicit construction of the affine $\tilde C_n$ Coxeter matrix on $n+1$ generators: labels $4$ on the two end edges, $3$ on interior edges, and $2$ elsewhere.

def AffineIsometryBuilding.affineDnMatrix (n : ℕ) (_hn : n ≥ 4) : Fin (n + 1) → Fin (n + 1) → ℕ

Explicit construction of the affine $\tilde D_n$ Coxeter matrix on $n+1$ generators: labels $3$ on the edges of the $\tilde D_n$ Dynkin diagram and $2$ elsewhere.

def AffineIsometryBuilding.affineBnMatrix (n : ℕ) (_hn : n ≥ 3) : Fin (n + 1) → Fin (n + 1) → ℕ

Explicit construction of the affine $\tilde B_n$ Coxeter matrix on $n+1$ generators: a single label-$4$ edge at the right end, label $3$ on the interior diagram, and $2$ elsewhere.

def AffineIsometryBuilding.AlternatingBuildingCoxeterType (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (_X : AffineAlternatingComplex C B) (wittIndex : ℕ) : Prop

The alternating-form building has affine Coxeter type $\tilde C_n$.

def AffineIsometryBuilding.DoubleOriflammeBuildingCoxeterType (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (halfDim : ℕ) (_X : DoubleOriflammeComplex C B halfDim) : Prop

The double oriflamme building has affine Coxeter type $\tilde D_n$.

def AffineIsometryBuilding.SingleOriflammeBuildingCoxeterType (C : DVRContext) (B : (Fin C.n → C.k) → (Fin C.n → C.k) → C.k) (_X : SingleOriflammeComplex C B) (wittIndex : ℕ) : Prop

The single oriflamme building has affine Coxeter type $\tilde B_n$.