Alphabeta Math
Pipeline-generated
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.

✓ 6 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Spherical Parabolic Cosets and the Davis Complex

1 · Prerequisites

2 · Summary

For a Coxeter system with finitely many generators, the spherical parabolic cosets form the Davis complex. This page constructs its finite-type cells, compatible face metrics, topology and group action, then proves its CW structure and simple connectivity.

The seven items proceed from the spherical-subset and coset definitions through finite orbit geometry to the complete cellulation. The claims apply to finite-rank Coxeter systems, including those whose ambient group is infinite.

Cells, action and simple connectivity

Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization defines the spherical subsets, nerve, inclusion poset of cosets and chamber. Equality, inclusion and intersection of spherical cosets, and the quotient poset proves the equality, containment and intersection criteria needed to index cells unambiguously. The finite-type Coxeter cell: exposed faces and normal cones identifies every face of a finite Coxeter orbit polytope, and Finite Coxeter orbit polytopes, face isometries and their cocycle supplies compatible affine face isometries for fixed positive mirror distances.

The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) constructs the isometric polyhedral gluing, identifies its barycentric subdivision with the Davis realization and proves completeness, properness, the cell and point stabilizer formulas, the proper group action and the compact chamber quotient. The Davis complex as a CW complex: disk cells and the Cayley skeleta gives disk characteristic maps and the CW topology; its one-skeleton is the Cayley graph and its two-cells are the finite rank-two polygons, with involution relations represented by backtracks.

The Davis complex is simply connected reduces loops to finite edge walks, fills the Coxeter relator polygons and uses relative cellular approximation to control the two-skeleton. The resulting Davis complex is simply connected. The companion examples make the cell geometry and the finite Coxeter sphere versus Davis cell distinction explicit.

Prerequisites and reading

Required earlier pages: parabolic-subgroups-and-double-coset-geometry, finite-reflection-arrangements-and-spherical-coxeter-complexes, coxeter-polyhedral-gluings-and-intrinsic-metrics, cw-complexes-and-cellular-homology, simplicial-subdivision-and-simplicial-approximation, simplicial-complexes-and-simplicial-homology, hurewicz-whitehead-freudenthal-and-cw-approximation. The companion spherical-parabolic-cosets-and-the-davis-complex-examples tests these constructions and conventions. Exact item dependencies and source reading limits are recorded in research/coxeter-scaffold/inventory.json and research/plan-coxeter-groups-track.md.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization

Definition

Let (S,m) be a Coxeter matrix with S finite, let W be the presented group with length function ℓ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), and for T⊆S let WT=⟨s:s∈T⟩≤W (Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (1), The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups); recall WT={w∈W:S(w)⊆T} for the support S(w) of a reduced expression (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1)).

(1) Spherical subsets and the nerve. A subset T⊆S is spherical when WT is finite. Let S denote the set of spherical subsets, partially ordered by inclusion; it has least element ∅ because W∅={1}. If T∈S and T′⊆T, then WT′≤WT (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups), so T′ is spherical by In a finite group, the subgroup, every coset and the set of cosets are finite: S is downward closed. For each s∈S, the relation s2=1 makes W{s} finite, so every singleton is spherical (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups). The nerve L is the abstract simplicial complex (An abstract simplicial complex) on vertex set S whose nonempty simplices are the nonempty spherical subsets; it also contains the empty simplex by the library's complex convention. Since S is finite, L is finite.

(2) The poset of spherical cosets. For T∈S and w∈W let wWT be the left coset (Left and right cosets gH and Hg of a subgroup), and put WS:={wWT:w∈W, T∈S}, partially ordered by inclusion of subsets of W. For T=∅ this gives wW∅={w}, so W sits inside WS as the set of minimal elements. A member of WS is the resulting subset of W, not a choice of representative pair (w,T); the equality, inclusion, and intersection criteria for these cosets are proved in Equality, inclusion and intersection of spherical cosets, and the quotient poset ↗.

(3) The Davis realization. Σ:=∣WS∣ is the geometric realization of the order complex of the poset WS (Face poset and order complex, The geometric realization of an abstract simplicial complex): its vertices are the cosets wWT, and its simplices are the finite chains in WS. The chamber is K:=∣S∣, the order complex of the poset of spherical subsets, and j ⁣:K→Σ is the simplicial map induced by T↦WT; this is simplicial because T⊆T′ implies WT⊆WT′. As an abstract complex, K is the cone with apex ∅ over the barycentric subdivision of L, and it is finite, hence compact and Hausdorff (A finite simplicial complex has a compact Hausdorff realization).

(4) The W-action. Left multiplication (v,wWT)↦(vw)WT is a well-defined left action of W on the set WS by order-preserving bijections (Group and abelian group, Left and right cosets gH and Hg of a subgroup); it induces a simplicial action of W on Σ. The chambers of Σ are the images wj(K)=wK, w∈W, and the map w↦wK is injective: the vertex W∅={1} of K is carried to wW∅={w}, and {v}={w}W∅ forces v=w (Left and right cosets gH and Hg of a subgroup).

Remarks

  • (5) Abstentions. Nothing beyond these constructions is asserted here: not that the chambers meet one another in faces, not that the spherical cosets wWT carry the structure of the Coxeter cells CT, not that the action on Σ is proper with compact quotient, and not that Σ is simply connected. Those assertions are the content of The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) ↗, a recorded justifier of this definition; simple connectivity is proved later on this page.
  • Choice. No Choice is used in (1)-(4): all constructions are set-theoretic over the finite set S and the fixed group W.
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Equality, inclusion and intersection of spherical cosets, and the quotient poset

Statement

Let (S,m), W, ℓ, S, the parabolics WT and the poset WS be as in Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization; keep the convention that S(w) is the set of letters of any reduced expression of w (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1)). Let T,T′∈S and w,w′∈W.

(1) Equality. wWT=w′WT′ if and only if T=T′ and w−1w′∈WT. Hence the projection π ⁣:WS→S, wWT↦T, is well-defined, the members of WS are exactly the left cosets of the subgroups WT (T∈S), and the left cosets of any one WT are pairwise disjoint while cosets of distinct parabolics are distinct.

(2) Inclusion. wWT⊆w′WT′ if and only if T⊆T′ and w−1w′∈WT′ (equivalently w∈w′WT′, equivalently wWT′=w′WT′). In particular WT⊆WT′ if and only if T⊆T′.

(3) Intersections are parabolic cosets. If wWT∩w′WT′≠∅, then wWT∩w′WT′=uWT∩T′for every u∈wWT∩w′WT′; moreover wWT∩w′WT′≠∅ if and only if w−1w′∈WTWT′, where WTWT′={ab:a∈WT, b∈WT′}. Thus the meet of two spherical cosets in the inclusion order, when their intersection is nonempty, is that intersection coset, of type T∩T′; disjoint spherical cosets have no common lower bound in WS.

(4) The quotient poset. The left action of (4) of Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization is order-preserving and π-invariant, and it is transitive on the cosets of each fixed parabolic; the induced map of posets W\WS→S is an isomorphism. Consequently the action on WS is free on the minimal elements wW∅.

Facts & Assumptions

Given: A finite Coxeter matrix (S,m) with presented group W and length ℓ; spherical subsets T,T′∈S; elements w,w′∈W.

[F1]

The support criterion is WT={x∈W:S(x)⊆T} (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1)).

[F2]

For each T⊆S, WT∩S=T (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2)).

[F3]

Intersections of standard parabolic subgroups: WI∩WJ=WI∩J for all I,J⊆S (Intersections of standard parabolics, the parabolic root subsystem, and global minimality of coset representatives (1)).

[F4]

Multiplication in W is associative, has identity 1, and every element has a two-sided inverse (Group and abelian group).

[F5]

The spherical subsets are downward closed and W∅={1} (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)).

[L1]

Coset membership and equality: for a subgroup H≤G and a,b∈G, one has b∈aH if and only if a−1b∈H, and aH=bH if and only if a−1b∈H (x∈aH iff a−1x∈H, and aH=bH iff a−1b∈H).

[L2]

A left coset of H≤G is the set gH={gh:h∈H} (Left and right cosets gH and Hg of a subgroup).

[L3]

Every subgroup contains the identity and is closed under products and inverses (Subgroup).

Proof

technique · direct
1.1givenF2L1L2L3algebra

Suppose wWT=w′WT′. Since 1∈WT and 1∈WT′ by [L3], the element w lies in wWT=w′WT′ and w′ lies in w′WT′=wWT; by [L1] this gives w−1w′∈WT′ and w′−1w∈WT. Left-multiplying the coset equality by w−1 and using (w−1w)WT=WT and (w−1w′)WT′=uWT′ with u:=w−1w′ gives WT=uWT′; since u−1=w′−1w∈WT by [L3], also WT′=u−1WT=WT. Intersecting with S and applying [F2] yields T=T′, and w−1w′=u∈WT′=WT.

1.2givenL1algebra

Conversely, if T=T′ and w−1w′∈WT, then w′∈wWT by [L1], so w′WT=wWT by [L1]; together with T=T′ this is wWT=w′WT′.

1.3givenF2L1L2L3algebra

Suppose wWT⊆w′WT′. Then w∈w′WT′, so w−1w′∈WT′ by [L1]; left-multiplying the inclusion by w−1 gives WT=w−1(wWT)⊆w−1(w′WT′)=(w−1w′)WT′=WT′ by [L3]. Hence T=WT∩S⊆WT′∩S=T′ by [F2].

1.4givenF1F2L1L2algebra

Conversely, if T⊆T′ and w−1w′∈WT′, then WT≤WT′ by [F1], so wWT⊆wWT′=w′WT′ by [L2]. This also covers the two reformulations: w∈w′WT′ is equivalent to w−1w′∈WT′ by [L1], and wWT′=w′WT′ is equivalent to w−1w′∈WT′ by [L1] applied with T=T′. Taking w=w′=1 gives WT⊆WT′ if and only if T⊆T′.

1.5givenF3F4L1L2algebra

Assume u∈wWT∩w′WT′. Then uWT=wWT and uWT′=w′WT′ by [L1]. Left multiplication by u is a bijection with inverse left multiplication by u−1, by [F4], so it takes intersections to intersections; hence wWT∩w′WT′=uWT∩uWT′=u(WT∩WT′)=uWT∩T′, the last equality by [F3].

1.6givenF4L2L3algebra

The intersection is nonempty if and only if w−1w′∈WTWT′: indeed wWT∩w′WT′≠∅ means that wa=w′b for some a∈WT, b∈WT′, which is equivalent by the group laws [F4] to w−1w′=ab−1∈WTWT′ because WT′ is closed under inverses by [L3].

2.1step 1.1step 1.2L1

The projection π is well-defined by [step 1.1]; for fixed T the criterion wWT=w′WT  ⟺  w−1w′∈WT is [step 1.1] and [step 1.2] together; and two cosets of WT are disjoint when they are unequal, since if u lies in both then wWT=uWT=w′WT by [L1]. Thus the members of WS are exactly the left cosets of the subgroups WT (T∈S).

2.2step 1.5F5givenalgebra

The meet statement of (3): by [step 1.5] the intersection p=wWT∩w′WT′ of two cosets is a member of WS when nonempty, with π(p)=T∩T′ (spherical, since T∩T′⊆T∈S and S is downward closed by [F5]); it is contained in both cosets, so it is a lower bound. If r=vWV∈WS satisfies r⊆wWT and r⊆w′WT′, then r⊆p by definition of intersection. Hence p is the greatest lower bound, and no member of WS is contained in two disjoint cosets because members of WS are nonempty.

2.3step 1.1step 1.3step 1.4F4algebra

The quotient poset of (4): left multiplication is order-preserving and π-invariant because (v⋅wWT)=(vw)WT has type T ([step 1.1]); it is transitive on the cosets of a fixed parabolic, as v:=w′w−1 sends wWT to w′WT by [F4]. The induced map πˉ ⁣:W\WS→S is well-defined by π-invariance, surjective because the orbit of WT has type T, and injective because two cosets of type T are wWT and w′WT, and v:=w′w−1 carries the first to the second. It preserves order: if orbits satisfy [q]≤[q′] with representatives vq⊆v′q′, then [step 1.3] gives π(vq)⊆π(v′q′) in S; it reflects order: if T⊆T′, then WT⊆WT′ by [step 1.4], so the corresponding orbits are comparable. Hence πˉ is an isomorphism of posets.

3.1F2F4F5L2L3step 1.1step 1.3step 2.3given∎

The minimal elements of WS are exactly the singletons wW∅={w}. If T≠∅, choose s∈T. By [F2], s∈WT and W∅∩S=∅; with [F5] and 1∈WT by [L3], this gives s∉W∅ and W∅={1}⊊WT, hence wW∅⊊wWT. Conversely, if vWV⊆wW∅, then [step 1.3] gives V⊆∅, so V=∅; the inclusion of singletons is equality, and [step 1.1] gives v=w. The action is free on them because v⋅wW∅=wW∅ forces vw=w and hence v=1 by [F4]. This completes (1)-(4). No Choice is used: every argument is set algebra in the fixed group W and the finite set S.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The finite-type Coxeter cell: exposed faces and normal cones

Statement

Let (W,S) be a Coxeter system of finite type with S finite, canonical reflection representation ρ on V=RS (The canonical reflection homomorphism, roots, reflections, and the positive cone), Coxeter form B (The real Coxeter form, its radical, reflections, and form-preserving maps), root system Φ=Φ+⊔Φ−, and let V≅V∗ be the identification b(v)=B(v,⋅) made in The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset; let C, C∘ and the faces CI‾ be the chamber, its interior and its faces of the dual action (The dual action, chambers, faces, and root hyperplanes), and let (vs)s∈S be the B-dual basis (The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (2)). Fix x∈C∘, put ds:=B(x,es)>0, S(y):={s∈S:B(y,es)=0} for y∈V, and P:=conv⁡(Wx).

(1) Inversion expansion. For every v∈W with reduced expression v=s1⋯sk, x−ρ(v)x=∑i=1k2 dsi ρ(s1⋯si−1)esi, a sum of nonnegative multiples of the positive roots ρ(s1⋯si−1)esi, which are the elements of N(v−1) (The geometric inversion set N(w) of an element of a Coxeter group (3), The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (2)). Consequently x−ρ(v)x∈V+∖{0} for v≠1, and B(y,x−ρ(v)x)≥0 for every y∈C.

(2) The normal cone at x. For y∈C one has max⁡v∈WB(y,ρ(v)x)=B(y,x), and the maximizer set {v∈W:B(y,ρ(v)x)=B(y,x)} equals WS(y).

(3) Maximizer faces. For arbitrary y∈V, write y=ρ(w)y0 with w∈W and y0∈C. The point y0 is unique, while w is determined exactly up to right multiplication by WS(y0), by the strict fundamental domain and chamber-face stabilizer in The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1),(3). Then the maximizer set of the linear functional B(y,⋅) on P is conv⁡(wWS(y0)x)=wconv⁡(WS(y0)x).

(4) The face poset. Every point of Wx is a vertex of P; the faces of P (Extreme point and face) are exactly the sets conv⁡(wWUx) for w∈W and U⊆S, each occurring for exactly one coset wWU; and conv⁡(wWUx)⊆conv⁡(w′WU′x)  ⟺  wWU⊆w′WU′. Hence wWU↦conv⁡(wWUx) is an isomorphism from the poset {wWU:w∈W, U⊆S} ordered by reverse inclusion onto the nonempty face poset of P ordered by reverse inclusion (restricting to U⊊S gives the proper-coset poset of The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset (3) and the proper nonempty faces), dim⁡conv⁡(wWUx)=∣U∣, and the setwise stabilizer of conv⁡(wWUx) in W is wWUw−1.

(5) Polyhedral cell description. Put cs:=B(vs,x) for s∈S; then cs>0, 0 lies in the interior of P, and P={v∈V:B(wvs,v)≤cs for all w∈W, s∈S}, a compact convex polyhedral cell in the sense of Finite convex cell complex and linear subdivision with 0 in its interior.

Facts & Assumptions

Given: A finite-type Coxeter system (W,S) with canonical representation ρ on (V,B), the chamber C, its interior C∘, the B-dual basis (vs), and x∈C∘ with ds=B(x,es)>0; P=conv⁡(Wx).

[F1]

For a∈V with B(a,a)≠0 the reflection ra(v)=v−2B(v,a)B(a,a)a is linear and involutive, preserves B, fixes {v:B(v,a)=0} pointwise, and rav=v holds if and only if B(v,a)=0; moreover ρ(s)=res and B(es,es)=1 (The real Coxeter form, its radical, reflections, and form-preserving maps (3), Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2), The canonical reflection homomorphism, roots, reflections, and the positive cone (1)).

[F2]

Φ=Φ+⊔Φ−, Φ−=−Φ+, es∈Φ+, and every positive root lies in V+∖{0}, where V+={∑s∈Sλses:λs≥0} (Root sign coherence and the action of simple reflections on positive roots (2)).

[F3]

For a reduced expression w=s1⋯sn the prefix roots ρ(s1⋯si−1)esi are positive, pairwise distinct, and form exactly N(w−1), and ℓ(ws)>ℓ(w) if and only if ρ(w)es∈Φ+ (The geometric inversion set N(w) of an element of a Coxeter group (3), The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (2), The root-length criterion and faithfulness of the canonical reflection representation (1)).

[F4]

In finite type W is finite and B is positive definite, so (V,B) is a Euclidean space and b(v)=B(v,⋅) identifies V with V∗, transferring C, C∘ and the faces; (vs) is the B-dual basis of (es), so B(vs,et)=δst and y=∑sB(y,es)vs for every y∈V; every W-orbit in V meets C in exactly one point; for x′∈wCI the stabilizer is Stab⁡W(x′)=wWIw−1 (The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset, The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1)-(3), Finiteness criterion: W is finite exactly when the Coxeter form is positive definite (1)).

[F5]

Coset inclusion criterion: wWU⊆w′WU′ if and only if U⊆U′ and w−1w′∈WU′ (Equality, inclusion and intersection of spherical cosets, and the quotient poset (2)).

[F6]

A point x of a convex set K is extreme exactly when the singleton {x} is a face of K, and a face is a nonempty convex subset F⊆K such that (1−t)y+tz∈F with y,z∈K, 0<t<1 forces y,z∈F; for a singleton set the only face is the set itself (Extreme point and face).

[F7]

For a nonempty compact convex set K and a continuous affine functional a, the level set {p∈K:a(p)=min⁡Ka} is a nonempty compact face of K (Minimizer face of a continuous affine functional).

[F8]

A point outside a nonempty closed convex set in a finite-dimensional Euclidean space is strictly separated from it by a nonzero linear functional (A point outside a nonempty closed convex set is strictly separated from it).

[F9]

Convex hulls of finitely many points are compact and closed in a Hausdorff TVS; convexity uses the usual finite convex combinations (Convex closures and hulls of finitely many compact convex sets, A convex subset of Rm contains every line segment between two of its points, Local convexity, convex and balanced sets, and the continuous dual).

[F10]

A compact convex polyhedral cell is a nonempty bounded subset of a finite-dimensional Euclidean affine space given by finitely many affine inequalities ≥0; it is closed and compact (Finite convex cell complex and linear subdivision).

[F11]

A linear subspace is closed under vector operations, its span is the smallest linear subspace containing the given vectors, a basis is a linearly independent spanning set, and dimension is the cardinality of a basis (Linear subspace of a vector space, Linear combination of a finite list, and the span span⁡(S) as the smallest linear subspace containing S, Linear independence: a finite list v:n→V is independent when ∑i<nλivi=0V forces every λi=0F, and a subset S⊆V is independent when every injective finite list into S is independent, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Finite-dimensional vector space, and its dimension dim⁡FV; infinite-dimensional means having no finite basis). For a finite set of vectors, a maximal linearly independent subset exists by choosing one of largest cardinality among its finitely many subsets; it spans the same subspace as the finite set.

[F12]

In a finite-dimensional inner-product space every linear subspace L has the orthogonal decomposition V=L⊕L⊥ (The orthogonal complement W⊥={v:⟨v,w⟩=0 for all w∈W}, For a subspace W of a finite-dimensional inner product space, V=W⊕W⊥). The map sending v=l+z in this unique decomposition to its L⊥ component z is linear and has kernel L, by uniqueness of the decomposition. A subspace of a finite-dimensional vector space is finite-dimensional (If dim⁡FV=n and U is a linear subspace of V, then U is finite-dimensional, dim⁡FU≤n, and dim⁡FU=n if and only if U=V), and a finite-dimensional inner-product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis); hence the strict-separation theorem [F8] applies in L⊥ with its inherited inner product.

[F13]

For every U⊆S, WU is the subgroup generated by U and a subgroup is closed under inverses; group multiplication has inverses and is associative (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups, Subgroup, Group and abelian group).

[F14]

The interior of a convex set is convex, and a finite convex combination of interior points of a convex set remains in the interior (Convex closures and hulls of finitely many compact convex sets).

Proof

technique · direct
1.1givenF4algebra

Since C={y:B(y,es)≥0 for all s} and x∈C∘, each ds=B(x,es) is positive; and by [F4] every y∈V satisfies y=∑s∈SB(y,es)vs, so for y∈C all coefficients B(y,es) are ≥0. Hence for y∈C and any z=∑sz(s)es∈V+ with z(s)≥0, linearity gives B(y,z)=∑sB(y,es)z(s)≥0.

1.2givenF1F3algebra

We prove (1) by induction on k=ℓ(v). For k=0 both sides vanish. For k≥1 write v=v′sk with v′=s1⋯sk−1 reduced. Then x−ρ(v)x=(x−ρ(v′)x)+ρ(v′)(x−ρ(sk)x), the reflection formula [F1] gives x−ρ(sk)x=2B(x,esk)esk=2dskesk, and substituting the induction hypothesis for v′ and applying ρ(v′) produces the displayed sum. Each ρ(s1⋯si−1)esi lies in Φ+ by the root-length criterion, since ℓ(s1⋯si−1si)=i>ℓ(s1⋯si−1), and these are precisely the elements of N(v−1) by [F3].

1.3givenF9algebra

We record the convex-combination principle: if ℓ is linear and S0⊆Wx is the set on which ℓ attains its maximum over Wx, then the maximizer set of ℓ on P=conv⁡(Wx) is conv⁡(S0). Indeed every p∈P is a convex combination p=∑iλiρ(vi)x with ∑iλi=1, λi≥0; then ℓ(p)=∑iλiℓ(ρ(vi)x)≤max⁡Wxℓ, and equality holds exactly when every ρ(vi)x with λi>0 lies in S0; the set of such combinations is conv⁡(S0), which is nonempty.

2.1step 1.1step 1.2F2algebra

If v≠1 then k≥1, so the expansion of [step 1.2] is a sum with all coefficients 2dsi positive of positive roots, which lie in V+∖{0} by [F2]; hence x−ρ(v)x∈V+∖{0}. For y∈C this gives B(y,x−ρ(v)x)≥0 by [step 1.1], that is B(y,ρ(v)x)≤B(y,x): the maximum in (2) equals B(y,x).

2.2step 1.1step 1.2F1algebra

Equality case of (2). Let y∈C and suppose B(y,ρ(v)x)=B(y,x), i.e. B(y,x−ρ(v)x)=0. By [step 1.2] write x−ρ(v)x=∑i=1k2dsiβi with βi∈Φ+⊆V+; by [step 1.1] every B(y,βi)≥0, so 0=∑i2dsiB(y,βi) with positive coefficients forces B(y,βi)=0 for all i. We prove v∈WS(y) by induction on k: for k=0 this is trivial; for k≥1, i=1 gives B(y,es1)=0, so s1∈S(y) and ρ(s1)y=y by [F1]. With v′=s2⋯sk one has ρ(v)x=ρ(s1)ρ(v′)x, hence B(y,ρ(v′)x)=B(ρ(s1)−1y,ρ(v′)x)=B(y,ρ(v)x)=B(y,x), and ℓ(v′)=k−1, so the induction hypothesis gives v′∈WS(y); with s1∈WS(y) this gives v∈WS(y). Conversely if v∈WS(y) then every generator s∈S(y) fixes y by [F1], so ρ(v)y=y and B(y,ρ(v)x)=B(ρ(v)−1y,x)=B(y,x). Hence the maximizer set in (2) is exactly WS(y).

3.1step 2.1step 1.3step 2.2F4algebra

For arbitrary y=ρ(w)y0 with y0∈C [F4], the chamber representative y0 is unique. If also y=ρ(w′)y0, then w−1w′∈Stab⁡W(y0)=WS(y0) by [F4], and conversely every such w′ gives the same y; thus the coset wWS(y0) is independent of the representative. For any v∈W, put u:=w−1v, so that v=wu; then B(y,ρ(v)x)=B(ρ(w)y0,ρ(w)ρ(u)x)=B(y0,ρ(u)x)≤B(y0,x)=B(y,ρ(w)x) by [step 2.1], with equality if and only if u∈WS(y0) by [step 2.2], i.e. v∈wWS(y0). So the orbit points maximizing B(y,⋅) on Wx are exactly ρ(w)WS(y0)x, and by the principle of [step 1.3] the maximizer set on P is conv⁡(ρ(w)WS(y0)x)=ρ(w)conv⁡(WS(y0)x), since ρ(w) is linear.

4.1step 3.1F4F6F7algebra

Every point of Wx is an extreme point of P. Indeed put y0:=∑s∈Svs, an element of C∘ because B(y0,es)=1>0 for every s by [F4]; thus S(y0)=∅ and WS(y0)={1}. For w∈W apply [step 3.1] to y:=ρ(w)y0: the maximizer set of the functional B(y,⋅) on P is conv⁡(ρ(w)W∅x)={ρ(w)x}, a singleton, so the minimizer set of the continuous affine functional −B(y,⋅) is that same singleton. By [F7] applied to −B(y,⋅) this singleton is a face of the compact convex set P, and by [F6] a point whose singleton is a face is an extreme point of P. Hence ρ(w)x is extreme in P.

4.2step 1.3step 3.1F4F8F9F11F12algebra

Every face of P is of the form conv⁡(wWUx). Let F be a face and A:=(Wx)∩F. Since F is nonempty, choose p0∈F and express it as a convex combination of orbit points; induction on the number of positive coefficients and the face condition show that every orbit point with positive coefficient lies in F, so A≠∅. Applying the same argument to each p∈F gives F=conv⁡(A). If A=Wx then F=P=conv⁡(Wx)=conv⁡(WSx), the case w=1, U=S. Otherwise put Aout:=(Wx)∖A, which is nonempty, and choose a0∈A. The finite set D0:={a−a0:a∈A} spans the direction space L:=span⁡{q−q′:q,q′∈F} because F=conv⁡(A). By [F11], choose a maximal linearly independent subset d1,…,dk of D0; it spans L, and for each i write di=ai−a0 with ai∈A. Put p:=(a0+a1+⋯+ak)/(k+1)∈F. We claim P∩(p+L)⊆F. For q∈P∩(p+L) write q−p=∑i=1ktidi. If k=0, then q=p∈F. If k>0, choose ε>0 small enough that all coefficients in r:=p−ε(q−p)=(1k+1+ε∑iti)a0+∑i=1k(1k+1−εti)ai are positive; these coefficients sum to 1, so r∈F. The identity p=ε1+εq+11+εr and the face condition imply q∈F, proving the claim. Now set D:=conv⁡(Aout), a nonempty compact convex set by [F9]. Let π:V→L⊥ send a vector to its L⊥ component in [F12]; it is linear and ker⁡π=L. If π(p)∈π(D), there is q∈D with q−p∈L, so q∈P∩(p+L)⊆F; writing q as a convex combination of points of Aout and using the face condition would put a positive-support orbit point in Aout∩F, a contradiction. Thus π(p)∉π(D). Linearity gives π(D)=conv⁡(π(Aout)), so [F9] makes π(D) nonempty, compact, and closed; it is convex as well. Since the point is outside this nonempty set, L⊥ is nonzero, and [F12] supplies orthonormal coordinates in which to apply [F8] in L⊥; pulling the Euclidean normal back to L⊥ gives u∈L⊥, u≠0, and b∈R such that B(u,π(q))≤b<B(u,π(p)) for every q∈D. As u⊥L, the functional B(u,⋅) is constant on p+L, so its value on every point of A⊆F⊆p+L equals B(u,p), while every point of Aout has strictly smaller value. Therefore its maximizers on Wx are exactly A, and [step 1.3] shows its maximizer face on P is conv⁡(A)=F. Write u=ρ(w)y0 with y0∈C by [F4] and apply [step 3.1]; then F=conv⁡(wWS(y0)x), with U:=S(y0).

5.1step 3.1step 4.1F4F6F7algebra

Fix U⊆S and w∈W and put y0:=∑s∉Uvs, an element of C because B(y0,es)=1 for s∉U and B(y0,es)=0 for s∈U by [F4], so that S(y0)=U. By [step 3.1] applied to y=ρ(w)y0, the set conv⁡(wWUx) is the maximizer set of B(y,⋅) on P, hence a face of P: it is the minimizer set of the continuous affine functional −B(y,⋅), so [F7] applied to the compact convex P gives the face and singles it out. Its extreme points are exactly wWUx. Each such orbit point is extreme in P by [step 4.1], and remains extreme in the contained convex subset conv⁡(wWUx). Conversely, if z is extreme in this finite hull, express z as a convex combination of its finite generating set; if a positive-weight term differs from z, grouping that term against the remaining terms gives a strict convex decomposition of z into two distinct points of the hull, contradicting extremality. Thus z is one of the generators. Finally the map v↦ρ(v)x is injective on W: if ρ(v)x=ρ(v′)x, then ρ(v−1v′)x=x, so v−1v′ lies in Stab⁡W(x)=WS(x)=W∅={1} by [F4], whence v=v′.

6.1step 5.1step 4.1step 4.2algebra

The assignment is injective on cosets: if conv⁡(wWUx)=conv⁡(w′WU′x), then by [step 5.1] the vertex sets coincide, wWUx=w′WU′x, and injectivity of v↦ρ(v)x from [step 5.1] gives wWU=w′WU′ as subsets of W. The inclusion equivalence of (4) now follows: if wWU⊆w′WU′ then conv⁡(wWUx)⊆conv⁡(w′WU′x); conversely, if the hulls are nested, each generator in the smaller vertex set wWUx is extreme in P by [step 4.1] and therefore remains extreme in the larger convex hull, so [step 5.1] puts it in the larger vertex set w′WU′x. Thus wWU⊆w′WU′. Combining with [step 5.1] and [step 4.2], the map wWU↦conv⁡(wWUx) is a bijection from the coset poset onto the set of faces carrying containment on cosets to containment of faces, hence an isomorphism from the poset ordered by reverse inclusion onto the face poset ordered by reverse inclusion.

6.2step 5.1F1F4F5F11F13algebra

Dimension and stabilizer. Put VU:=span⁡{es:s∈U}. For each t∈U and s∈U, the reflection formula gives ρ(t)es=es−2B(es,et)et∈VU, so ρ(t) preserves VU and hence so does every ρ(u) with u∈WU. Also ρ(t)x−x=−2dtet∈VU; induction on a word in the generators of WU then gives ρ(u)x−x∈VU for every u∈WU. Thus wWUx⊆ρ(w)x+ρ(w)VU and its affine dimension is at most ∣U∣. For the reverse inequality, its affine span contains ρ(w)x and all ρ(w)ρ(s)x=ρ(ws)x for s∈U, whose differences ρ(w)(ρ(s)x−x)=−2dsρ(w)es are linearly independent because ds>0, the es are a basis subset and ρ(w) is invertible. Hence dim⁡conv⁡(wWUx)=∣U∣. For the setwise stabilizer, g⋅conv⁡(wWUx)=conv⁡(wWUx) if and only if gwWUx=wWUx by the vertex-set description [step 5.1], if and only if gwWU=wWU by injectivity in [step 5.1]. By the coset inclusion criterion [F5], equality implies w−1g−1w∈WU; since WU is a subgroup and closed under inverses [F13], this is equivalent to w−1gw∈WU, and the reverse implication gives the same coset equality. Thus the stabilizer is wWUw−1.

7.1step 2.1step 6.2F1F4F8F9F10F14algebra

Polyhedral description and the origin. First, P⊆Q:={v:B(wvs,v)≤cs for all w∈W, s∈S}: if p=∑iλiρ(vi)x∈P, then for all w,s, linearity and B-invariance give B(wvs,p)=∑iλiB(vs,ρ(w−1vi)x)≤∑iλiB(vs,x)=cs by [step 2.1] applied to vs∈C and the orbit point ρ(w−1vi)x. Second, Q⊆P: suppose z∈Q∖P; since P is compact (a finite point hull, [F9]) and convex, [F8] gives u with B(u,z)>max⁡PB(u,⋅). The set Q is invariant under ρ(W) because B(ρ(w)vs,ρ(g)z)=B(ρ(g)−1ρ(w)vs,z) and the W-orbit of each vs is permuted. Choose g∈W with ρ(g)u∈C by [F4], and replace both z and u by ρ(g)z and ρ(g)u: the new point stays in Q∖P, and the strict inequality persists because P is ρ(W)-invariant and B is ρ(W)-invariant. Thus we may assume u∈C. Then u=∑sasvs with as=B(u,es)≥0 and B(u,z)=∑sasB(vs,z)≤∑sascs, while max⁡PB(u,⋅)=B(u,x)=∑sasB(vs,x)=∑sascs by [step 2.1] and the dual-basis expansion; this contradicts the strict separation. Hence P=Q. Third, 0∈int⁡P: the points x and ρ(s)x for s∈S have differences −2dses, so if ∣S∣>0 their convex hull is a full-dimensional simplex contained in P; if S=∅, then V=P={0} and its interior in V is itself. Thus P has nonempty interior. For any p∈int⁡P, each ρ(w)p is also in int⁡P since ρ(w) is an invertible linear map with ρ(w)P=P; convexity of the interior [F9] then puts the average pˉ:=1∣W∣∑w∈Wρ(w)p in int⁡P. It is W-fixed, and the only W-fixed vector is 0: if every s fixes v, [F1] gives B(v,es)=0 for all s, so the dual-basis expansion [F4] gives v=∑sB(v,es)vs=0. Hence 0=pˉ∈int⁡P. Fourth, cs>0: if cs≤0 for some s, then for every ε>0 the point z=εvs has B(vs,z)=εB(vs,vs)>0≥cs, using positive definiteness [F4]; it violates the defining w=1,s inequality of Q=P. Such points approach 0 as ε→0, contradicting 0∈int⁡P. Thus each cs=B(vs,x) is positive. Therefore P=Q is presented by the finitely many affine inequalities cs−B(wvs,⋅)≥0 in the Euclidean space (V,B), is nonempty, bounded and compact, and contains 0 in its interior; by [F10] it is a compact convex polyhedral cell with 0 in its interior.

8.1step 1.2step 2.2step 3.1step 4.2step 6.1step 7.1F8F9F11given∎

The five clauses are now proved: (1) is [step 1.2] with [step 2.1]; (2) is [step 2.1] with [step 2.2]; (3) is [step 3.1]; (4) is [step 4.1], [step 5.1], [step 4.2], [step 6.1], [step 6.2]; and (5) is [step 7.1]. No axiom of choice is used: each selection is a single witness or a finite selection from a finite set, the maximal independent subset in [step 4.2] is chosen from finitely many candidates, [F9] uses only finite choice proved in ZF, and strict separation [F8] follows from the nearest-point variational inequality within ZF.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

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=RS 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 (ds)s∈S be positive real numbers. For T∈S (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization) put VT:=span⁡{es:s∈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 (WT,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 WT finite, the restriction of B to VT is positive definite by Finiteness criterion: W is finite exactly when the Coxeter form is positive definite (1), so BT:=B∣VT is an inner product (Real and complex inner-product spaces and their induced length). Let vs(T)∈VT (s∈T) be its B-dual basis, and put xT:=∑s∈Tds vs(T)∈VT,CT:=conv⁡(WT xT)⊆VT.

(1) Cells. For every spherical T, CT is a compact convex polyhedral cell of dimension ∣T∣ inside the Euclidean affine space (VT,BT) 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⁡(uWUxT), u∈WT, U⊆T, each occurring for exactly one coset uWU; face inclusion agrees with coset inclusion (and the simultaneously reversed face and coset orders also agree). The remaining face is ∅, which has no coset index. This is The finite-type Coxeter cell: exposed faces and normal cones applied to the finite-type system (WT,T) and the point xT in the open fundamental chamber {v∈VT:B(v,es)>0 for all s∈T}, whose distances to the simple mirrors are B(xT,es)=ds.

(2) Projections. For U⊆T, the B-orthogonal projection of xT onto VU is xU; equivalently xT=xU+zT,U with zT,U∈VU⊥∩VT, and zT,U is fixed by ρ(WU). In particular xU depends only on U and on the numbers ds with s∈U.

(3) Face isometries. For U⊆T and w∈WT, the affine map φwT,U ⁣:VU→VT,φ(v)=ρ(w)(v+zT,U), is a Euclidean isometry of (VU,BU) onto the affine span of the face conv⁡(wWUxT) and carries CU onto that face. Hence the intrinsic metric of the face conv⁡(wWUxT) of CT equals that of CU, and depends only on U, the numbers ds (s∈U) and no other choice.

(4) Cocycle. For spherical U⊆T⊆T′ and g1∈WT, g2∈WT′ one has φg2g1T′,U=φg2T′,T∘φg1T,U, an identity of isometries VU→VT′; consequently the face identifications of the cells CT 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=RS, positive numbers (ds)s∈S, and for each spherical T the space VT with the form BT=B∣VT, the dual basis vs(T), the point xT and the cell CT=conv⁡(WTxT).

[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)), (WT,T) is a Coxeter system of finite type, WT∩S=T, and BT is positive definite; the restriction ρ∣WT is the canonical reflection representation of the subsystem acting on VT with basis (es)s∈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⊆S and u∈WU one has ρ(u)VU=VU; every ρ(w) preserves B; and for s∈S the reflection formula gives ρ(s)v=v−2B(v,es)es (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 (es)s∈T form a basis of VT; their coordinate functionals es∗ 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∈B associated to a Hamel basis B, defined by b∗(c)=δbc). The finite-dimensional Riesz theorem for the real inner-product space (VT,BT) gives unique vectors vs(T) with es∗(y)=B(y,vs(T)); symmetry gives B(vs(T),et)=δst. For y∈VT, the difference y−∑s∈TB(y,es)vs(T) lies in VT and pairs to zero with every spanning vector et, so it is zero by positive definiteness. Also, for a subspace W0 of a finite-dimensional inner-product space there is a unique orthogonal decomposition v=PW0v+z with z⊥W0, and PW0v is the orthogonal projection (Finite-dimensional Riesz representation: every functional is uniquely v↦⟨v,w⟩, For a subspace W of a finite-dimensional inner product space, V=W⊕W⊥, The orthogonal projection PWv is the W-component in V=W⊕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 Cp→Cq→Cr and Cp→Cr agree whenever p≤q≤r (Abstract isometric polyhedral gluings and the chain metric).

Proof

technique · direct
1.1givenF1F2F4algebra

Fix a spherical T. By [F2] the subsystem (WT,T) is finite with positive definite BT, and ρ∣WT is its canonical representation; the element xT=∑s∈Tdsvs(T) satisfies BT(xT,es)=ds>0 for every s∈T by [F4], so xT lies in the open chamber of the subsystem. Applying [F1] to (WT,T), BT and xT gives clause (1): CT is a compact convex polyhedral cell of dimension ∣T∣ with 0 in its interior, its nonempty faces are exactly the sets conv⁡(uWUxT) for u∈WT, U⊆T, each for exactly one coset uWU, 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 ∅, which is not any of the nonempty orbit hulls. For T=∅, one has VT=CT={0}, and the faces are ∅ and {0}; only the latter is indexed by the unique coset W∅={1}.

2.1step 1.1F4algebra

Let U⊆T. For every t∈U the dual-basis identity of [F4] gives B(xT,et)=dt=B(xU,et); hence B(xT−xU,et)=0 for all t∈U, so xT−xU∈VU⊥∩VT. Since xU∈VU, this is the orthogonal decomposition of xT along VU, and uniqueness [F4] gives PVUxT=xU. Conversely, any decomposition xT=xU+z with xU∈VU and z∈VU⊥∩VT is that same unique orthogonal decomposition, so its VU-component is the projection. Put zT,U:=xT−xU.

3.1step 1.1step 2.1F3F4F5algebra

Let U⊆T and w∈WT. The affine map φwT,U(v)=ρ(w)(v+zT,U) has linear part ρ(w)∣VU, which maps VU into VT by [F3] applied to T, and preserves B by [F3]; translation then shows it is an isometry onto ρ(w)zT,U+ρ(w)VU by [F5]. To identify this image with the affine span of the face, first note that for every t∈U, [step 1.1] and the reflection formula give ρ(t)xT−xT=−2B(xT,et)et=−2dtet∈VU. Induction on a word u=vt in generators of WU gives ρ(u)xT−xT=ρ(v)(ρ(t)xT−xT)+(ρ(v)xT−xT)∈VU, because ρ(v)VU=VU by [F3]. Thus WUxT⊆xT+VU, while the differences ρ(s)xT−xT=−2dses for s∈U span VU since ds>0 and the es are linearly independent; hence aff⁡(WUxT)=xT+VU. Applying ρ(w) gives aff⁡(wWUxT)=ρ(w)xT+ρ(w)VU. Since xT=xU+zT,U by [step 2.1] and xU∈VU, this affine span is ρ(w)zT,U+ρ(w)VU, the image of φwT,U. Finally, for v,v′∈VU, B-invariance gives BT(φ(v)−φ(v′),φ(v)−φ(v′))=BU(v−v′,v−v′), so the affine isometry preserves the induced Euclidean distances.

3.2step 2.1F2F3algebra

The vector zT,U is fixed by ρ(WU): for s∈U the reflection formula [F3] gives ρ(s)xT=xT−2B(xT,es)es and ρ(s)xU=xU−2B(xU,es)es, and the two pairings are equal to ds by [step 2.1], so subtracting yields ρ(s)zT,U=zT,U; since U generates WU, this gives ρ(u)zT,U=zT,U for every u∈WU. Moreover xU=∑s∈Udsvs(U) is built from U and the numbers ds with s∈U only, so the same holds for the projected point of (2).

4.1step 1.1step 3.2step 3.1F5

The map φwT,U carries CU onto the face conv⁡(wWUxT): for u∈WU one has φwT,U(ρ(u)xU)=ρ(w)ρ(u)(xU+zT,U)=ρ(wu)(xU+zT,U)=ρ(wu)xT, because ρ(u)zT,U=zT,U by [step 3.2]; as u runs over WU, wu runs over the coset wWU, and φ is affine, so it maps the convex hull CU onto the convex hull of those points. Since φwT,U is an isometry [step 3.1], the intrinsic metric of the face equals that of CU by [F5]; and CU is built from U and the numbers ds with s∈U only, by [step 3.2].

4.2step 2.1step 3.2F4algebra

Let U⊆T⊆T′ be spherical. Then zT,U+zT′,T=zT′,U: both sides belong to VU⊥∩VT′, and xT′=xT+zT′,T=xU+zT,U+zT′,T while also xT′=xU+zT′,U; the orthogonal decomposition of xT′ along VU in (VT′,BT′) is unique by [F4], so the two complements agree.

5.1step 3.2step 4.2F6algebra

Cocycle. Let U⊆T⊆T′ be spherical, g1∈WT and g2∈WT′. By [step 3.2] applied to the pair T⊆T′, the vector zT′,T is fixed by ρ(WT), in particular by ρ(g1). Hence, using [step 4.2], φg2T′,T(φg1T,U(v))=ρ(g2)(ρ(g1)(v+zT,U)+zT′,T)=ρ(g2g1)(v+zT,U+ρ(g1)−1zT′,T)=ρ(g2g1)(v+zT′,U)=φg2g1T′,U(v). Thus the face isometries of the cells CT satisfy the cocycle condition of gluing data [F6] and are compatible on common faces: a coset w′WU⊆wWT carries both the identification of the face of CwWT with Cw′WU 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 WT are finite, and the only identifications are explicit isometries.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K)

Statement

Let (S,m) be a Coxeter matrix with S finite, W its presented group with length ℓ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), and let S, WS, Σ=∣WS∣, K=∣S∣, j ⁣:K→Σ be as in Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization. Let CT, zT,U and φwT,U be as in Finite Coxeter orbit polytopes, face isometries and their cocycle. For each spherical coset q=wWT, let q˙ be its unique element of minimum length, which exists by Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (3). Then:

(1) The cellulation is an isometric polyhedral gluing. Adjoining to WS a formal least element ∅ corresponding to the empty face gives a poset P whose principal down-sets are finite and are face posets of the compact convex polyhedral cells CT. For each q=wWT, take a copy Cq of CT with its coordinates in the chart determined by q˙. For p=w′WU⊆q=wWT, define the face isometry hp,q:=φq˙−1p˙T,U from Cp onto the face of Cq indexed by p. These cells and maps form an isometric polyhedral gluing X of shape P in the sense of Abstract isometric polyhedral gluings and the chain metric: the cocycle condition follows from Finite Coxeter orbit polytopes, face isometries and their cocycle (4), and the intersection condition holds because the intersection of two spherical cosets is a spherical coset of type T∩T′ or empty (Equality, inclusion and intersection of spherical cosets, and the quotient poset (3)), so the images of Cp and Cq meet exactly in the image of the face of Cp∧q. The standing hypotheses (H1)-(H3) hold: X is connected (it contains the Cayley graph on W), locally finite and has finitely many cell shapes (one for each T∈S, and S is finite). Consequently the chain metric d is a metric on X with the weak topology, and (X,d) is complete and proper in the sense of Complete metric space: every Cauchy sequence converges in the space and Open cover, subcover, compact metric space, and compact subset of a metric space, by The chain metric is a metric, its topology is the weak topology, and the space is proper and complete (1)-(3); and the canonical barycentric-subdivision map ∣WS∣→X of Face coherence, global hat coordinates and a uniform star radius (i) is a homeomorphism Σ≅X that carries the subposet WS≤q onto the barycentric subdivision of the cell Cq.

(2) Cells, incidence and stabilizers. Under this identification the cells of Σ are the images of the cells CwWT, of dimension ∣T∣; there is one W-orbit of cells for each spherical T; Σ has finitely many cell shapes and every closed cell meets only finitely many cells; the setwise stabilizer of the cell wWT is wWTw−1; and every point of Σ lies in the relative interior of exactly one cell. For q=wWT, use the chart fixed by its unique minimum-length representative q˙; if a point y in the relative interior of that cell corresponds to y′∈CT and y′ lies in the relative interior of the chamber face w0CIT of the finite-type chamber decomposition of VT (where w0∈WT, I⊆T, B(w0−1y′,es)=0 for s∈I and B(w0−1y′,es)>0 for s∈T∖I), then Stab⁡W(y)=(q˙w0)WI(q˙w0)−1, a conjugate of the spherical parabolic WI. In particular every point stabilizer is finite, is a spherical parabolic, and is contained in the setwise stabilizer wWTw−1 of its cell. The relative interiors of the cells partition Σ.

(3) The action is proper. The W-action on Σ is cellular and isometric for d, and it is proper: for every compact subset C⊆Σ the set {w∈W:wC∩C≠∅} is finite.

(4) Compact chamber quotient. Give W\Σ the quotient topology of the orbit projection Σ→W\Σ (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection). The projection WS→S induces a W-invariant continuous map p ⁣:Σ→K that is the identity on the chamber and maps every translated chamber simplex back to its simplex of K; passing to quotients gives a continuous bijection pˉ ⁣:W\Σ→K, and W\Σ is compact as the image of the compact chamber K under the quotient map, so pˉ is a homeomorphism (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism (1),(3)). In particular W\Σ is compact, and K, the chamber, is a strict fundamental domain for the action.

(5) The model U(W,K). Give W the discrete topology, W×K the product topology, and U(W,K):=(W×K)/ ⁣∼ the quotient topology (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection), where (w,x)∼(w′,x′) iff x=x′ and w−1w′ lies in the subgroup generated by S(x):={s∈S:x∈Ks} with Ks:=∣S≥{s}∣ (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups). Then [w,x]↦w⋅j(x) is a well-defined W-equivariant homeomorphism U(W,K)→Σ with inverse given by the carrier-simplex coordinates of Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization: a point of Σ lies in the relative interior of a unique carrier simplex, a chain w0WT0⊂⋯⊂wkWTk, and by Equality, inclusion and intersection of spherical cosets, and the quotient poset (2) the chain equals w0WT0⊂⋯⊂w0WTk, so the barycentric coordinates define a point of the simplex of K on T0⊂⋯⊂Tk; the two maps are mutually inverse by construction and continuous for the stated quotient and weak topologies.

Facts & Assumptions

Given: A finite Coxeter matrix (S,m), its presented group W, and the objects S, WS, Σ=∣WS∣, K=∣S∣, j, the cells CT, the projections zT,U and the face isometries φwT,U constructed in Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization and Finite Coxeter orbit polytopes, face isometries and their cocycle.

[F1]

The realization: WS is the poset of spherical cosets with the inclusion order and W acts on it by left multiplication preserving the type π(wWT)=T; Σ=∣WS∣ is its order complex; K=∣S∣ and j ⁣:K→Σ is the simplicial map T↦WT (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)-(4)).

[F2]

Coset calculus: wWU⊆w′WU′ iff U⊆U′ and w−1w′∈WU′; wWU=w′WU′ iff U=U′ and w−1w′∈WU; if wWU∩w′WU′≠∅ then the intersection is uWU∩U′ for every u in it, and it is nonempty iff w−1w′∈WUWU′; the left action is order-preserving, π-invariant and transitive on the cosets of each fixed parabolic (Equality, inclusion and intersection of spherical cosets, and the quotient poset (1)-(4)).

[F3]

Cell and face-map data: for spherical T, CT is a compact convex polyhedral cell of dimension ∣T∣. Its nonempty faces are conv(uWUxT) for u∈WT and U⊆T, each occurring for exactly one coset uWU, and face inclusion agrees with inclusion of the indexing cosets. The vector zT,U is fixed by ρ(WU), and the affine map φwT,U:CU→CT, v↦ρ(w)(v+zT,U), is an isometry onto the face indexed by wWU (Finite Coxeter orbit polytopes, face isometries and their cocycle (1)-(3)).

[F4]

Gluing definition: an isometric polyhedral gluing has finite face down-sets, affine face isometries satisfying the cocycle, an intersection condition, the weak topology, and standing hypotheses (H1)-(H3); its chain metric is defined from lengths of finite chains (Abstract isometric polyhedral gluings and the chain metric).

[F5]

Finite-type chamber facts: if T∈S, then WT is finite by [F1], clause (2) of Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification makes (WT,T) a Coxeter system, and [F17] identifies its reflection space with (VT,BT,ρ∣WT). The finite chamber theorem and arrangement definition then imply that the relative interiors of the faces w0CIT (w0∈WT, I⊆T) partition VT, and Stab⁡WT(y′)=w0WIw0−1 for y′ in the relative interior of w0CIT (The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1),(3), The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset).

[F6]

Topological compactness: K is compact and Hausdorff because it is a finite simplicial realization; continuous images of compact spaces are compact; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism (A finite simplicial complex has a compact Hausdorff realization, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism (1),(3), Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

[F7]

Every left coset q=aWT has a unique minimum-length representative q˙ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (3)); if p⊆q then q˙−1p˙∈WT by [F2].

[F8]

A left group action satisfies e⋅x=x and (gh)⋅x=g⋅(h⋅x) (Left group actions, transitive actions, and faithful actions).

[F9]

The compatible barycentric triangulation map ∣K′∣→X of the order complex of the nonempty faces is a homeomorphism for the weak topologies (Face coherence, global hat coordinates and a uniform star radius (i)).

[F10]

The chain metric is a metric inducing the gluing weak topology; every closed bounded subset is compact and the metric is complete (The chain metric is a metric, its topology is the weak topology, and the space is proper and complete (1)-(3), Open cover, subcover, compact metric space, and compact subset of a metric space, Complete metric space: every Cauchy sequence converges in the space).

[F11]

Give W the discrete topology and W×K the product topology; each slice map x↦(w,x) is continuous, and the quotient topology makes the orbit and model quotient projections continuous (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, The product set ∏i∈IXi of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).

[F12]

For a left action, Stab⁡W(x)={g∈W:g⋅x=x} (The orbit G⋅x and stabilizer Gx of a point in a group action).

[F14]

Every point has a neighborhood contained in a finite closed star meeting only finitely many cells (Face coherence, global hat coordinates and a uniform star radius (iii)).

[F15]

The group W is generated by the Coxeter generators S and ℓ is the word-length function from the Coxeter presentation (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F16]

The realization K=∣S∣ is compact and Hausdorff because it is a finite simplicial complex (A finite simplicial complex has a compact Hausdorff realization).

[F17]

A4 defines VT=span⁡{es:s∈T} and BT=B∣VT. For s∈T, the canonical reflection homomorphism sends s to res, and the Coxeter-form reflection formula restricts to v↦v−2BT(v,es)es on VT; thus VT is invariant and ρ∣WT is precisely the canonical reflection representation of (WT,T) (Finite Coxeter orbit polytopes, face isometries and their cocycle, The canonical reflection homomorphism, roots, reflections, and the positive cone, The real Coxeter form, its radical, reflections, and form-preserving maps).

[F13]

For spherical U⊆T⊆T′, the face isometries satisfy φg2g1T′,U=φg2T′,T∘φg1T,U for g1∈WT and g2∈WT′ (Finite Coxeter orbit polytopes, face isometries and their cocycle (4)).

Proof

technique · direct
1.1givenF1F2F3algebra

The poset P:=WS∪{∅} with ∅ below every coset [F1]: for p=wWT the principal down-set P≤p consists of ∅ and the cosets w′WU⊆wWT, which by [F2] are exactly the cosets w′WU with U⊆T and w′∈wWT; it is finite because WT and the set of subsets of the finite T are finite. The map w′WU↦conv⁡((w−1w′)WUxT) is a bijection from P≤p∖{∅} onto the nonempty faces of CT by [F3], it is order-preserving and reflecting by [F2] and [F3], and extending it by ∅↦∅ sends the formal least element to the empty face; hence P≤p is isomorphic to the face poset of CT.

1.2givenF2F3F4F7F13algebra

Gluing data. For p=p˙WU≤q=q˙WT, [F2] gives U⊆T and [F7] gives g:=q˙−1p˙∈WT. Put Cp:=CU, Cq:=CT and hp,q:=φgT,U; by [F3] this is an isometry from Cp onto the face of Cq indexed by p. If p≤q≤r with types U⊆V⊆T, then [F3] gives hq,r∘hp,q=φr˙−1q˙T,V∘φq˙−1p˙V,U=φ(r˙−1q˙)(q˙−1p˙)T,U=φr˙−1p˙T,U=hp,r, so the cocycle condition of [F4] holds. The unique representatives in [F7] make every map independent of notation for coset representatives; no choice of representatives is made.

2.1step 1.2F2F3F4algebra

Intersection condition. Let p=wWT, q=w′WT′ be cosets. For y∈Cp, define its address r≤p to be the unique spherical coset indexing the face whose relative interior contains y; existence and uniqueness are the face decomposition of the polytope CT in [F3]. If p≤q, write p=p˙WU, q=q˙WV, and r=p˙ uWJ. The map hp,q=φq˙−1p˙V,U sends the face of CU indexed by uWJ to the face of CV indexed by (q˙−1p˙)uWJ [F3], which has global label q˙(q˙−1p˙)uWJ=r; hence it preserves the address. For a point y∈Cp with address r, set ξ(y):=hr,p−1(y)∈Cr. If p≤q, the cocycle gives hr,q=hp,q∘hr,p, so ξ is unchanged by the generating identification y∼hp,q(y); it is also unchanged by the inverse identification. Therefore equivalent points have the same address and the same ξ. Conversely, if y∈Cp and y′∈Cq have the same address r and the same coordinate ξ, each is identified with that common point of Cr, so y∼y′. Thus equivalence is exactly equality of address and ξ. In particular each map Cp→X is injective, since equal classes from Cp have the same address and coordinate and hr,p is injective. If two cell images meet, their common class has an address r≤p,q, hence r≤p∧q and lies in the image of Cp∧q; conversely every point of Cp∧q lies in both images, with the empty meet interpreted as the empty set. This is the intersection condition of [F4].

3.1step 2.1F2F3F4F15algebra

The standing hypotheses. X is connected: the 1-cells CwW{s}=conv⁡({x{s},sx{s}}) join the 0-cells with addresses wW∅={w} and wsW∅={ws} (which are faces of those 1-cells by [F3]), so the image of the disjoint union contains a copy of the connected Cayley graph of (W,S) on the vertices w; and every cell CwWT contains the 0-cell of w as the face indexed by wW∅≤wWT [F3], so every cell is attached to that graph and X is connected. It is locally finite: by [step 2.1] the cells whose image contains the class of a point y of address r=wrWT(r) are exactly the cells Cq with q≥r, and by [F2] a coset containing wrWT(r) has the form wrWT′ with T′⊇T(r); these are finitely many because S is finite. There are finitely many shapes because the cells are the CT, T∈S, and S is finite.

4.1step 1.1step 1.2step 2.1step 3.1F4F9F10

Conclusion of (1). By [step 1.1] the shape P has finite down-sets isomorphic to face posets of the cells CT; by [step 1.2] the maps hp,q are the face isometries of a gluing satisfying the cocycle condition; by [step 2.1] the intersection condition holds; by [step 3.1] the hypotheses (H1)-(H3) hold. Hence the metric theorem [F10] applies: the chain metric d is a metric on X inducing the weak topology, and every closed d-bounded subset of X is compact, so (X,d) is complete and proper. The canonical map f ⁣:∣WS∣→X of [F9] is a bijection and is affine on each simplex of ∣WS∣; it is continuous because ∣WS∣ carries the weak topology and each restriction to a closed simplex is affine; and its inverse is described on each closed cell of X by the carrier-simplex coordinates of [F9], hence is also affine on each simplex of the subdivision and continuous. So f is a homeomorphism Σ≅X, and by [F9] it carries the subposet WS≤wWT onto the barycentric subdivision of the cell CT.

5.1step 2.1step 4.1F2F3

Clause (2), incidence. Under the homeomorphism Σ≅X the cells of Σ are the images of the cells CwWT of dimension ∣T∣ by [F3] and [step 4.1]; W acts on the set of cosets of each fixed type transitively by [F2], so there is one orbit per spherical T; there are finitely many shapes since S is finite; and every closed cell meets only finitely many cells: the cells meeting the closed cell wWT are the vWV with vWV∩wWT≠∅, equivalently v∈wWTWV by [F2]; as V ranges over the finitely many spherical subsets and WV and WT are finite, these are finitely many cells. The relative interiors of the cells partition Σ because two cells meet in the image of Cp∧q [step 2.1], and within one cell the relative interiors of its faces partition it [F3]. The setwise stabilizer of the cell wWT is wWTw−1: v⋅wWT=vwWT equals wWT iff w−1vw∈WT by [F2].

5.2step 4.1F1F2F6F7F8F11F16algebra

Clause (4). Let π ⁣:WS→S be the type map. On each simplex of Σ belonging to a chain q0⊂⋯⊂qk, map the vertex qi to π(qi) and extend affinely; this defines a continuous map p ⁣:Σ→K because the type map preserves inclusions [F2] and Σ has the weak topology. It satisfies p∘j=idK and is W-invariant because π(vq)=π(q) [F2]. Every simplex is a left translate of a simplex of K: if q0=q˙0WT0, then for each i, [F2] gives qi=q˙0WTi, so left multiplication by q˙0−1 takes the chain to WT0⊆⋯⊆WTk. Thus the orbit projection qΣ ⁣:Σ→W\Σ restricts to a surjection on K. If x,x′∈K and v⋅x=x′, then W-invariance gives x=p(x)=p(v⋅x)=p(x′)=x′, so K meets each orbit exactly once. The induced map pˉ ⁣:W\Σ→K is continuous because pˉ∘qΣ=p and the quotient topology makes qΣ a quotient map: for open V⊆K, qΣ−1(pˉ−1(V))=p−1(V) is open. The restriction qΣ∣K is continuous and surjective, so W\Σ is compact as a continuous image of compact K [F6]. Since K is Hausdorff, [F6] makes pˉ a homeomorphism. Hence K is a strict fundamental domain.

6.1step 3.1step 4.1step 5.1F2F3F4F7F8F9F10F14

Clause (3), action and properness. For a coset q=wWT and v∈W, put a(v,q):=vq˙−1vq˙∈WT by [F2], [F7], and define Lv ⁣:Cq→Cvq in the type-T charts by Lv=ρ(a(v,q))∣CT. This is an isometry because a(v,q)∈WT permutes the orbit vertices of CT. Also a(1,q)=1, so L1=id, and a(u,vq)a(v,q)=uvq˙−1uvq˙=a(uv,q), so LuLv=Luv; these are the left-action identities [F8]. If p≤q has types U⊆T, let g:=q˙−1p˙, aq:=a(v,q), ap:=a(v,p), and g′:=vq˙−1vp˙=aqgap−1. For x∈CU, [F3] says ap∈WU fixes zT,U, so Lv∣Cq(hp,q(x))=ρ(aqg)(x+zT,U)=ρ(g′)ρ(ap)(x+zT,U)=hvp,vq(Lv∣Cp(x)). Thus Lv preserves the equivalence relation defining X and descends to an action by cellwise isometries. It preserves the chain metric because it sends each chain to one of the same length, and its inverse is Lv−1. Each Lv∣Cq carries the vertices of Cq to those of Cvq, hence sends their barycentres to each other; the affine barycentric maps on carrier simplices show that this action agrees, under [step 4.1], with the natural left action on Σ. For properness, let C⊆Σ be compact. By [F14], every point has a neighborhood contained in a finite closed star, hence meeting only finitely many cells; finitely many such neighborhoods cover C, so C meets only finitely many cells. For cells uWT and vWT′, the set of w with w(uWT)∩vWT′≠∅ equals vWT′WTu−1: [F2] says exactly that (wu)−1v∈WTWT′. This set is finite because WT and WT′ are finite. There are only finitely many pairs of cells meeting C, so only finitely many w satisfy wC∩C≠∅.

6.2step 4.1step 5.2F1F2F7F8F11algebra

Clause (5). Let R be the relation on W×K in the statement and put S(x)={s:x∈Ks}. If the carrier chain of x∈K is T0⊂⋯⊂Tk, then x∈Ks=∣S≥{s}∣ exactly when every vertex of that carrier chain contains s, which is equivalent to s∈T0. Thus S(x)=T0 and the subgroup it generates is WT0 (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups). For u∈WT0, the chamber carrier chain WT0⊂⋯⊂WTk has each vertex fixed by u, since [F2] gives uWTi=WTi; hence u fixes j(x). The relation R is an equivalence relation because on each fibre over x it is equality of left cosets of the subgroup WT0, and [w,x]↦w⋅j(x) is well defined by the fixed-point calculation. It is W-equivariant and surjective: a point with carrier chain q0⊂⋯⊂qk has, by [F2], the form q˙0WT0⊂⋯⊂q˙0WTk; its barycentric coordinates give x in the chamber simplex on T0⊂⋯⊂Tk, and its image is q˙0⋅j(x). It is injective: if w⋅j(x)=w′⋅j(x′), equality of carrier simplices and barycentric coordinates gives x=x′ and wWT0=w′WT0; therefore w−1w′∈WT0=WS(x) and [w,x]=[w′,x′]. For continuity, the map F ⁣:W×K→Σ, F(w,x)=w⋅j(x), is continuous: the slices {w}×K are open and its restriction to each is the continuous map x↦w⋅j(x). It is constant on R-classes, so it descends continuously through the quotient projection by [F11]. For the inverse, on a simplex with chain q0⊂⋯⊂qk, use the unique representative q˙0 and the affine barycentric-coordinate map to its chamber simplex in K, then send that point x to [q˙0,x]. This is continuous on the simplex by the product and quotient topologies [F11]. These formulas agree on common faces: when the minimum coset rises to qj, both representatives lie in qj, so their quotient classes agree because q˙0−1q˙j∈WTj=WS(x). The weak topology of Σ is simplexwise, so the inverse is continuous. The two maps are mutually inverse by the carrier-chain construction, proving the claimed homeomorphism.

7.1step 4.1step 5.1step 6.1F2F5F7F8F12F17algebra

Clause (2), point stabilizers. Let q=wWT and let y lie in the relative interior of its cell, with coordinate y′∈CT in the q˙-chart. Let w0∈WT, I⊆T be determined by y′∈w0CIT (relative interior of a chamber face, [F5]). Let z be the point of the copy CWT=CT corresponding to y′ under the barycentric subdivision of [step 4.1]. For every v∈WT, a(v,WT)=v, so [step 6.1] makes the action on this copy exactly ρ(v), and y corresponds to q˙⋅z under Σ≅X. The subdivision pairs each vertex uWU with the face conv⁡(uWUxT) by [step 1.1], and ρ(v) carries this face to conv⁡(vuWUxT); as an isometry it carries each face barycentre and its barycentric coordinates to the corresponding ones. Thus Stab⁡W(z)∩WT=Stab⁡WT(y′)=w0WIw0−1 by [F5], using the stabilizer definition [F12]. Any element fixing z preserves the cell whose relative interior contains z; the cell is unique by [step 5.1], and its setwise stabilizer is WT by [step 5.1]. Hence Stab⁡W(z)=w0WIw0−1 and Stab⁡W(y)=q˙Stab⁡W(z)q˙−1=(q˙w0)WI(q˙w0)−1. This is a conjugate of the spherical parabolic WI, and it lies in the setwise stabilizer wWTw−1 because w0WIw0−1≤WT and q˙∈wWT.

8.1step 1.2step 4.1step 6.1step 6.2step 7.1step 5.2given∎

The clauses are proved: (1) is [step 4.1], (2) is [step 5.1] with [step 7.1], (3) is [step 6.1], (4) is [step 5.2] and (5) is [step 6.2]. No Choice is used: coset charts use the unique minimum-length representatives of [F7], all chamber and cell models are finite, and the topological and metric arguments use no selection from an arbitrary family.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

The Davis complex as a CW complex: disk cells and the Cayley skeleta

Statement

Let (S,m) be a Coxeter matrix with S finite, W its presented group, and let Σ carry the cellulation of The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) with cells the spherical cosets wWT, T∈S (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization); write S for the spherical subsets and CT for the Coxeter cells of Finite Coxeter orbit polytopes, face isometries and their cocycle. Then:

(1) The cells are disks. For T=∅, CT={0} is the closed zero-ball. For nonempty T, the cell CT is homeomorphic to the closed disk B‾(0,1)⊆VT by the radial map ψ ⁣:CT→B‾(0,1),ψ(0)=0,ψ(x)=xtmax⁡(x/∥x∥B) (x≠0), where tmax⁡(u)=min⁡{ℓi(0)/(ℓi(0)−ℓi(u)):ℓi(u)<ℓi(0)} is the exit parameter of the unit ray through u for a finite list of affine functions ℓi≥0 defining CT={v:ℓi(v)≥0} with ℓi(0)>0; ψ carries the boundary ∂CT onto the unit sphere. Consequently the cells wWT admit characteristic maps from closed ∣T∣-disks (Cell attachment by a characteristic map).

(2) CW structure. With these characteristic maps and the face-identification attaching maps, the cellulation is a CW complex in the sense of CW complex with closure finiteness and weak topology: the weak topology is the topology of the gluing of The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K), and the cells meeting the closed cell wWT are the cells vWV with vWV∩wWT≠∅, equivalently v∈wWTWV; by Equality, inclusion and intersection of spherical cosets, and the quotient poset (3) and the finiteness of the spherical subsets V and of both WT and WV these are finitely many, so the closure finiteness condition (C) holds.

(3) Skeleta. The skeleta (Skeleta, CW subcomplexes, and relative CW complexes) are: Σ0=W, the cosets wW∅={w}; Σ1 is the (undirected, S-labelled) Cayley graph of (W,S) (The Cayley graph of a group with respect to a subset, The directed labelled Cayley graph of a group with respect to a subset), each 1-cell wW{s}={w,ws} being an edge labelled s; and Σ2 is Davis's reduced Cayley 2-complex of the Coxeter presentation W=⟨S∣s2 (s∈S), (st)m(s,t) (s≠t, m(s,t)<∞)⟩: the involution relators s2 contribute only edge backtracks, with no 2-cells, and the finite pair-relator circuits are identified up to cyclic shift and reversal; its 2-cells are the cosets wW{s,t} with m(s,t)<∞, each a 2m(s,t)-gon whose boundary closed edge path is w,ws,wst,…,w(st)m(s,t)=w.

(4) Two-dimensional case. For ∣T∣=2, CT is the regular 2m(s,t)-gon when ds=dt, and for ∣T∣=1, CT is the interval from −dses to dses; the cellulation has no cells of dimension ≥3 exactly when no three-element spherical subset exists.

Facts & Assumptions

Given: A finite Coxeter matrix (S,m), its presented group W, the spherical subsets S, the Davis realization Σ=∣WS∣, the cells CT=conv⁡(WTxT), and the cell charts indexed by spherical cosets wWT.

[F1]

For nonempty spherical T, in the finite-dimensional Euclidean space (VT,BT) the cell CT is bounded, contains 0 in its interior, and is defined by finitely many affine inequalities ℓi(v)≥0 with ℓi(0)>0 (The finite-type Coxeter cell: exposed faces and normal cones (5), applied to (WT,T)).

[F2]

For every spherical T, CT has dimension ∣T∣, its generating point is xT=∑s∈Tdsvs(T) with B(xT,es)=ds, and its nonempty faces are exactly conv⁡(uWUxT) for u∈WT, U⊆T, each indexed by exactly one coset; face inclusion agrees with coset inclusion (Finite Coxeter orbit polytopes, face isometries and their cocycle (1)).

[F3]

The canonical barycentric-subdivision map ∣WS∣→X is a homeomorphism Σ≅X carrying the subposet below each spherical coset q onto the barycentric subdivision of its cell Cq (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1)).

[F16]

Under the cellulation identification, the cells indexed by wWT have dimension ∣T∣, and every point lies in the relative interior of exactly one cell (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (2)).

[F4]

A characteristic map is a continuous map from a closed disk whose interior maps homeomorphically onto the open cell and whose boundary maps into the preceding skeleton (Cell attachment by a characteristic map).

[F5]

A homeomorphism is a continuous bijection with continuous inverse (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

[F6]

A CW complex is Hausdorff and has a filtration by skeleta with closure finiteness and the weak-topology condition (CW complex with closure finiteness and weak topology).

[F7]

The skeleta are the subcomplexes formed by cells of dimension at most the given degree (Skeleta, CW subcomplexes, and relative CW complexes).

[F8]

The choice-free attachment lemma constructs a CW complex from supplied cells with finite boundary support and their weak attachment topology (Cellular attachments with finite boundary support form a CW complex).

[F9]

A subset T is spherical exactly when WT is finite, and W∅={1} (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization).

[F10]

For every T⊆S, WT is the Coxeter group with restricted Coxeter matrix on T; when T={s} the presentation has only s2=1, so every word reduces to 1 or s, and the map to the two-element group sending s to its nonidentity element separates them. Hence W{s}={1,s} (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2), Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F11]

The undirected Cayley graph has vertices W and edges {g,gs}, while its directed labelled version has an arc (g,s,gs) for each g∈W, s∈S (The Cayley graph of a group with respect to a subset, The directed labelled Cayley graph of a group with respect to a subset).

[F12]

For a presentation, Davis's Cayley 2-complex attaches 2-cells along circuits of relators other than words s or s2; circuits are identified up to cyclic shift and reversal, and cells are attached equivariantly by the group (Davis, The Geometry and Topology of Coxeter Groups, §2.2, pp. 19–20). Thus the Coxeter relators (st)m(s,t) with distinct s,t and finite m(s,t) supply the 2-cells, while the involution relations s2 do not add 2-cells.

[F13]

In a finite rank-two Coxeter system the simple mirrors bound the fundamental sector of angle π/m (The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (2)). Their reflections preserve the positive-definite plane form, and their product has determinant 1 and trace 2cos⁡(2π/m), hence is a rotation by ±2π/m (Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2),(3)).

[F14]

B(es,es)=1 (The real Coxeter form, its radical, reflections, and form-preserving maps (2)).

[F19]

The simple reflection formula is res(v)=v−2B(v,es)B(es,es)es (The real Coxeter form, its radical, reflections, and form-preserving maps (3)).

[F20]

The notation rs means res for every s∈S (The canonical reflection homomorphism, roots, reflections, and the positive cone).

[F21]

The canonical reflection homomorphism satisfies ρ(s)=rs for every s∈S (The canonical reflection homomorphism, roots, reflections, and the positive cone (1)).

[F15]

For spherical T,V, the coset subsets meet exactly when w−1v∈WTWV (Equality, inclusion and intersection of spherical cosets, and the quotient poset (3)).

[F17]

In the isometric gluing, U⊆X is open exactly when U∩ιp(Cp) is relatively open in every cell image ιp(Cp) (Abstract isometric polyhedral gluings and the chain metric, Definition (iii)).

[F18]

The cell intersection condition says that images of cells indexed by spherical cosets meet exactly in the image of the face indexed by their intersection coset, and are disjoint when the cosets are disjoint (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1)).

Proof

technique · direct
1.1givenF1algebra

Fix a spherical T. If T=∅, then VT={0}, xT=0, and CT={0}, so the unique map from this point to the closed zero-ball is a homeomorphism and both boundaries are empty. Suppose T≠∅. Write CT={v:ℓi(v)≥0 (i∈I)} as in [F1], with I finite and ℓi(0)>0. For a unit vector u∈VT, at least one index satisfies ℓi(u)<ℓi(0): otherwise ℓi(su)=ℓi(0)+s(ℓi(u)−ℓi(0))≥0 for every s≥0 and every i, so the whole ray would lie in the bounded set CT. Along that ray, each index with ℓi(u)<ℓi(0) imposes s≤ℓi(0)/(ℓi(0)−ℓi(u)), while the other indices impose no upper bound. Thus CT∩{su:s≥0}={su:0≤s≤tmax⁡(u)}, with tmax⁡(u) the finite positive minimum in clause (1).

1.2F6F9F15F17F18algebra

By [F18], the closed cells vWV and wWT meet exactly when the spherical coset subsets vWV and wWT meet. By [F15], this is equivalent to w−1v∈WTWV, hence to v∈wWTWV; conversely, v=wab with a∈WT, b∈WV gives the common element wa=vb−1. There are finitely many spherical V⊆S, and each product wWTWV is finite because spherical WT,WV are finite. Thus only finitely many cells meet a fixed closed cell, proving closure finiteness (C). The gluing definition [F17] tests openness cellwise; by taking complements this is exactly condition (W) in [F6].

2.1step 1.1F1algebra

Assume T≠∅. For each unit u0, let I0={i:ℓi(u0)<ℓi(0)}, which is nonempty by [step 1.1]. Every fi(u)=ℓi(0)/(ℓi(0)−ℓi(u)) for i∈I0 is continuous near u0. If i∉I0 and ℓi(u0)>ℓi(0), that index remains inactive near u0; if ℓi(u0)=ℓi(0), its value tends to +∞ whenever it becomes active as u→u0. Choose j∈I0; fj stays bounded on a sufficiently small neighborhood, so after shrinking that neighborhood no newly active equality index can attain the minimum. There tmax⁡=min⁡i∈I0fi, proving continuity at u0. By [F1], choose ϵ>0 with {v:∥v∥B<ϵ}⊂CT and R<∞ with CT⊆{v:∥v∥B≤R}. The ray description gives ϵ≤tmax⁡(u)≤R for every unit u.

3.1step 1.1step 2.1F1F5algebra

For T≠∅, define θ:B‾(0,1)→CT by θ(0)=0 and, for y≠0, t=∥y∥B, u=y/t, and θ(y)=t tmax⁡(u)u. The ray description shows θ(y)∈CT. If x=su∈CT with u unit, then ψ(x)=(s/tmax⁡(u))u and θ(ψ(x))=x; conversely, for y=tu≠0, ψ(θ(y))=tu=y, and both composites fix 0. Away from 0 both maps are continuous by continuity of tmax⁡; at 0, ∥θ(y)∥B≤R∥y∥B and ∥ψ(x)∥B≤∥x∥B/ϵ, so both are continuous there. Thus θ and the stated ψ are mutually inverse homeomorphisms by [F5]. For s<tmax⁡(u) all inequalities defining CT are strict at su, so continuity of the finite affine list makes su an interior point; at s=tmax⁡(u) at least one inequality is equality, and for every larger s that inequality fails. Thus the boundary consists exactly of tmax⁡(u)u for unit u, and ψ maps it onto the unit sphere.

4.1step 3.1F1F2F3F4F5F16

For nonempty T, the map θ of [step 3.1], followed by the cell chart CT→CwWT⊆Σ of [F3], is a characteristic map for the cell indexed by wWT. Its interior maps homeomorphically onto the open cell by [F16]. If x is a boundary point, some defining inequality ℓi(x) is 0, since otherwise the finite affine list stays positive in a neighborhood of x; then CT∩{ℓi=0} is a face: if a strict convex combination has ℓi-value 0, both endpoint values are 0. It is proper because ℓi(0)>0; by [F2] it is a lower-dimensional cell. Thus the boundary maps into the preceding skeleton. For T=∅, the one-point chart is the characteristic map of a zero-cell, with empty boundary.

5.1step 4.1step 1.2F2F3F4F5F6F7F8F17

Each cell boundary is a union of finitely many proper nonempty faces by [F2], and each such face is indexed by w′WU with U⊊T, so it lies in the preceding skeleton since its dimension is ∣U∣<∣T∣. For a zero-cell this is the empty union. The zero-skeleton is the discrete set W. Attach the characteristic disks of [step 4.1] in increasing dimension; every attaching map has finite boundary support, and the weak attachment topology agrees with the gluing topology from [F17] because it tests openness on closed cell images, and each characteristic map is a homeomorphism onto its closed cell by [F3],[F5]. Since S is finite, there are finitely many dimensions. The choice-free attachment lemma [F8] therefore gives the asserted CW structure with the given cells and topology, including its Hausdorff condition.

6.1step 5.1F2F3F7F9F10F11F12F16algebra

The zero-cells are wW∅={w} by [F3] and [F9], so Σ0=W. Each one-cell is wW{s}={w,ws} and its boundary vertices are w and ws; its label is s, giving exactly the undirected Cayley graph by [F11]. Now fix distinct s,t and put m=m(s,t). By [F10], W{s,t} has presentation ⟨s,t∣s2=t2=1,(st)m=1⟩ if m<∞, and omits the last relation if m=∞. When m<∞, writing r=st and using srs=r−1 reduces every word to rk or srk, 0≤k<m, so the group has at most 2m elements. The map to the group of pairs Dm=Z/m×{±1} with multiplication (a,ϵ)(b,δ)=(a+ϵb,ϵδ), s↦(0,−1) and t↦(1,−1), is onto: these images are involutions and their product (−1,1) generates the rotation subgroup; hence ∣Dm∣=2m gives ∣W{s,t}∣=2m. When m=∞, the maps s(x)=−x, t(x)=2−x on R satisfy the involution relations and make st a nonzero translation, so W{s,t} is infinite. Hence {s,t} is spherical exactly when m<∞. For finite m, the boundary walk of wW{s,t} alternates the s- and t-edges and has vertices w(st)k and w(st)ks (0≤k<m), all distinct by the dihedral normal forms; it closes at w(st)m=w. By [F2] these alternating rank-one cosets are edges of the cell, so the closed walk through all 2m vertices is its polygon boundary. Translates of this circuit are indexed by the left cosets wW{s,t}, since its vertices are exactly that coset and its cyclic order is the unique alternating circuit in the rank-two Cayley graph. By [F12], the 2-cells are precisely these circuits: the relators (st)m attach polygonal cells and the relators s2 add none.

7.1step 6.1F2F3F9F13F14F16F19F20F21algebra

For T={s}, vs(T)=es because B(es,es)=1, so xT=dses by [F2]; since rs=res by [F20] and ρ(s)=rs by [F21], [F19] gives sxT=−dses and CT=[−dses,dses]. For T={s,t} with finite m, [step 6.1] gives the 2m-gon. By [F13], its generating mirrors bound a sector of angle π/m; equality ds=dt means xT is equidistant from those walls, hence lies on their angle bisector. The product of the two wall reflections rotates by 2π/m, so the dihedral orbit has arguments θ+2kπ/m and −θ+2kπ/m with θ=π/(2m), which are the 2m equally spaced arguments θ+jπ/m; their convex hull is regular. Finally, cells of dimension at least 3 correspond exactly to spherical subsets of size at least 3 by [F2], [F3], and [F16]; any such subset contains a spherical three-element subset because its parabolic subgroup is finite by [F9], and every spherical three-element subset gives a three-dimensional cell. Thus there are no cells of dimension ≥3 exactly when no three-element spherical subset exists.

8.1step 3.1step 4.1step 1.2step 5.1step 6.1step 7.1F8given∎

Clauses (1)–(4) follow from [step 3.1] with [step 4.1], [step 1.2] with [step 5.1], [step 6.1], and [step 7.1], respectively. No Choice is used: each exit parameter is a minimum over a specified nonempty finite set, and all cell maps and attachments are explicitly supplied; the finite-dimensional disk identifications require only finite-dimensional Euclidean bases.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The Davis complex is simply connected

Statement

Let (S,m) be a Coxeter matrix with S finite, W its presented group (Group presentation by generators and relations, Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), and let Σ be the Davis realization of Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization with the CW structure of The Davis complex as a CW complex: disk cells and the Cayley skeleta. Then Σ is simply connected (Simply connected topological spaces, Based loops and the fundamental group). More precisely, for every vertex v∈Σ0=W, inclusion j ⁣:Σ2↪Σ induces an isomorphism j∗ ⁣:π1(Σ2,v)→π1(Σ,v), these groups are trivial, and in particular π1(Σ2,1) is trivial.

Facts & Assumptions

Given: A finite Coxeter matrix (S,m), its presented group W, and the Davis realization Σ with its CW structure and skeleta.

[F1]

The CW structure has Σ0=W, Σ1 the undirected S-labelled Cayley graph, and Σ2 the Cayley 2-complex whose 2-cells are the cosets wW{s,t} for distinct s,t with finite m(s,t), each a 2m(s,t)-gon with the Coxeter-relator boundary (The Davis complex as a CW complex: disk cells and the Cayley skeleta (2)-(3)).

[F2]

The skeleta of a CW complex are subcomplexes, so (Σ,Σ0) and (Σ,Σ2) are CW pairs and Σ2 is itself a CW complex (CW complex with closure finiteness and weak topology, Skeleta, CW subcomplexes, and relative CW complexes, The Davis complex as a CW complex: disk cells and the Cayley skeleta (2)-(3)).

[F3]

For CW pairs (X,A) and (Y,B), if X∖A has finitely many cells and a map of pairs is cellular on A, it is homotopic rel A through maps of pairs to a cellular map; for a finite relative source this clause uses no Choice (Cellular approximation for maps of CW pairs).

[F4]

The Coxeter presentation is W=F(S)/N, with N the normal closure of R={s2:s∈S}∪{(st)m(s,t):s≠t, m(s,t)<∞}; a word represents 1 in W iff it lies in N, and every element of N is a finite product of conjugates of relators and their inverses (Group presentation by generators and relations, Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, In ⟨X∣R⟩, the words u and v represent the same element if and only if u−1v∈⟨ ⁣⟨R⟩ ⁣⟩, The normal closure of R is the set of finite products of conjugates of elements of R and their inverses).

[F5]

In F(S), words use the alphabet S∪S−1; equality is generated by insertion and deletion of adjacent inverse pairs, and each element has a reduced-word representative (Free group on a set of generators, Words in an alphabet with formal inverses, elementary cancellation, and reduced words, Reduced words form the free group on an alphabet).

[F6]

Based loop classes form a group with the constant loop as identity and reverse paths as inverses; a continuous pointed map induces a homomorphism on π1; a space is simply connected when it is nonempty, path-connected, and its fundamental groups are trivial (Based loops and the fundamental group, Loop classes form the group π1(X,x0) under concatenation, The homomorphism on fundamental groups induced by a pointed continuous map, Simply connected topological spaces, Paths, path-connected spaces and path components).

[F7]

Each spherical-coset cell is a convex polytope, and for q=wWT its face indexed by wW∅={w} is a vertex; S generates W, so the Cayley graph on W is connected (The cellulation of the Davis complex: incidence, stabilizers and the model U(W,K) (1)-(2), Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)-(2), Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F8]

For each s∈S, the one-generator parabolic is W{s}={1,s}: its restricted presentation reduces every word to 1 or s, and the map to the two-element group separates them (The Davis complex as a CW complex: disk cells and the Cayley skeleta Fact [F10]).

[F9]

For a finite simplicial source and subcomplexes A,B, a map of pairs has a simplicial approximation after sufficiently many barycentric subdivisions and a homotopy through maps of pairs; the proof uses only finite choice (Finite simplicial approximation for maps of pairs). If B is the singleton basepoint, this homotopy fixes it.

Proof

technique · direct
1.1givenF1F2F3

A loop in either X=Σ or X=Σ2 based at a vertex v is homotopic rel v in X to an edge loop. Give S1 the CW structure with one 0-cell ∗ and one 1-cell, and view the loop as a map of pairs (S1,∗)→(X,X0). It is cellular on the 0-skeleton because it sends ∗ to v∈X0=Σ0; the relative source S1∖{∗} is one cell, so [F3] gives a cellular approximation rel ∗, whose image lies in X1=Σ1.

2.1step 1.1F1F2F3

Suppose a loop β in Σ2 based at a vertex v is null-homotopic in Σ, so it has a based homotopy H ⁣:I2→Σ with H(s,0)=β(s), H(s,1)=v, and H(0,t)=H(1,t)=v. Use [step 1.1] with X=Σ2 to homotope β rel endpoints to an edge loop β′ by F ⁣:I2→Σ2, where F(s,0)=β(s) and F(s,1)=β′(s). Define H′(s,t)=F(s,1−2t) for 0≤t≤12 and H′(s,t)=H(s,2t−1) for 12≤t≤1; the two formulas agree at t=12, and H′ is a based null-homotopy of β′. Its boundary is cellular for (I2,∂I2)→(Σ,Σ2): the bottom edge maps into Σ1, and the other boundary edges and vertices map to v∈Σ0. The relative source has one open 2-cell, so [F3] gives a cellular approximation rel boundary; because the source has dimension 2, its image lies in Σ2. Thus β′ and then β are null-homotopic in Σ2.

2.2step 1.1F1F4F5F6F8F9

Every continuous loop in Σ1 based at 1 is based-homotopic to a finite edge walk. Barycentrically subdivide the Cayley graph to an abstract simplicial graph: every original edge is split at its midpoint, so distinct original edges give distinct simplicial edges. Triangulate the circle with the basepoint as a vertex, and apply [F9] with the singleton basepoint as each distinguished subcomplex. The resulting map on a finite subdivided circle is a finite walk in the subdivided graph, with a homotopy fixing the basepoint. Delete stationary traversals and immediate reversals; at each midpoint the two incident half-edges either reverse or join to one full original edge, so compressing gives a finite based edge walk in the original graph. We now show that each such walk is null-homotopic in Σ2. Orient each traversal and record s or s−1 according to its direction, obtaining a word w∈F(S) whose image in W is 1 by [F1]. By [F4], w is a finite product g1r1ϵ1g1−1⋯gkrkϵkgk−1 in F(S), with ri∈R and ϵi∈{1,−1}; k=0 is allowed. The path for this product is a concatenation of conjugate relator loops, and [F5] turns equality in F(S) into finitely many insertions or deletions of adjacent inverse letters. Since each Coxeter generator satisfies s=s−1 in W, each such pair is an immediate backtrack in the undirected Cayley graph; [F8] ensures the s-edge has distinct endpoints. A relator s2 traverses that edge out and back, while a relator (st)m(s,t) with distinct s,t and finite label is the boundary of the corresponding 2m(s,t)-gon in Σ2 by [F1]; inverse relators reverse these loops. Thus every conjugate relator loop contracts in Σ2 (conjugation preserves the identity class by [F6]), and the finite concatenation contracts by the group law [F6]. If S=∅, then W=1 and Σ1 is one vertex, so the only edge loop is constant; the same argument also allows the empty relator product k=0. If no finite rank-two label occurs, there are no polygon relators and the only relator loops are involution backtracks. Finally [step 1.1] reduces every loop in Σ2 at 1 to an edge loop, proving π1(Σ2,1)=1.

3.1step 1.1step 2.1F6

For every vertex v, inclusion j ⁣:Σ2↪Σ induces an isomorphism j∗ ⁣:π1(Σ2,v)→π1(Σ,v). Every class represented by a loop in Σ has an edge-loop representative by [step 1.1], hence lies in the image. If a loop in Σ2 maps to the identity, [step 2.1] makes it null-homotopic in Σ2, so j∗ is injective. Its induced homomorphism is defined by [F6].

3.2step 1.1step 2.2F1F6F7

The graph Σ1 is connected because its vertices are W and S generates W [F1, F7]. Every closed cell is a convex polytope containing its vertex wW∅={w} as a face [F7], and each point of Σ lies in such a cell; a segment in that cell joins the point to a vertex of Σ1. Hence Σ is path-connected. For an arbitrary basepoint x, choose a path p from x to 1 and a loop α at x. The loop pˉ∗α∗p at 1 is homotopic rel basepoint to an edge loop by [step 1.1], then contracts by [step 2.2]. Prepending p and appending pˉ to that based null-homotopy gives a homotopy rel x from (p∗pˉ)∗α∗(p∗pˉ) to p∗pˉ, after reparameterizing concatenations. The loop p∗pˉ contracts rel x by the homotopy G(u,t)=p(2u(1−t)) for u≤12 and G(u,t)=p(2(1−u)(1−t)) for u≥12: the formulas agree at u=12, are continuous, and keep both endpoints at x. Hence (p∗pˉ)∗α∗(p∗pˉ) is null-homotopic and is also homotopic rel x to α by contracting its two outer copies of p∗pˉ. Thus α is null-homotopic, and every fundamental group of Σ is trivial.

4.1step 3.1step 2.2step 3.2F3given∎

The CW complex Σ is nonempty, path-connected and has trivial fundamental groups by [step 3.2], so it is simply connected; [step 3.1] then gives triviality of π1(Σ2,v) and the asserted inclusion isomorphism for every vertex v, while [step 2.2] gives the explicit basepoint case π1(Σ2,1)=1. The cellular approximations use finite relative sources and [F3] is explicitly choice-free in that case; the normal-closure product and all word reductions are finite, and the path p in [step 3.2] is chosen separately for one basepoint. No Axiom of Choice is used.

Remarks

5 · Examples, counterexamples and false statements

None yet.

Sources