LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 unreduced Burau matrices satisfy the Artin relations

Statement

The matrices $B_{1}, \dots, B_{n - 1} \in {GL}_{n} (Λ_{1})$ of The unreduced Burau matrices satisfy $B_{i} B_{i + 1} B_{i} = B_{i + 1} B_{i} B_{i + 1}$ for $1 \leq i \leq n - 2$ and $B_{i} B_{j} = B_{j} B_{i}$ for $∣ i - j ∣ \geq 2$ . Consequently, by von Dyck, the assignment $σ_{i} \mapsto B_{i}$ extends uniquely to a group homomorphism $ρ_{n}^{m a t} : B_{n} ⟶ {GL}_{n} (Λ_{1})$ from the presented braid group of The braid group by Artin presentation. No choice principle is used.

Facts & Assumptions

Given: $n \geq 1$ , the ring $Λ_{1} = Z [t^{\pm 1}]$ , and the matrices $B_{1}, \dots, B_{n - 1}$ of The unreduced Burau matrices.

[F1]

$B_{i}$ is the identity outside rows and columns $i, i + 1$ , and its $2 \times 2$ block there is $(\begin{array}{cc} 1 - t & t \\ 1 & 0 \end{array})$ ; each $B_{i}$ is invertible (The unreduced Burau matrices).

[F2]

Matrix product is entrywise summation, $(A B)_{p q} = \sum_{k} A_{p k} B_{k q}$ , with the identity matrix as unit and the usual associativity and distributivity laws (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose, Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products).

[F3]

The Artin presentation of $B_{n}$ has generators $σ_{1}, \dots, σ_{n - 1}$ and the relations $σ_{i} σ_{i + 1} σ_{i} = σ_{i + 1} σ_{i} σ_{i + 1}$ and, for $∣ i - j ∣ > 1$ , $σ_{i} σ_{j} = σ_{j} σ_{i}$ ; a generator assignment satisfying these relations extends uniquely to a homomorphism (von Dyck) (The braid group by Artin presentation, Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

Proof

technique · direct

1.1F1F2

Far commutation. Write $B_{i} = I + M_{i}$ , where $M_{i} = B_{i} - I$ is supported in rows and columns ${i, i + 1}$ ; by [F1] every nonzero entry of $M_{i}$ has both indices in that pair. If $∣ i - j ∣ \geq 2$ , the index sets ${i, i + 1}$ and ${j, j + 1}$ are disjoint; for any $p, q$ and any $k$ , not both $M_{i} (p, k) \neq 0$ (which forces $p, k \in {i, i + 1}$ ) and $M_{j} (k, q) \neq 0$ can hold, so $(M_{i} M_{j})_{p q} = 0$ and $(M_{j} M_{i})_{p q} = 0$ by the product formula [F2]. Hence $B_{i} B_{j} = (I + M_{i}) (I + M_{j}) = I + M_{i} + M_{j} = B_{j} B_{i}$ .

1.2F1F2algebra

The braid relation. First compute in the $3 \times 3$ case: with $B_{1}^{(3)} = (\begin{array}{ccc} 1 - t & t & 0 \\ 1 & 0 & 0 \\ 0 & 0 & 1 \end{array})$ and $B_{2}^{(3)} = (\begin{array}{ccc} 1 & 0 & 0 \\ 0 & 1 - t & t \\ 0 & 1 & 0 \end{array})$ , direct entrywise multiplication [F2] gives $B_{1}^{(3)} B_{2}^{(3)} B_{1}^{(3)} = (\begin{array}{ccc} 1 - t & t - t^{2} & t^{2} \\ 1 - t & t & 0 \\ 1 & 0 & 0 \end{array}) = B_{2}^{(3)} B_{1}^{(3)} B_{2}^{(3)} .$ For general $i$ , the matrices $B_{i}$ and $B_{i + 1}$ are the identity outside rows and columns ${i, i + 1, i + 2}$ , and on that block they equal $B_{1}^{(3)}$ and $B_{2}^{(3)}$ respectively; since the identity part acts trivially on the complementary rows and columns, the product formula [F2] gives that $B_{i} B_{i + 1} B_{i}$ and $B_{i + 1} B_{i} B_{i + 1}$ have the displayed block on ${i, i + 1, i + 2}$ and the identity elsewhere. Hence $B_{i} B_{i + 1} B_{i} = B_{i + 1} B_{i} B_{i + 1}$ .

2.1F1F3step 1.1step 1.2∎

Von Dyck. Steps 1.1 and 1.2 verify exactly the defining relations of the Artin presentation [F3] under the assignment $σ_{i} \mapsto B_{i}$ ; von Dyck's theorem therefore yields a unique homomorphism $ρ_{n}^{m a t} : B_{n} \to {GL}_{n} (Λ_{1})$ with $ρ_{n}^{m a t} (σ_{i}) = B_{i}$ . Its values are products of the invertible matrices $B_{i}$ and their inverses, hence lie in ${GL}_{n} (Λ_{1})$ by [F1], so $ρ_{n}^{m a t}$ takes values in ${GL}_{n} (Λ_{1})$ . No choice principle is used.

Depends on

Used by

Cited to discharge well-definedness by The unreduced Burau matrices.

Dependency tree · two levels

27 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

Joan S. Birman and Tara E. Brendle, Braids: A Survey (background on Burau matrices, the cyclic cover and absolute homology) (standard reference, not scraped)
Vasudha Bharathram, Joan S. Birman and Tara E. Brendle, The Burau representation is faithful for n = 4, arXiv:2607.05283v1 (6 July 2026), section 2 (printed pp. 1-5) (standard reference, not scraped)