LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

The positive braid monoid is left and right cancellative

Statement

Let $n \in N$ , let $Σ_{n}$ be the alphabet of Positive braid monoid with the congruence $\equiv^{+}$ and the monoid $B_{n}^{+} = Σ_{n}^{*} / ⁣ \equiv^{+}$ , and let $w \mapsto w^{r e v}$ denote reversal of words. Then:

(a) Reversal descends to an involutive anti-automorphism. If $u \equiv^{+} v$ then $u^{r e v} \equiv^{+} v^{r e v}$ ; consequently $ρ ([w]) : = [w^{r e v}]$ is a well-defined bijection $ρ ⁣ : B_{n}^{+} \to B_{n}^{+}$ satisfying $ρ \circ ρ = i d$ and $ρ (x y) = ρ (y) ρ (x)$ for all $x, y \in B_{n}^{+}$ .

(b) Left cancellation. $x a = x b$ implies $a = b$ , for all $a, b, x \in B_{n}^{+}$ .

(c) Right cancellation. $a x = b x$ implies $a = b$ , for all $a, b, x \in B_{n}^{+}$ .

(d) Dictionary. For positive words $u, v, w$ one has $[u] = [v]$ if and only if $[u^{r e v}] = [v^{r e v}]$ , and $[w] = [u] [v]$ if and only if $[w^{r e v}] = [v^{r e v}] [u^{r e v}]$ . Thus reversal translates left cancellation into right cancellation and exchanges the two sides of every product equation.

For $n \leq 1$ the alphabet is empty, $B_{n}^{+}$ is the one-element monoid, and every statement is trivial. No choice principle is used.

Facts & Assumptions

Given: A natural number $n \geq 2$ , the alphabet $Σ_{n}$ , the congruence $\equiv^{+}$ , the monoid $B_{n}^{+}$ and word reversal $w \mapsto w^{r e v}$ .

[F1]

$\equiv^{+}$ is the smallest congruence on $Σ_{n}^{*}$ containing the braid pairs $σ_{i} σ_{i + 1} σ_{i} \equiv^{+} σ_{i + 1} σ_{i} σ_{i + 1}$ ( $1 \leq i \leq n - 2$ ) and the far-commutation pairs $σ_{i} σ_{j} \equiv^{+} σ_{j} σ_{i}$ ( $∣ i - j ∣ \geq 2$ ); $B_{n}^{+} = Σ_{n}^{*} / ⁣ \equiv^{+}$ with $[u] [v] = [u v]$ , and $[u] = [v]$ holds if and only if $u \equiv^{+} v$ (Positive braid monoid, Words in an alphabet with formal inverses, elementary cancellation, and reduced words).

[F2]

$u \equiv^{+} v$ implies $∣ u ∣ = ∣ v ∣$ , and $ℓ ([w]) : = ∣ w ∣$ is a well-defined monoid homomorphism $B_{n}^{+} \to N$ (Positive artin relations preserve homogeneous length).

[L3]

Left cancellation, in the form proved by reversing. For all $x, u, v \in B_{n}^{+}$ , $x u = x v$ implies $u = v$ (Artin positive word reversing is complete, part (d)).

[L4]

Induction on the natural numbers, and the elementary theory of the free monoid $Σ_{n}^{*}$ of Words in an alphabet with formal inverses, elementary cancellation, and reduced words: reversal of words is the local recursive definition $(ε)^{r e v} = ε$ , $(w s)^{r e v} = s w^{r e v}$ for a letter $s$ , whose well-definedness is an instance of induction (The principle of mathematical induction); it satisfies $(u v)^{r e v} = v^{r e v} u^{r e v}$ , $(w^{r e v})^{r e v} = w$ and $∣ w^{r e v} ∣ = ∣ w ∣$ by induction on the length of $w$ .

Proof

technique · direct

1.1

Reversal is an involution of free words. By [L4], $w \mapsto w^{r e v}$ is a well-defined involution of $Σ_{n}^{*}$ with $(u v)^{r e v} = v^{r e v} u^{r e v}$ and $∣ w^{r e v} ∣ = ∣ w ∣$ ; in particular $ε^{r e v} = ε$ and reversal is a bijection of the free monoid fixing no letter-type but permuting letters by identity.

1.2

Reversal preserves the defining pairs, hence the congruence. The set $R_{n}$ of defining pairs of [F1] is stable under reversal: for indices with $∣ i - j ∣ \geq 2$ , $(σ_{i} σ_{j})^{r e v} = σ_{j} σ_{i}$ and $(σ_{j} σ_{i})^{r e v} = σ_{i} σ_{j}$ , so the pair is preserved; for the braid pair, $(σ_{i} σ_{i + 1} σ_{i})^{r e v} = σ_{i} σ_{i + 1} σ_{i}$ and $(σ_{i + 1} σ_{i} σ_{i + 1})^{r e v} = σ_{i + 1} σ_{i} σ_{i + 1}$ , so each side is fixed and the pair is preserved. Now suppose $u \equiv^{+} v$ : by [F1] there is a finite chain $u = w_{0}, w_{1}, \dots, w_{m} = v$ in which each step replaces a subword by the other side of a pair in $R_{n}$ ; by induction on $m$ (The principle of mathematical induction), if $w_{k + 1}$ is obtained from $w_{k}$ by replacing $a$ with $b$ inside the decomposition $w_{k} = x a y$ , $w_{k + 1} = x b y$ where ${a, b} \in R_{n}$ , then $w_{k + 1}^{r e v} = y^{r e v} b^{r e v} x^{r e v}$ is obtained from $w_{k}^{r e v} = y^{r e v} a^{r e v} x^{r e v}$ by replacing $a^{r e v}$ with $b^{r e v}$ , and ${a^{r e v}, b^{r e v}} = {a, b} \in R_{n}$ by the stability just proved; so $w_{k}^{r e v} \equiv^{+} w_{k + 1}^{r e v}$ and transitivity gives $u^{r e v} \equiv^{+} v^{r e v}$ .

F1L4

1.3

Left cancellation (b). This is [L3], stated there for arbitrary $x$ ; the case $x = 1$ is trivial, and for $n \leq 1$ both sides lie in the one-element monoid. Since $ℓ$ takes natural values [F2], the case $x = 1$ is also covered: $ℓ (x) = 0$ means $x = [ε] = 1$ , and then $x a = x b$ reads $a = b$ .

F2L3

2.1

The induced map is an involutive anti-automorphism. By 1.2 the assignment $ρ ([w]) : = [w^{r e v}]$ is well defined on $\equiv^{+}$ -classes; it is a bijection because $w \mapsto w^{r e v}$ is an involution of $Σ_{n}^{*}$ (1.1) and $u \equiv^{+} v$ implies $u^{r e v} \equiv^{+} v^{r e v}$ in both directions, so $ρ \circ ρ = i d$ . For classes $x = [u]$ , $y = [v]$ we get $ρ (x y) = ρ ([u v]) = [(u v)^{r e v}] = [v^{r e v} u^{r e v}] = [v^{r e v}] [u^{r e v}] = ρ (y) ρ (x)$ , using 1.1 and the multiplicativity of the quotient monoid [F1].

F1L4step 1.1step 1.2

3.1

Right cancellation (c). Assume $a x = b x$ in $B_{n}^{+}$ . Applying the anti-automorphism $ρ$ of step 2.1 gives $ρ (a x) = ρ (x) ρ (a)$ and $ρ (b x) = ρ (x) ρ (b)$ , hence $ρ (x) ρ (a) = ρ (x) ρ (b)$ ; left cancellation (step 1.3, with $x$ replaced by $ρ (x)$ ) gives $ρ (a) = ρ (b)$ , and applying $ρ$ again gives $a = ρ (ρ (a)) = ρ (ρ (b)) = b$ by step 2.1.

step 1.3step 2.1

3.2

The dictionary (d). For positive words: $[u] = [v]$ implies $[u^{r e v}] = [v^{r e v}]$ by step 1.2, and the converse follows by applying step 1.2 to $u^{r e v}, v^{r e v}$ together with the involution of step 1.1. For products, $ρ ([w]) = [w^{r e v}]$ and, by step 2.1, $ρ ([u] [v]) = [v^{r e v}] [u^{r e v}]$ ; since $ρ$ is injective, $[w] = [u] [v]$ holds if and only if $[w^{r e v}] = [v^{r e v}] [u^{r e v}]$ . Lengths agree, $∣ w^{r e v} ∣ = ∣ w ∣$ (step 1.1), as [F2] requires.

F2step 1.1step 1.2step 2.1

4.1

Assembly. Part (a) is steps 1.2 and 2.1, part (b) is step 1.3, part (c) is step 3.1 and part (d) is step 3.2; the case $n \leq 1$ was noted in the statement and each step above also holds there. Every step is a finite computation or an induction over $N$ ; no choice principle occurs. ∎

step 1.2step 1.3step 2.1step 3.1step 3.2

Remarks

The conventions are those of Positive braid monoid: $\equiv^{+}$ is generated by the two families of Artin relations, and $[u v] = [u] [v]$ , so that $B_{n}^{+}$ is the monoid presented by the positive relations. Reversal is an anti-automorphism, not an automorphism: $ρ (x y) = ρ (y) ρ (x)$ .
Left cancellation is proved in Artin positive word reversing is complete by the source's criterion for right-reversing (Corollary 4.45); the present item records it in the class-level form used by the divisibility items that follow and adds the reversal dictionary, which is what turns left-divisibility into right-divisibility throughout this page.
Sources: GM Section 4, printed pp. 26--27 (cancellativity step), where cancellation is used to obtain lattice properties; Dehornoy et al., Chapter II, Proposition 4.44 and Corollary 4.45, printed p. 78, for the reversing proof reused here.
No axiom of choice, no transfinite induction and no infinite construction is used: reversal is an operation on finite words and every induction is over $N$ .

Depends on

Used by

Dependency tree · two levels

13 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

J. Gonzalez-Meneses, Basic results on braid groups, Section 4, printed pp. 26-27 (cancellativity step) (standard reference, not scraped)
Patrick Dehornoy et al., Foundations of Garside Theory, Chapter II, Proposition 4.44 and Corollary 4.45, printed p. 78 (standard reference, not scraped)