LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

How statement and proof provenance work

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

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

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

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

Statement

Let $(S, m)$ , $W$ , $ℓ$ , $S$ , the parabolics $W_{T}$ and the poset $W S$ 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^{'} \in S$ and $w, w^{'} \in W$ .

(1) Equality. $w W_{T} = w^{'} W_{T^{'}}$ if and only if $T = T^{'}$ and $w^{- 1} w^{'} \in W_{T}$ . Hence the projection $π ⁣ : W S \to S$ , $w W_{T} \mapsto T$ , is well-defined, the members of $W S$ are exactly the left cosets of the subgroups $W_{T}$ ( $T \in S$ ), and the left cosets of any one $W_{T}$ are pairwise disjoint while cosets of distinct parabolics are distinct.

(2) Inclusion. $w W_{T} \subseteq w^{'} W_{T^{'}}$ if and only if $T \subseteq T^{'}$ and $w^{- 1} w^{'} \in W_{T^{'}}$ (equivalently $w \in w^{'} W_{T^{'}}$ , equivalently $w W_{T^{'}} = w^{'} W_{T^{'}}$ ). In particular $W_{T} \subseteq W_{T^{'}}$ if and only if $T \subseteq T^{'}$ .

(3) Intersections are parabolic cosets. If $w W_{T} \cap w^{'} W_{T^{'}} \neq \emptyset$ , then $w W_{T} \cap w^{'} W_{T^{'}} = u W_{T \cap T^{'}} for every u \in w W_{T} \cap w^{'} W_{T^{'}};$ moreover $w W_{T} \cap w^{'} W_{T^{'}} \neq \emptyset$ if and only if $w^{- 1} w^{'} \in W_{T} W_{T^{'}}$ , where $W_{T} W_{T^{'}} = {a b : a \in W_{T}, b \in W_{T^{'}}}$ . Thus the meet of two spherical cosets in the inclusion order, when their intersection is nonempty, is that intersection coset, of type $T \cap T^{'}$ ; disjoint spherical cosets have no common lower bound in $W S$ .

(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 \ W S \to S$ is an isomorphism. Consequently the action on $W S$ is free on the minimal elements $w W_{\emptyset}$ .

Facts & Assumptions

Given: A finite Coxeter matrix $(S, m)$ with presented group $W$ and length $ℓ$ ; spherical subsets $T, T^{'} \in S$ ; elements $w, w^{'} \in W$ .

[F1]

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

[F2]

For each $T \subseteq S$ , $W_{T} \cap S = T$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2)).

[F3]

Intersections of standard parabolic subgroups: $W_{I} \cap W_{J} = W_{I \cap J}$ for all $I, J \subseteq 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_{\emptyset} = {1}$ (Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization (1)).

[L1]

Coset membership and equality: for a subgroup $H \leq G$ and $a, b \in G$ , one has $b \in a H$ if and only if $a^{- 1} b \in H$ , and $a H = b H$ if and only if $a^{- 1} b \in H$ ( $x \in a H$ iff $a^{- 1} x \in H$ , and $a H = b H$ iff $a^{- 1} b \in H$ ).

[L2]

A left coset of $H \leq G$ is the set $g H = {g h : h \in H}$ (Left and right cosets $g H$ and $H g$ of a subgroup).

[L3]

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

Proof

technique · direct

1.1givenF2L1L2L3algebra

Suppose $w W_{T} = w^{'} W_{T^{'}}$ . Since $1 \in W_{T}$ and $1 \in W_{T^{'}}$ by [L3], the element $w$ lies in $w W_{T} = w^{'} W_{T^{'}}$ and $w^{'}$ lies in $w^{'} W_{T^{'}} = w W_{T}$ ; by [L1] this gives $w^{- 1} w^{'} \in W_{T^{'}}$ and $w^{' - 1} w \in W_{T}$ . Left-multiplying the coset equality by $w^{- 1}$ and using $(w^{- 1} w) W_{T} = W_{T}$ and $(w^{- 1} w^{'}) W_{T^{'}} = u W_{T^{'}}$ with $u : = w^{- 1} w^{'}$ gives $W_{T} = u W_{T^{'}}$ ; since $u^{- 1} = w^{' - 1} w \in W_{T}$ by [L3], also $W_{T^{'}} = u^{- 1} W_{T} = W_{T}$ . Intersecting with $S$ and applying [F2] yields $T = T^{'}$ , and $w^{- 1} w^{'} = u \in W_{T^{'}} = W_{T}$ .

1.2givenL1algebra

Conversely, if $T = T^{'}$ and $w^{- 1} w^{'} \in W_{T}$ , then $w^{'} \in w W_{T}$ by [L1], so $w^{'} W_{T} = w W_{T}$ by [L1]; together with $T = T^{'}$ this is $w W_{T} = w^{'} W_{T^{'}}$ .

1.3givenF2L1L2L3algebra

Suppose $w W_{T} \subseteq w^{'} W_{T^{'}}$ . Then $w \in w^{'} W_{T^{'}}$ , so $w^{- 1} w^{'} \in W_{T^{'}}$ by [L1]; left-multiplying the inclusion by $w^{- 1}$ gives $W_{T} = w^{- 1} (w W_{T}) \subseteq w^{- 1} (w^{'} W_{T^{'}}) = (w^{- 1} w^{'}) W_{T^{'}} = W_{T^{'}}$ by [L3]. Hence $T = W_{T} \cap S \subseteq W_{T^{'}} \cap S = T^{'}$ by [F2].

1.4givenF1F2L1L2algebra

Conversely, if $T \subseteq T^{'}$ and $w^{- 1} w^{'} \in W_{T^{'}}$ , then $W_{T} \leq W_{T^{'}}$ by [F1], so $w W_{T} \subseteq w W_{T^{'}} = w^{'} W_{T^{'}}$ by [L2]. This also covers the two reformulations: $w \in w^{'} W_{T^{'}}$ is equivalent to $w^{- 1} w^{'} \in W_{T^{'}}$ by [L1], and $w W_{T^{'}} = w^{'} W_{T^{'}}$ is equivalent to $w^{- 1} w^{'} \in W_{T^{'}}$ by [L1] applied with $T = T^{'}$ . Taking $w = w^{'} = 1$ gives $W_{T} \subseteq W_{T^{'}}$ if and only if $T \subseteq T^{'}$ .

1.5givenF3F4L1L2algebra

Assume $u \in w W_{T} \cap w^{'} W_{T^{'}}$ . Then $u W_{T} = w W_{T}$ and $u W_{T^{'}} = w^{'} W_{T^{'}}$ 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 $w W_{T} \cap w^{'} W_{T^{'}} = u W_{T} \cap u W_{T^{'}} = u (W_{T} \cap W_{T^{'}}) = u W_{T \cap T^{'}}$ , the last equality by [F3].

1.6givenF4L2L3algebra

The intersection is nonempty if and only if $w^{- 1} w^{'} \in W_{T} W_{T^{'}}$ : indeed $w W_{T} \cap w^{'} W_{T^{'}} \neq \emptyset$ means that $w a = w^{'} b$ for some $a \in W_{T}$ , $b \in W_{T^{'}}$ , which is equivalent by the group laws [F4] to $w^{- 1} w^{'} = a b^{- 1} \in W_{T} W_{T^{'}}$ because $W_{T^{'}}$ 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 $w W_{T} = w^{'} W_{T} ⟺ w^{- 1} w^{'} \in W_{T}$ is [step 1.1] and [step 1.2] together; and two cosets of $W_{T}$ are disjoint when they are unequal, since if $u$ lies in both then $w W_{T} = u W_{T} = w^{'} W_{T}$ by [L1]. Thus the members of $W S$ are exactly the left cosets of the subgroups $W_{T}$ ( $T \in S$ ).

2.2step 1.5F5givenalgebra

The meet statement of (3): by [step 1.5] the intersection $p = w W_{T} \cap w^{'} W_{T^{'}}$ of two cosets is a member of $W S$ when nonempty, with $π (p) = T \cap T^{'}$ (spherical, since $T \cap T^{'} \subseteq T \in S$ and $S$ is downward closed by [F5]); it is contained in both cosets, so it is a lower bound. If $r = v W_{V} \in W S$ satisfies $r \subseteq w W_{T}$ and $r \subseteq w^{'} W_{T^{'}}$ , then $r \subseteq p$ by definition of intersection. Hence $p$ is the greatest lower bound, and no member of $W S$ is contained in two disjoint cosets because members of $W S$ are nonempty.

2.3step 1.1step 1.3step 1.4F4algebra

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

3.1F2F4F5L2L3step 1.1step 1.3step 2.3given∎

The minimal elements of $W S$ are exactly the singletons $w W_{\emptyset} = {w}$ . If $T \neq \emptyset$ , choose $s \in T$ . By [F2], $s \in W_{T}$ and $W_{\emptyset} \cap S = \emptyset$ ; with [F5] and $1 \in W_{T}$ by [L3], this gives $s \notin W_{\emptyset}$ and $W_{\emptyset} = {1} ⊊ W_{T}$ , hence $w W_{\emptyset} ⊊ w W_{T}$ . Conversely, if $v W_{V} \subseteq w W_{\emptyset}$ , then [step 1.3] gives $V \subseteq \emptyset$ , so $V = \emptyset$ ; the inclusion of singletons is equality, and [step 1.1] gives $v = w$ . The action is free on them because $v \cdot w W_{\emptyset} = w W_{\emptyset}$ forces $v w = 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$ .

Depends on

Used by

Cited to discharge well-definedness by Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization.

Dependency tree · two levels

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

Sources

M. W. Davis, The Geometry and Topology of Coxeter Groups, author manuscript of the first edition (Princeton Univ. Press, 2008) (standard reference, not scraped)
R. Boyd, Homology of Coxeter and Artin groups, PhD thesis, University of Aberdeen, 2018 (with corrections) (standard reference, not scraped)