TheoremStatement: 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.

Unique minimal double coset representatives and the additive normal form u-d-v

Statement

Let $I, J \subseteq S$ , let $d \in^{I} W^{J}$ , and put

$K : = I \cap d J d^{- 1} = {s \in I : d^{- 1} s d \in J},$

so that $W_{I} \cap d W_{J} d^{- 1} = W_{K}$ by The parabolic intersection W_I cap dW_Jd inverse for d in ^IW^J. Write

$W_{I}^{K} : = {u \in W_{I} : ℓ (u s) > ℓ (u) for all s \in K}$

for the set of elements of $W_{I}$ with no right descent in $K$ --- the same construction as in Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (2), applied inside the Coxeter system $(W_{I}, I)$ with its standard parabolic subgroup $W_{K}$ .

(1) Unique minimum. Two elements of $^{I} W^{J}$ lie in a common double coset $W_{I} w W_{J}$ only if they are equal. Hence, by Descent reduction, minimum-length elements, and the additive factorization in a double coset (1),(2), every double coset $W_{I} w W_{J}$ contains exactly one element of $^{I} W^{J}$ , namely its unique element of minimum length; in particular $d$ is uniquely determined by the double coset $W_{I} d W_{J}$ .

(2) The additive normal form. Every $x \in W_{I} d W_{J}$ has a unique representation

$x = u d v with u \in W_{I}^{K}, v \in W_{J},$

and every product $u d v$ with $u \in W_{I}^{K}$ , $v \in W_{J}$ lies in $W_{I} d W_{J}$ . Thus

$W_{I}^{K} \times W_{J} \to W_{I} d W_{J}, (u, v) \mapsto u d v$

is a bijection, and for all $u \in W_{I}^{K}$ and $v \in W_{J}$

$ℓ (u d v) = ℓ (u) + ℓ (d) + ℓ (v) .$

(3) The size of a double coset. $∣ W_{I} d W_{J} ∣ = ∣ W_{I}^{K} ∣ \cdot ∣ W_{J} ∣$ ; and if $W_{I}$ is finite then $∣ W_{I} d W_{J} ∣ = (∣ W_{I} ∣ / ∣ W_{K} ∣) \cdot ∣ W_{J} ∣$ , with the quotient a finite integer and the product interpreted as cardinal multiplication.

(4) The restriction to $W_{I}^{K}$ is necessary. For arbitrary $u \in W_{I}$ the representation $x = u d v$ is not unique in general: if $u = u_{0} z$ is the factorization of $u$ with $u_{0} \in W_{I}^{K}$ and $z \in W_{K}$ , and $z^{'} : = d^{- 1} z d \in W_{J}$ , then

$u d v = u_{0} d (z^{'} v), u_{0} \in W_{I}^{K}, z^{'} v \in W_{J},$

and $z^{'} \neq 1$ whenever $z \neq 1$ ; so the same $x$ has two representations of the form $u d v$ with different first factors unless $u \in W_{I}^{K}$ already. This is why the transversal restriction in (2) is recorded explicitly and may not be dropped.

Facts & Assumptions

Given: a finite Coxeter matrix $(S, m)$ with presented group $W$ and length $ℓ$ , subsets $I, J \subseteq S$ , an element $d \in^{I} W^{J}$ , the subset $K = {s \in I : d^{- 1} s d \in J}$ and the transversal $W_{I}^{K}$ of the statement.

[F1]

Inside the Coxeter system $(W_{I}, I)$ with standard parabolic subgroup $W_{K}$ : $W_{I}^{K} = {u \in W_{I} : ℓ (u s) > ℓ (u) for all s \in K}$ is the set of minimal-length representatives of the left cosets $u W_{K}$ in $W_{I}$ ; every $u \in W_{I}$ has a unique factorization $u = u_{0} z$ with $u_{0} \in W_{I}^{K}$ , $z \in W_{K}$ , and then $ℓ (u) = ℓ (u_{0}) + ℓ (z)$ , while $ℓ (u_{0} z^{'}) = ℓ (u_{0}) + ℓ (z^{'})$ for all $z^{'} \in W_{K}$ ; more generally $W_{J} = {w : S (w) \subseteq J}$ for $J \subseteq S$ , every left coset $a W_{J}$ has a unique minimal element, and $ℓ (d u) = ℓ (d) + ℓ (u)$ for a minimal representative $d \in W^{J}$ of $a W_{J}$ and $u \in W_{J}$ , with the mirrored statement for right cosets: for the minimal representative $d$ of a right coset $W_{J} a$ one has $ℓ (u d) = ℓ (u) + ℓ (d)$ for all $u \in W_{J}$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification).

[F2]

The element $x = d^{- 1} z d$ of the statement lies in $W_{J}$ : indeed $W_{I} \cap d W_{J} d^{- 1} = W_{K}$ and $d^{- 1} W_{K} d = W_{d^{- 1} K d} \subseteq W_{J}$ (The parabolic intersection W_I cap dW_Jd inverse for d in ^IW^J).

[F3]

Every double coset $W_{I} w W_{J}$ contains an element of $^{I} W^{J}$ ; for $d \in^{I} W^{J}$ one has $ℓ (d) \leq ℓ (x)$ for all $x \in W_{I} d W_{J}$ with equality if and only if $x = d$ ; and every $x \in W_{I} d W_{J}$ has the form $x = a d c$ with $a \in W_{I}$ , $c \in W_{J}$ and $ℓ (x) = ℓ (a) + ℓ (d) + ℓ (c)$ (Descent reduction, minimum-length elements, and the additive factorization in a double coset).

[F4]

For $w = s_{1} \dots s_{k}$ one has $ℓ (w) \leq k$ , so $ℓ (u v) \leq ℓ (u) + ℓ (v)$ for all $u, v \in W$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F5]

Multiplication in $W$ is associative and equalities in $W$ may be multiplied and cancelled; in particular conjugation $w \mapsto c w c^{- 1}$ is injective (Group and abelian group).

Proof

technique · direct; existence by factoring inside $W_I$ and $W_J$, uniqueness by the intercoset intersection $W_K$, then the cardinality and necessity clauses

1.1F1F2F3F5

Existence of the normal form. Let $x \in W_{I} d W_{J}$ . By [F3] write $x = a d c$ with $a \in W_{I}$ , $c \in W_{J}$ and $ℓ (x) = ℓ (a) + ℓ (d) + ℓ (c)$ ; by [F1] factor $a = u_{0} z$ with $u_{0} \in W_{I}^{K}$ , $z \in W_{K}$ and $ℓ (a) = ℓ (u_{0}) + ℓ (z)$ . Put $z^{'} : = d^{- 1} z d \in W_{J}$ by [F2], which satisfies $z d = d z^{'}$ because $z = d z^{'} d^{- 1}$ , and put $v : = z^{'} c \in W_{J}$ . Then $x = u_{0} z d c = u_{0} d z^{'} c = u_{0} d v$ with $u_{0} \in W_{I}^{K}$ , $v \in W_{J}$ , so every element of the double coset has a representation of the required form.

1.2F1F2F5

Uniqueness of the first factor I: the intersection. Suppose $u d v = u^{'} d v^{'}$ with $u, u^{'} \in W_{I}^{K}$ and $v, v^{'} \in W_{J}$ . Left-multiplying by $u^{- 1}$ and right-multiplying by $(v^{'})^{- 1} d^{- 1}$ and cancelling gives $u^{- 1} u^{'} = d v (v^{'})^{- 1} d^{- 1} \in W_{I} \cap d W_{J} d^{- 1}$ , which equals $W_{K}$ by [F2]; hence $u^{'} = u z$ for some $z \in W_{K}$ . Since $u, u^{'} \in W_{I}^{K}$ and $W_{I}^{K}$ consists of the minimal representatives of the left cosets $u W_{K}$ in $W_{I}$ by [F1], $u = u^{'}$ ; substituting back gives $d v = d v^{'}$ and hence $v = v^{'}$ by cancellation, so the representation has at most one pair of factors and the map of (2) is injective.

2.1F1F3F4step 1.1step 1.2

Additivity along the representation. Let $x \in W_{I} d W_{J}$ and write $x = a d c$ with $a \in W_{I}$ , $c \in W_{J}$ as in [F3], and factor $a = u_{0} z$ , $z^{'} = d^{- 1} z d$ , $v = z^{'} c$ as in step 1.1. First $ℓ (z) = ℓ (z^{'})$ : indeed $z d = d z^{'}$ , while $ℓ (z d) = ℓ (z) + ℓ (d)$ because $z \in W_{K} \subseteq W_{I}$ and $d \in^{I} W$ , and $ℓ (d z^{'}) = ℓ (d) + ℓ (z^{'})$ because $d \in W^{J}$ and $z^{'} \in W_{J}$ , both by [F1]. Estimating with subadditivity [F4], $ℓ (x) \leq ℓ (u_{0}) + ℓ (d) + ℓ (v) \leq ℓ (u_{0}) + ℓ (d) + ℓ (z^{'}) + ℓ (c) = ℓ (u_{0}) + ℓ (z) + ℓ (d) + ℓ (c) = ℓ (a) + ℓ (d) + ℓ (c) = ℓ (x)$ , where the last equality is [F3]; hence every inequality is an equality, so $ℓ (u_{0} d v) = ℓ (u_{0}) + ℓ (d) + ℓ (v)$ for the representation of step 1.1, and also $ℓ (v) = ℓ (z^{'}) + ℓ (c)$ . For any prescribed $u \in W_{I}^{K}$ , $v \in W_{J}$ , apply this construction to $x = u d v$ ; uniqueness in step 1.2 identifies the constructed pair with $(u, v)$ , proving additivity for every such pair.

2.2F1step 1.1step 1.2

The size formulas. The map $W_{I}^{K} \times W_{J} \to W_{I} d W_{J}$ , $(u, v) \mapsto u d v$ , is surjective by step 1.1 and injective by step 1.2, hence a bijection, so $∣ W_{I} d W_{J} ∣ = ∣ W_{I}^{K} ∣ \cdot ∣ W_{J} ∣$ . If $W_{I}$ is finite, the factorization $u = u_{0} z$ of [F1] is a bijection $W_{I}^{K} \times W_{K} \to W_{I}$ , so $∣ W_{I}^{K} ∣ = ∣ W_{I} ∣ / ∣ W_{K} ∣$ and therefore $∣ W_{I} d W_{J} ∣ = (∣ W_{I} ∣ / ∣ W_{K} ∣) \cdot ∣ W_{J} ∣$ , also when $W_{J}$ is infinite.

3.1F3step 1.1step 2.1

Uniqueness of the minimum. Suppose $d, d^{'} \in^{I} W^{J}$ lie in a common double coset $Ω : = W_{I} d W_{J} = W_{I} d^{'} W_{J}$ . By [F3] each of $d, d^{'}$ is a minimum-length element of $Ω$ , so $ℓ (d) = ℓ (d^{'})$ ; applying the representation of steps 1.1 and 2.1 with $x : = d^{'}$ and base point $d$ gives $d^{'} = u d v$ with $u \in W_{I}^{K}$ , $v \in W_{J}$ and $ℓ (d^{'}) = ℓ (u) + ℓ (d) + ℓ (v)$ . Hence $ℓ (u) + ℓ (v) = 0$ , so $u = v = 1$ and $d^{'} = d$ . Consequently each double coset contains at most one element of $^{I} W^{J}$ ; by [F3] (or its part (1)) it contains at least one, namely its unique minimum.

4.1F1F2F5step 1.1step 1.2step 2.1∎

The normal form and the necessity of the restriction. By steps 1.1, 1.2 and 2.1 every $x \in W_{I} d W_{J}$ has a unique representation $x = u d v$ with $u \in W_{I}^{K}$ , $v \in W_{J}$ , and then $ℓ (x) = ℓ (u) + ℓ (d) + ℓ (v)$ ; conversely every product $u d v$ with $u \in W_{I}^{K} \subseteq W_{I}$ and $v \in W_{J}$ lies in $W_{I} d W_{J}$ by the definition of the double coset, so the displayed map is a bijection and (2) holds. For (4) let $u \in W_{I}$ and $v \in W_{J}$ be arbitrary and factor $u = u_{0} z$ with $u_{0} \in W_{I}^{K}$ , $z \in W_{K}$ by [F1]; put $z^{'} : = d^{- 1} z d \in W_{J}$ by [F2]. Then $u d v = u_{0} z d v = u_{0} d z^{'} v = u_{0} d (z^{'} v)$ with $u_{0} \in W_{I}^{K}$ and $z^{'} v \in W_{J}$ , so $x = u d v$ has two representations with first factors $u$ and $u_{0}$ ; and $z^{'} \neq 1$ whenever $z \neq 1$ , because $z = d z^{'} d^{- 1}$ and conjugation by $d$ is injective by [F5], so $u \neq u_{0}$ whenever $z \neq 1$ , that is, whenever $u \notin W_{I}^{K}$ . This is (4) and completes the proof of (1)-(4); no Axiom of Choice is used.

Remarks

The theorem is the algebraic heart of the double coset calculus: (1) and (3) say that the double cosets $W_{I} w W_{J}$ are parameterized by $^{I} W^{J}$ , and (2) upgrades the transversal to a normal form with exact length additivity. The counterexample in (4) is the classical failure of uniqueness once the transversal condition on the first factor is dropped.
The finite formula of (3) is the parabolic analogue of $∣ W_{I} w W_{J} ∣ = ∣ W_{I} ∣ ∣ W_{J} ∣ / ∣ W_{I} \cap w W_{J} w^{- 1} ∣$ ; the intersection is written $W_{K}$ by The parabolic intersection W_I cap dW_Jd inverse for d in ^IW^J.

Depends on

Used by

Cited to discharge well-definedness by Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups.

Dependency tree · two levels

42 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

George Lusztig, Hecke Algebras with Unequal Parameters (revised arXiv edition of the CRM monograph, arXiv:math/0208154v2) (standard reference, not scraped)
Sara Billey, Matjaz Konvalinka, T. Kyle Petersen, William Slofstra and Bridget Tenner, Parabolic double cosets in Coxeter groups (arXiv:1612.00736v2) (standard reference, not scraped)
Michael W. Davis, The Geometry and Topology of Coxeter Groups (first-edition author manuscript, 2007-2008) (standard reference, not scraped)
Anders Bjorner and Francesco Brenti, Combinatorics of Coxeter Groups (Graduate Texts in Mathematics 231, Springer 2005; author-hosted complete PDF) (standard reference, not scraped)