ExampleConstruction: Literature-sourcedVerification: 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.

Type-A Artin projections, positive lifts, and the positive braid monoid

Example

Let $n \geq 2$ , $S = {s_{1}, \dots, s_{n - 1}}$ and let $m$ be the type- $A_{n - 1}$ Coxeter matrix on $S$ : $m (s_{i}, s_{i}) = 1$ , $m (s_{i}, s_{j}) = 3$ when $∣ i - j ∣ = 1$ , and $m (s_{i}, s_{j}) = 2$ when $∣ i - j ∣ > 1$ . Let $W$ be the presented Coxeter group with length $ℓ$ , let $G_{n} : = A (S, m)$ and $G_{n}^{+} : = A^{+} (S, m)$ be the Artin group and monoid of Artin monoid and Artin group presentations, and the canonical monoid-to-group map, and let $π : G_{n} \to W$ , $π^{+} : G_{n}^{+} \to W$ , $γ$ , $σ_{i} : = σ_{s_{i}}$ and $b_{w}$ be as in Universal properties of the Artin monoid and group, the projection onto the Coxeter group, and the quotient by the squares and The reduced positive section b_w, its length additivity, and the degree homomorphism. By the type- $A$ clause of Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4), $s_{i} \mapsto (i i + 1)$ extends to an isomorphism $W \to S_{n}$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation) with $ℓ (w) = inv (w)$ , the inversion number (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations).

Throughout, relabel the library's underlying set ${0, \dots, n - 1}$ as ${1, \dots, n}$ by $k \mapsto k + 1$ , as in that supplier. Cycle symbols, one-line lists and inversion positions below use these transported labels; the order-preserving relabelling leaves inversion numbers unchanged.

The Artin-to-symmetric map. Composing with that isomorphism, $s_{i} \mapsto (i i + 1)$ extends to a surjective homomorphism

$π_{n} : G_{n} ⟶ S_{n}, π_{n} (σ_{i}) = (i i + 1),$

with $π_{n} (σ_{i_{1}} \dots σ_{i_{k}}) = s_{i_{1}} \dots s_{i_{k}}$ for every word; the same assignment on the generators gives a monoid homomorphism $π_{n}^{+} : G_{n}^{+} \to S_{n}$ with $π_{n} \circ γ = π_{n}^{+}$ . Surjectivity holds because the adjacent transpositions generate $S_{n}$ (the existence follows from the universal property (2) of Universal properties of the Artin monoid and group, the projection onto the Coxeter group, and the quotient by the squares, since the braid words of the type- $A$ matrix are equal in $S_{n}$ ).

Positive lifts. For $w \in S_{n}$ the element $b_{w} = σ_{i_{1}} \dots σ_{i_{k}}$ of any reduced expression is well defined, satisfies $π_{n}^{+} (b_{w}) = w$ , and the map $w \mapsto b_{w}$ is injective (The reduced positive section b_w, its length additivity, and the degree homomorphism (1),(2)). For instance, when $n \geq 3$ ,

$b_{s_{1} s_{2}} = σ_{1} σ_{2}, b_{s_{1}} b_{s_{2}} = σ_{1} σ_{2} = b_{s_{1} s_{2}}$

because $inv (s_{1} s_{2}) = 2 = 1 + 1$ , an instance of the length-additive case of The reduced positive section b_w, its length additivity, and the degree homomorphism (4).

Two reduced expressions of the longest element. For $n = 3$ , $w_{0} = (1 3) = s_{1} s_{2} s_{1} = s_{2} s_{1} s_{2}$ has $ℓ (w_{0}) = 3 = inv (w_{0})$ , and the two reduced expressions are related by the braid move $σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2}$ in $G_{3}$ , so

$b_{w_{0}} = σ_{1} σ_{2} σ_{1} = σ_{2} σ_{1} σ_{2},$

a nonempty instance of the independence clause (1) of The reduced positive section b_w, its length additivity, and the degree homomorphism.

Positive braid monoid. For the same standard type- $A_{n - 1}$ indexing, the generators and positive braid relations of $G_{n}^{+}$ agree exactly with the presentation of $B_{n}^{+}$ in Positive braid monoid. Thus the assignment $σ_{i} \mapsto {\overline{σ}}_{i}$ gives a monoid isomorphism $G_{n}^{+} ≅ B_{n}^{+}$ by the quotient universal properties. This is only an identification by positive presentations; it does not assert that $B_{n}^{+}$ embeds in $G_{n}$ or construct a geometric braid monoid.
Scope. This example proves only the stated presentation-level maps, lifts and finite calculations. It constructs no topological model, proves no Garside or lattice property, and makes no claim about the embedding of the positive monoid into the group. The type-A group identification with geometric braids is the separate conditional application in A2, using its independently published completeness theorem. The failure of $b$ to be multiplicative is the companion counterexample.

Facts & Assumptions

Given: An integer $n \geq 2$ , the type- $A_{n - 1}$ Coxeter matrix on $S = {s_{1}, \dots, s_{n - 1}}$ , the group $W$ with length $ℓ$ , and the constructions $G_{n} = A (S, m)$ , $G_{n}^{+} = A^{+} (S, m)$ , $γ$ , $σ_{i}$ and $b_{w}$ of the items named in the statement, together with the isomorphism $W \to S_{n}$ , $s_{i} \mapsto (i i + 1)$ , of the type- $A$ clause (4) of Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification.

[F1]

A map $f : S \to M$ into a monoid whose values on the two words of every braid pair agree extends uniquely to a monoid homomorphism $\overset{ˉ}{f} : A^{+} \to M$ with $\overset{ˉ}{f} (σ_{s}) = f (s)$ . (Universal properties of the Artin monoid and group, the projection onto the Coxeter group, and the quotient by the squares)

[F2]

A map $f : S \to G$ into a group whose values on the two words of every braid pair agree extends uniquely to a group homomorphism $\overset{ˉ}{f} : A \to G$ with $\overset{ˉ}{f} (σ_{s}) = f (s)$ . (Universal properties of the Artin monoid and group, the projection onto the Coxeter group, and the quotient by the squares)

[F3]

$b_{w}$ is well defined independently of the reduced expression, $b_{1} = [ε]$ , and $π^{+} (b_{w}) = w$ . (The reduced positive section b_w, its length additivity, and the degree homomorphism)

[F4]

$π^{+} \circ b = {i d}_{W}$ and $π \circ γ \circ b = {i d}_{W}$ , hence $b$ is injective and is a set-theoretic section. (The reduced positive section b_w, its length additivity, and the degree homomorphism)

[F5]

$b_{u} b_{v} = b_{u v}$ if and only if $ℓ (u v) = ℓ (u) + ℓ (v)$ . (The reduced positive section b_w, its length additivity, and the degree homomorphism)

[F6]

For $n \geq 2$ the symmetric group has the presentation with generators $s_{i} = (i i + 1)$ and relations $s_{i}^{2} = 1$ , $s_{i} s_{i + 1} s_{i} = s_{i + 1} s_{i} s_{i + 1}$ and $s_{i} s_{j} = s_{j} s_{i}$ for $∣ i - j ∣ > 1$ . (The symmetric group has the Coxeter presentation)

[F7]

For $n \geq 2$ the adjacent transpositions $s_{j} = (j j + 1)$ generate $S_{n}$ . Generation follows directly from the zero-indexed adjacent-swap proof of Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4). The repaired Adjacent transpositions generate the finite symmetric group $S_{n}$ also proves generation in exactly the transported one-based model fixed above; the direct argument here remains valid.

[F8]

In the transported one-based model fixed above, an inversion of $σ \in S_{n}$ is a pair $(i, j)$ with $1 \leq i < j \leq n$ and $σ (i) > σ (j)$ , and $inv (σ)$ is the number of inversions. (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations)

[F9]

Let $M$ be a monoid and $a_{1}, \dots, a_{n - 1} \in M$ satisfy $a_{i} a_{i + 1} a_{i} = a_{i + 1} a_{i} a_{i + 1}$ and $a_{i} a_{j} = a_{j} a_{i}$ for $∣ i - j ∣ > 1$ ; then there is exactly one monoid homomorphism $φ : B_{n}^{+} \to M$ with $φ ({\overline{σ}}_{i}) = a_{i}$ . (Positive braid monoid)

[F10]

The subgroup generated by a set is contained in every subgroup containing that set. (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups)

Verification

1.1F2F6F7F10

The braid pairs of the type- $A_{n - 1}$ matrix are the pairs of alternating words ${s_{i} s_{i + 1} s_{i}, s_{i + 1} s_{i} s_{i + 1}}$ for $∣ i - j ∣ = 1$ and the commuting pairs ${s_{i} s_{j}, s_{j} s_{i}}$ for $∣ i - j ∣ > 1$ ; their images under $f (s_{i}) : = (i i + 1)$ are equal in $S_{n}$ by the presentation of [F6]. Hence [F2] gives a homomorphism $π_{n} : G_{n} \to S_{n}$ with $π_{n} (σ_{i}) = (i i + 1)$ . Its image is a subgroup of $S_{n}$ containing the adjacent transpositions, which generate $S_{n}$ by [F7], so the image is all of $S_{n}$ by [F10]: $π_{n}$ is surjective.

1.2F1F9

The monoid isomorphism $G_{n}^{+} ≅ B_{n}^{+}$ : define $φ : G_{n}^{+} \to B_{n}^{+}$ on generators by $φ (σ_{i}) : = {\overline{σ}}_{i}$ . The braid pairs of the type- $A$ matrix map to the two defining word pairs of $B_{n}^{+}$ of [F9], whose two members are $\equiv^{+}$ -equivalent in $B_{n}^{+}$ , so [F1] gives a monoid homomorphism $φ$ . Conversely the elements $a_{i} : = σ_{i} \in G_{n}^{+}$ satisfy $a_{i} a_{i + 1} a_{i} = a_{i + 1} a_{i} a_{i + 1}$ and $a_{i} a_{j} = a_{j} a_{i}$ for $∣ i - j ∣ > 1$ , because the corresponding alternating words are $\equiv^{+}$ -equivalent in $A^{+} (S, m)$ and hence equal in $G_{n}^{+}$ ; so [F9] gives a monoid homomorphism $ψ : B_{n}^{+} \to G_{n}^{+}$ with $ψ ({\overline{σ}}_{i}) = σ_{i}$ . The composites $φ \circ ψ$ and $ψ \circ φ$ fix every generator, hence are the respective identities by the uniqueness clauses of [F1] and [F9]; thus $φ$ and $ψ$ are mutually inverse isomorphisms.

2.1F1step 1.1

The same assignment $f (s_{i}) : = (i i + 1)$ has equal values on the two words of every braid pair by [F6], so [F1] with $M = S_{n}$ gives a monoid homomorphism $π_{n}^{+} : G_{n}^{+} \to S_{n}$ with $π_{n}^{+} (σ_{i}) = (i i + 1)$ . The composites $π_{n} \circ γ$ and $π_{n}^{+}$ are monoid homomorphisms $G_{n}^{+} \to S_{n}$ agreeing on every generator $σ_{i}$ , so they are equal by the uniqueness clause of [F1]: $π_{n} \circ γ = π_{n}^{+}$ .

3.1F3F4step 2.1

The map $b : S_{n} \to G_{n}^{+}$ is well defined by the type- $A$ isomorphism of the given data: its input $w \in S_{n}$ corresponds to the unique element of $W$ with the same name, and [F3] applies. It satisfies $π_{n}^{+} (b_{w}) = w$ by [F3], and $π_{n} \circ γ \circ b = {i d}_{S_{n}}$ because $π_{n} \circ γ = π_{n}^{+}$ by step 2.1 and $π_{n}^{+} \circ b = i d$ by [F4]; in particular $b$ is injective by [F4] and is a set-theoretic section of both $π_{n}^{+}$ and $π_{n} \circ γ$ .

4.1F5F8step 3.1

For $n \geq 3$ , the element $s_{1} s_{2}$ permutes the first three symbols as in $S_{3}$ and fixes the others; it corresponds to $(1 2) (2 3) = (1 2 3)$ , whose one-line form is $[2, 3, 1, 4, \dots, n]$ (with no tail when $n = 3$ ); the pairs $(1, 3)$ and $(2, 3)$ are its only inversions: $(1, 2)$ is not an inversion and all pairs involving the increasing tail contribute none, so $inv (s_{1} s_{2}) = 2$ by [F8]. By the given type- $A$ clause $ℓ (s_{1} s_{2}) = 2$ while $ℓ (s_{1}) = ℓ (s_{2}) = 1$ , so $ℓ (s_{1} s_{2}) = ℓ (s_{1}) + ℓ (s_{2})$ and [F5] gives $b_{s_{1}} b_{s_{2}} = b_{s_{1} s_{2}}$ ; explicitly both sides equal $σ_{1} σ_{2}$ , and no braid move is needed for this pair.

4.2F8step 3.1

For $n = 3$ , the two words $s_{1} s_{2} s_{1}$ and $s_{2} s_{1} s_{2}$ both act as the transposition $(1 3)$ , whose one-line form $[3, 2, 1]$ has all three pairs as inversions, so $inv (w_{0}) = 3$ by [F8]; with $ℓ (w_{0}) = 3$ by the given type- $A$ clause, both words have length $ℓ (w_{0})$ and hence are reduced expressions of $w_{0}$ . Step 3.1 therefore gives $b_{w_{0}}$ as the product along either word, and the two products are equal in $G_{3}$ because $σ_{1} σ_{2} σ_{1}$ and $σ_{2} σ_{1} σ_{2}$ are the two words of a braid pair of $A (S, m)$ , hence equal in $G_{3}^{+}$ and in $G_{3}$ .

5.1given∎

Scope and choice: only presentation-level maps, the positive monoid isomorphism and the displayed finite computations are proved; no topological model, no Garside or lattice property, and no embedding of $G_{n}^{+}$ into $G_{n}$ or $B_{n}^{+}$ into $B_{n}$ is asserted. All constructions are given on generators of explicitly presented monoids and groups, and no choice is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

58 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

Rachael Boyd, Homology of Coxeter and Artin groups (PhD thesis, University of Aberdeen 2018, corrected version) (standard reference, not scraped)
Michael W. Davis, The Geometry and Topology of Coxeter Groups (Princeton University Press 2008; author's complete PDF) (standard reference, not scraped)