Davis Regular Tessellations of Spheres and Straight Line Coxeter Groups In Davis' "Geometry and Topology of Coxeter Groups", section B.3, in particular Theorem B.3.1, there is a proof that every finite "straight line" Coxeter group is associated to a unique tessellation of the $(|S|-1)$-sphere up to isometry.
I will repeat/summarise the content from the textbook here, and include a tikz diagram I made. There is a finite Coxeter system $(W,S)$ with $S = \{s_0,s_1, \ldots, s_n\}$ and a Coxeter matrix $m_{ij}$ where the Coxeter diagram is a straight line. We know from a previous result that there is a spherial simplex $\sigma$ with $n+1$ many codimension one faces $\sigma_i$ such that $s_i$ is represented as a reflection across $\sigma_i$. In particular, the dihedral angles are correct. Davis then numbers the vertices according to the opposite face, so that $v_0$ is the vertex opposite $\sigma_0$
They consider the parabolic subgroup $W_{(i)}$ which is generated by all $s_j \in S$ with $j \neq i$, and consider the decomposition into the two irreducible Coxeter groups $W_{(i)} = G_i \times H_i$, where $G_i$ corresponds to the left side and $H_i$ the right side.
Denoting $\sigma(i)$ by the (simplicial) face of $\sigma$ spanned by $v_0, v_1, \ldots, v_i$, they define
$$ F_i = \bigcup_{w \in G_i} w \sigma(i),$$
which corresponds to the image of $\sigma(i)$ under the isotropy subgroup of $v_i$ (a subgroup of the isotropy group, really - although I think the idea is an induction so the interesting case to deal with is the top one??).
The claim is made (halfway down page 427) that two results

*

*$F_i$ is a convex spherical polytope in the $i$-sphere $\mathbb{S}^i$ fixed by $H_i$

*The triangulation of $F_i$ by the $i$-simplices $\{w\sigma(i)\}_{w \in W_{(i)}}$ is the barycentric subdivision

together implies that the $G_{i+1}$ translates of the $F_i$ are the cells of the regular tesselation.
My question:
I have no idea how these two results imply that. Here is a diagram of the result for the symmetric group $A_3$, in the case $i=2$, so $G_2 = A_2$ and $H_2 = 1$. The black sphere has lines on the sphere corresponding to the hyperplanes of the geometric representation of $A_3$, which gives the spherical simplex required. To be exact, the lines are the intersections of the hyperplanes with the sphere. The coloured image is a conformal projection (via the mercator projection) of the black 2-sphere onto a plane, like how many world maps do it. The three black dots are the vertices $v_0, v_1, v_2$ of the spherical simplex $\sigma(2)$. Each region bounded by lines represents a translate of $\sigma(2)$, and each colour represents $F_2$, or a $G_3 = A_3$ translate thereof.
Indeed, I can see that we do have a regular tesselation given by each coloured region, corresponding to the tetrahedron. But I have no idea how we can know that the translates actually tessellate the sphere, nor why it is regular.


 A: I believe I have figured it out. This might be wrong, so don't take this at face value. It also might be needlessly complex.
First we need to verify that the $F_i$ translates tessellate the sphere. That the $i$-simplices tessellate the sphere is easy to see - the $i$-simplex comes from the geometric representation, which gives us a tessellation with the right angles automatically (see Humphreys book on Coxeter groups for details on the geometric representation, and consider the intersection with a sphere). The issue is that we need the translates of $F_i$ to tessellate the sphere.
Although this isn't obvious, Björner's book Combinatorics of Coxeter Groups has a result (Cor 2.4.6)  which almost immediately solves this part. The result essentially states that, for every Coxeter group $(W,S)$ and subgroup $J \subseteq S$, every element $w \in W$ be uniquely represented as $w^J w_J$, where $w_J$ is in the parabolic subgroup $W_J$, and $w^J$ is such that for all $s \in J$, we have $l(w^Js) < l(w^J)$. This basically corresponds to the fact that if you take the Cayley graph of $W$ and delete the edges corresponding to all $s \notin J$, you get a bunch of disconnected copies of the parabolic subgroup, and every vertex is still connected to some edges, which is not too hard to see.
To apply this to the problem, we just need to notice that this tessellation of the sphere given by the translates of the simplices is the Coxeter complex, which corresponds to the Cayley graph. I can't quite see why this is true, but it feels like something that ought to be well known. Therefore, the translates of $F_i$ tessellate the sphere.
Davis already proved that an action on the chambers of a connected cell complex has to be free. So we actually only now need to prove that the action is transitive on the flags. But this is quite obvious - since the top dimensional cells are translates, of course there is a transitive action on the top dimensional cells. Moreover, there is also an action fixing $F_i$ that is transitive on the cells contained in $F_i$, because the only cells contained in $F_i$ are translates of the face $\sigma_i$.
Therefore we have a free and transitive action on the flags of the tessellation.
