Chamber Complexes, Coxeter Systems, and Buildings


Title: Chamber Complexes, Coxeter Systems, and Buildings
Author: Jeremy Sylvestre
Submission date: 2016-07-01
Abstract: We provide a basic formal framework for the theory of chamber complexes and Coxeter systems, and for buildings as thick chamber complexes endowed with a system of apartments. Along the way, we develop some of the general theory of abstract simplicial complexes and of groups (relying on the group_add class for the basics), including free groups and group presentations, and their universal properties. The main results verified are that the deletion condition is both necessary and sufficient for a group with a set of generators of order two to be a Coxeter system, and that the apartments in a (thick) building are all uniformly Coxeter.
  author  = {Jeremy Sylvestre},
  title   = {Chamber Complexes, Coxeter Systems, and Buildings},
  journal = {Archive of Formal Proofs},
  month   = jul,
  year    = 2016,
  note    = {\url{},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License