def CoxeterComplex.ChamberAdjacent {B : Type u_1} (M : CoxeterMatrix B) (w w' : M.Group) : Prop

Two elements $w, w'$ of the Coxeter group $W$ are chamber-adjacent when $w \neq w'$ and $w' = w \cdot s_i$ for some simple generator $s_i$.

def CoxeterComplex.IsGallery {B : Type u_1} (M : CoxeterMatrix B) : List M.Group → Prop

A list of group elements is a gallery in the Coxeter complex iff consecutive entries are chamber-adjacent.

structure CoxeterComplex.Simplex {B : Type u_1} (M : CoxeterMatrix B) : Type u_1

A simplex in the Coxeter complex of $M$: a chamber representative $w \in W$ together with a subset of simple generators determining the standard parabolic.

• rep : M.Group
• subset : Finset B

def CoxeterComplex.Simplex.IsFaceOf {B : Type u_1} (M : CoxeterMatrix B) (σ τ : Simplex M) : Prop

Face relation between simplices: $\tau$ is a face of $\sigma$ when its index-set is contained in $\sigma$'s and $\sigma^{-1}\tau$ lies in the parabolic subgroup generated by $\sigma$'s simples.

theorem CoxeterComplex.chamberAdjacent_irrefl {B : Type u_1} (M : CoxeterMatrix B) (w : M.Group) : ¬ChamberAdjacent M w w

Chamber adjacency is irreflexive: $w$ is never adjacent to itself.

theorem CoxeterComplex.isGallery_nil {B : Type u_1} (M : CoxeterMatrix B) : IsGallery M []

The empty list is trivially a gallery.

theorem CoxeterComplex.isGallery_singleton {B : Type u_1} (M : CoxeterMatrix B) (w : M.Group) : IsGallery M [w]

A singleton list is trivially a gallery.

theorem CoxeterComplex.isGallery_cons {B : Type u_1} (M : CoxeterMatrix B) (w w' : M.Group) (rest : List M.Group) (h : IsGallery M (w :: w' :: rest)) : ChamberAdjacent M w w' ∧ IsGallery M (w' :: rest)

Destructor: a gallery of length $\geq 2$ decomposes as an adjacent first edge and a tail gallery.

theorem CoxeterComplex.Simplex.isFaceOf_refl {B : Type u_1} (M : CoxeterMatrix B) (σ : Simplex M) : IsFaceOf M σ σ

Reflexivity of the face relation: every simplex is a face of itself.