def CoxeterMatrix.IsIndecomposable {B : Type u_1} (M : CoxeterMatrix B) : Prop

A Coxeter matrix is indecomposable if its Coxeter graph (with edges $\{s,t\}$ whenever $M_{st} \ne 2$) is connected: any partition of the generating set into two nonempty subsets is joined by a non-commuting generator pair.

noncomputable def CoxeterMatrix.cosineMatrix {B : Type u_1} (M : CoxeterMatrix B) : Matrix B B ℝ

The cosine matrix $C$ of a Coxeter matrix $M$: $C_{ij} = -\cos(\pi / M_{ij})$. This is the matrix of the standard symmetric bilinear form used to test sphericity/affineness of $M$.

noncomputable def CoxeterMatrix.IsAffine {B : Type u_1} (M : CoxeterMatrix B) : Prop

A Coxeter matrix $M$ is affine if its cosine matrix is positive semidefinite but not positive definite. This characterises the affine Coxeter types $\tilde A_n, \tilde B_n, \tilde C_n, \tilde D_n$, etc.

def Building.IsAffineBuilding {V : Type u_1} [DecidableEq V] (b : Building V) : Prop

A building is affine if it has a Coxeter type whose Coxeter matrix is indecomposable and affine.

def Building.IsTree {V : Type u_1} [DecidableEq V] (b : Building V) : Prop

A building is a tree if it is an affine building of rank one (a single generator), i.e. type $\tilde A_1$.

structure IwahoriSubgroup (G : Type u_2) [Group G] {B_idx : Type u_3} (M : CoxeterMatrix B_idx) : Type (max u_2 u_3)

The Iwahori subgroup of a group $G$ from a BN-pair with indecomposable affine Coxeter type: bundled data consisting of the BN-pair together with the indecomposable affine hypotheses on its Coxeter matrix.

• bnpair : BNPair G M
• indecomposable : M.IsIndecomposable
• affine : M.IsAffine

def IwahoriSubgroup.toSubgroup {G : Type u_2} [Group G] {B_idx : Type u_3} {M : CoxeterMatrix B_idx} (I : IwahoriSubgroup G M) : Subgroup G

The underlying subgroup of an Iwahori datum: the distinguished subgroup $B$ of the BN-pair.