LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite Coxeter orbit polytopes, face isometries and their cocycle

Statement

Let $(S, m)$ be a Coxeter matrix with $S$ finite, $W$ its presented group (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups) with Coxeter form $B$ on $V = R^{S}$ and reflection representation $ρ$ (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone), and let $(d_{s})_{s \in S}$ be positive real numbers. For $T \in S$ (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization) put $V_{T} : = span {e_{s} : s \in T}$ (Linear subspace of a vector space, Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ); since $(W_{T}, T)$ is a Coxeter system of finite type (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2)) with $W_{T}$ finite, the restriction of $B$ to $V_{T}$ is positive definite by Finiteness criterion: W is finite exactly when the Coxeter form is positive definite (1), so $B_{T} : = B ∣_{V_{T}}$ is an inner product (Real and complex inner-product spaces and their induced length). Let $v_{s}^{(T)} \in V_{T}$ ( $s \in T$ ) be its $B$ -dual basis, and put $x_{T} : = \sum_{s \in T} d_{s} v_{s}^{(T)} \in V_{T}, C_{T} : = conv (W_{T} x_{T}) \subseteq V_{T} .$

(1) Cells. For every spherical $T$ , $C_{T}$ is a compact convex polyhedral cell of dimension $∣ T ∣$ inside the Euclidean affine space $(V_{T}, B_{T})$ with $0$ in its interior, a compact convex polyhedral cell in the sense of Finite convex cell complex and linear subdivision, and its nonempty faces are exactly the sets $conv (u W_{U} x_{T})$ , $u \in W_{T}$ , $U \subseteq T$ , each occurring for exactly one coset $u W_{U}$ ; face inclusion agrees with coset inclusion (and the simultaneously reversed face and coset orders also agree). The remaining face is $\emptyset$ , which has no coset index. This is The finite-type Coxeter cell: exposed faces and normal cones applied to the finite-type system $(W_{T}, T)$ and the point $x_{T}$ in the open fundamental chamber ${v \in V_{T} : B (v, e_{s}) > 0 for all s \in T}$ , whose distances to the simple mirrors are $B (x_{T}, e_{s}) = d_{s}$ .

(2) Projections. For $U \subseteq T$ , the $B$ -orthogonal projection of $x_{T}$ onto $V_{U}$ is $x_{U}$ ; equivalently $x_{T} = x_{U} + z_{T, U}$ with $z_{T, U} \in V_{U}^{⊥} \cap V_{T}$ , and $z_{T, U}$ is fixed by $ρ (W_{U})$ . In particular $x_{U}$ depends only on $U$ and on the numbers $d_{s}$ with $s \in U$ .

(3) Face isometries. For $U \subseteq T$ and $w \in W_{T}$ , the affine map $φ_{w}^{T, U} ⁣ : V_{U} \to V_{T}, φ (v) = ρ (w) (v + z_{T, U}),$ is a Euclidean isometry of $(V_{U}, B_{U})$ onto the affine span of the face $conv (w W_{U} x_{T})$ and carries $C_{U}$ onto that face. Hence the intrinsic metric of the face $conv (w W_{U} x_{T})$ of $C_{T}$ equals that of $C_{U}$ , and depends only on $U$ , the numbers $d_{s}$ ( $s \in U$ ) and no other choice.

(4) Cocycle. For spherical $U \subseteq T \subseteq T^{'}$ and $g_{1} \in W_{T}$ , $g_{2} \in W_{T^{'}}$ one has $φ_{g_{2} g_{1}}^{T^{'}, U} = φ_{g_{2}}^{T^{'}, T} \circ φ_{g_{1}}^{T, U},$ an identity of isometries $V_{U} \to V_{T^{'}}$ ; consequently the face identifications of the cells $C_{T}$ are compatible on common faces and satisfy the cocycle condition of a gluing (Abstract isometric polyhedral gluings and the chain metric).

Facts & Assumptions

Given: A finite Coxeter matrix $(S, m)$ , its presented group $W$ , the form $B$ and representation $ρ$ on $V = R^{S}$ , positive numbers $(d_{s})_{s \in S}$ , and for each spherical $T$ the space $V_{T}$ with the form $B_{T} = B ∣_{V_{T}}$ , the dual basis $v_{s}^{(T)}$ , the point $x_{T}$ and the cell $C_{T} = conv (W_{T} x_{T})$ .

[F1]

The cell lemma: for a finite-type Coxeter system acting on its positive definite reflection space, the orbit polytope of a point of the open chamber is a compact convex polyhedral cell with the listed nonempty faces, norms and cell description (The finite-type Coxeter cell: exposed faces and normal cones (1)-(5)); the term compact convex polyhedral cell has the definition in Finite convex cell complex and linear subdivision.

[F2]

For spherical $T$ (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)), $(W_{T}, T)$ is a Coxeter system of finite type, $W_{T} \cap S = T$ , and $B_{T}$ is positive definite; the restriction $ρ ∣_{W_{T}}$ is the canonical reflection representation of the subsystem acting on $V_{T}$ with basis $(e_{s})_{s \in T}$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2), Finiteness criterion: W is finite exactly when the Coxeter form is positive definite (1), The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone).

[F3]

For every $U \subseteq S$ and $u \in W_{U}$ one has $ρ (u) V_{U} = V_{U}$ ; every $ρ (w)$ preserves $B$ ; and for $s \in S$ the reflection formula gives $ρ (s) v = v - 2 B (v, e_{s}) e_{s}$ (Intersections of standard parabolics, the parabolic root subsystem, and global minimality of coset representatives (2), Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2), The canonical reflection homomorphism, roots, reflections, and the positive cone (1), The real Coxeter form, its radical, reflections, and form-preserving maps (3)).

[F4]

The coordinate vectors $(e_{s})_{s \in T}$ form a basis of $V_{T}$ ; their coordinate functionals $e_{s}^{*}$ are the dual family (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ ). The finite-dimensional Riesz theorem for the real inner-product space $(V_{T}, B_{T})$ gives unique vectors $v_{s}^{(T)}$ with $e_{s}^{*} (y) = B (y, v_{s}^{(T)})$ ; symmetry gives $B (v_{s}^{(T)}, e_{t}) = δ_{s t}$ . For $y \in V_{T}$ , the difference $y - \sum_{s \in T} B (y, e_{s}) v_{s}^{(T)}$ lies in $V_{T}$ and pairs to zero with every spanning vector $e_{t}$ , so it is zero by positive definiteness. Also, for a subspace $W_{0}$ of a finite-dimensional inner-product space there is a unique orthogonal decomposition $v = P_{W_{0}} v + z$ with $z ⊥ W_{0}$ , and $P_{W_{0}} v$ is the orthogonal projection (Finite-dimensional Riesz representation: every functional is uniquely $v \mapsto ⟨ v, w ⟩$ , For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ , The orthogonal projection $P_{W} v$ is the $W$ -component in $V = W \oplus W^{⊥}$ , Real and complex inner-product spaces and their induced length).

[F5]

A linear isometry preserves the inner-product norm and hence the induced metric; translation leaves all pairwise distances unchanged, and a bijective isometry identifies the corresponding cell metrics (Linear isometries and isometric isomorphisms, Isometry, isometric embedding, and the subspace metric on a subset).

[F6]

Gluing data for an isometric polyhedral gluing consist of face isometries subject to the cocycle condition: the composites $C_{p} \to C_{q} \to C_{r}$ and $C_{p} \to C_{r}$ agree whenever $p \leq q \leq r$ (Abstract isometric polyhedral gluings and the chain metric).

Proof

technique · direct

1.1givenF1F2F4algebra

Fix a spherical $T$ . By [F2] the subsystem $(W_{T}, T)$ is finite with positive definite $B_{T}$ , and $ρ ∣_{W_{T}}$ is its canonical representation; the element $x_{T} = \sum_{s \in T} d_{s} v_{s}^{(T)}$ satisfies $B_{T} (x_{T}, e_{s}) = d_{s} > 0$ for every $s \in T$ by [F4], so $x_{T}$ lies in the open chamber of the subsystem. Applying [F1] to $(W_{T}, T)$ , $B_{T}$ and $x_{T}$ gives clause (1): $C_{T}$ is a compact convex polyhedral cell of dimension $∣ T ∣$ with $0$ in its interior, its nonempty faces are exactly the sets $conv (u W_{U} x_{T})$ for $u \in W_{T}$ , $U \subseteq T$ , each for exactly one coset $u W_{U}$ , and face inclusion agrees with coset inclusion (and the simultaneously reversed face and coset orders also agree). The supplier proves these nonempty faces are exposed, so its face description agrees with the nonempty faces in the polyhedral-cell convention of [F1]; that convention also includes $\emptyset$ , which is not any of the nonempty orbit hulls. For $T = \emptyset$ , one has $V_{T} = C_{T} = {0}$ , and the faces are $\emptyset$ and ${0}$ ; only the latter is indexed by the unique coset $W_{\emptyset} = {1}$ .

2.1step 1.1F4algebra

Let $U \subseteq T$ . For every $t \in U$ the dual-basis identity of [F4] gives $B (x_{T}, e_{t}) = d_{t} = B (x_{U}, e_{t})$ ; hence $B (x_{T} - x_{U}, e_{t}) = 0$ for all $t \in U$ , so $x_{T} - x_{U} \in V_{U}^{⊥} \cap V_{T}$ . Since $x_{U} \in V_{U}$ , this is the orthogonal decomposition of $x_{T}$ along $V_{U}$ , and uniqueness [F4] gives $P_{V_{U}} x_{T} = x_{U}$ . Conversely, any decomposition $x_{T} = x_{U} + z$ with $x_{U} \in V_{U}$ and $z \in V_{U}^{⊥} \cap V_{T}$ is that same unique orthogonal decomposition, so its $V_{U}$ -component is the projection. Put $z_{T, U} : = x_{T} - x_{U}$ .

3.1step 1.1step 2.1F3F4F5algebra

Let $U \subseteq T$ and $w \in W_{T}$ . The affine map $φ_{w}^{T, U} (v) = ρ (w) (v + z_{T, U})$ has linear part $ρ (w) ∣_{V_{U}}$ , which maps $V_{U}$ into $V_{T}$ by [F3] applied to $T$ , and preserves $B$ by [F3]; translation then shows it is an isometry onto $ρ (w) z_{T, U} + ρ (w) V_{U}$ by [F5]. To identify this image with the affine span of the face, first note that for every $t \in U$ , [step 1.1] and the reflection formula give $ρ (t) x_{T} - x_{T} = - 2 B (x_{T}, e_{t}) e_{t} = - 2 d_{t} e_{t} \in V_{U}$ . Induction on a word $u = v t$ in generators of $W_{U}$ gives $ρ (u) x_{T} - x_{T} = ρ (v) (ρ (t) x_{T} - x_{T}) + (ρ (v) x_{T} - x_{T}) \in V_{U}$ , because $ρ (v) V_{U} = V_{U}$ by [F3]. Thus $W_{U} x_{T} \subseteq x_{T} + V_{U}$ , while the differences $ρ (s) x_{T} - x_{T} = - 2 d_{s} e_{s}$ for $s \in U$ span $V_{U}$ since $d_{s} > 0$ and the $e_{s}$ are linearly independent; hence $aff (W_{U} x_{T}) = x_{T} + V_{U}$ . Applying $ρ (w)$ gives $aff (w W_{U} x_{T}) = ρ (w) x_{T} + ρ (w) V_{U}$ . Since $x_{T} = x_{U} + z_{T, U}$ by [step 2.1] and $x_{U} \in V_{U}$ , this affine span is $ρ (w) z_{T, U} + ρ (w) V_{U}$ , the image of $φ_{w}^{T, U}$ . Finally, for $v, v^{'} \in V_{U}$ , B-invariance gives $B_{T} (φ (v) - φ (v^{'}), φ (v) - φ (v^{'})) = B_{U} (v - v^{'}, v - v^{'})$ , so the affine isometry preserves the induced Euclidean distances.

3.2step 2.1F2F3algebra

The vector $z_{T, U}$ is fixed by $ρ (W_{U})$ : for $s \in U$ the reflection formula [F3] gives $ρ (s) x_{T} = x_{T} - 2 B (x_{T}, e_{s}) e_{s}$ and $ρ (s) x_{U} = x_{U} - 2 B (x_{U}, e_{s}) e_{s}$ , and the two pairings are equal to $d_{s}$ by [step 2.1], so subtracting yields $ρ (s) z_{T, U} = z_{T, U}$ ; since $U$ generates $W_{U}$ , this gives $ρ (u) z_{T, U} = z_{T, U}$ for every $u \in W_{U}$ . Moreover $x_{U} = \sum_{s \in U} d_{s} v_{s}^{(U)}$ is built from $U$ and the numbers $d_{s}$ with $s \in U$ only, so the same holds for the projected point of (2).

4.1step 1.1step 3.2step 3.1F5

The map $φ_{w}^{T, U}$ carries $C_{U}$ onto the face $conv (w W_{U} x_{T})$ : for $u \in W_{U}$ one has $φ_{w}^{T, U} (ρ (u) x_{U}) = ρ (w) ρ (u) (x_{U} + z_{T, U}) = ρ (w u) (x_{U} + z_{T, U}) = ρ (w u) x_{T}$ , because $ρ (u) z_{T, U} = z_{T, U}$ by [step 3.2]; as $u$ runs over $W_{U}$ , $w u$ runs over the coset $w W_{U}$ , and $φ$ is affine, so it maps the convex hull $C_{U}$ onto the convex hull of those points. Since $φ_{w}^{T, U}$ is an isometry [step 3.1], the intrinsic metric of the face equals that of $C_{U}$ by [F5]; and $C_{U}$ is built from $U$ and the numbers $d_{s}$ with $s \in U$ only, by [step 3.2].

4.2step 2.1step 3.2F4algebra

Let $U \subseteq T \subseteq T^{'}$ be spherical. Then $z_{T, U} + z_{T^{'}, T} = z_{T^{'}, U}$ : both sides belong to $V_{U}^{⊥} \cap V_{T^{'}}$ , and $x_{T^{'}} = x_{T} + z_{T^{'}, T} = x_{U} + z_{T, U} + z_{T^{'}, T}$ while also $x_{T^{'}} = x_{U} + z_{T^{'}, U}$ ; the orthogonal decomposition of $x_{T^{'}}$ along $V_{U}$ in $(V_{T^{'}}, B_{T^{'}})$ is unique by [F4], so the two complements agree.

5.1step 3.2step 4.2F6algebra

Cocycle. Let $U \subseteq T \subseteq T^{'}$ be spherical, $g_{1} \in W_{T}$ and $g_{2} \in W_{T^{'}}$ . By [step 3.2] applied to the pair $T \subseteq T^{'}$ , the vector $z_{T^{'}, T}$ is fixed by $ρ (W_{T})$ , in particular by $ρ (g_{1})$ . Hence, using [step 4.2], $φ_{g_{2}}^{T^{'}, T} (φ_{g_{1}}^{T, U} (v)) = ρ (g_{2}) (ρ (g_{1}) (v + z_{T, U}) + z_{T^{'}, T}) = ρ (g_{2} g_{1}) (v + z_{T, U} + ρ (g_{1})^{- 1} z_{T^{'}, T}) = ρ (g_{2} g_{1}) (v + z_{T^{'}, U}) = φ_{g_{2} g_{1}}^{T^{'}, U} (v) .$ Thus the face isometries of the cells $C_{T}$ satisfy the cocycle condition of gluing data [F6] and are compatible on common faces: a coset $w^{'} W_{U} \subseteq w W_{T}$ carries both the identification of the face of $C_{w W_{T}}$ with $C_{w^{'} W_{U}}$ and its identification through any intermediate cell, and the two composites agree by the displayed identity.

6.1step 1.1step 2.1step 3.1step 4.1step 5.1given∎

The four clauses are proved: (1) is [step 1.1], (2) is [step 2.1] with [step 3.2], (3) is [step 3.1] with [step 4.1], and (4) is [step 5.1]. No Choice is used: all hulls are finite, the subsystems $W_{T}$ are finite, and the only identifications are explicit isometries.

Depends on

Used by

Dependency tree · two levels

148 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. W. Davis, The Geometry and Topology of Coxeter Groups, author manuscript of the first edition (Princeton Univ. Press, 2008) (standard reference, not scraped)
M. W. Davis, The Geometry and Topology of Coxeter Groups (MSC lecture slides, Tsinghua, 2013) (standard reference, not scraped)