Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Artin automorphisms permute meridian conjugacy classes and fix the boundary word

Statement

For every braid word β in the generators σ1±1,…,σn−1±1 and every i, the element ρ(β)(xi) is conjugate in Fn to one of the generators x1,…,xn, and ρ(β)(x1x2⋯xn)=x1x2⋯xn. Here x1⋯xn is the boundary word, i.e. the element represented by the positively oriented boundary loop ∂ by The oriented boundary loop represents the ordered product of the standard meridians. No choice principle is used.

Facts & Assumptions

Given: the free group Fn=⟨x1,…,xn⟩ with its reduced words, the generators ρ(σi)±1 of Artin automorphisms of the free group, the homomorphism ρ:Bn→Aut⁡(Fn) of The Artin representation on a free group, an arbitrary braid word β, and the boundary loop ∂ with its class of The oriented boundary loop represents the ordered product of the standard meridians.

[F1]

The generator substitutions. For 1≤i≤n−1, ρ(σi)(xi)=xixi+1xi−1,ρ(σi)(xi+1)=xi,ρ(σi)(xj)=xj (j∉{i,i+1}), so ρ(σi) sends xi to the conjugate xi xi+1 xi−1 of xi+1, sends xi+1 to the generator xi, and fixes every other generator; and ρ(σi)(xixi+1)=(xixi+1xi−1) xi=xixi+1, so ρ(σi) fixes the ordered product. The inverse ρ(σi)−1 has image formulas ρ(σi)−1(xi)=xi+1, ρ(σi)−1(xi+1)=xi+1−1xixi+1 and fixes all other generators, so it too carries every basis letter to a conjugate of a generator and fixes the ordered product. (Artin automorphisms of the free group.)

[F2]

The representation. ρ is a group homomorphism, so ρ(β) is the composite of the automorphisms attached to the letters of β, with the leftmost letter the outermost map (the rightmost map is evaluated first), and ρ of the empty word is the identity. Two endomorphisms of Fn agree as soon as they agree on the free basis x1,…,xn, and equality of elements is decided by reduced words (The Artin representation on a free group, Free group on a set of generators, Reduced words form the free group on an alphabet).

[F3]

The boundary word. The class of the loop x1⋯xn is [x1]⋯[xn], and under the identification of π1(D2∖Qn,d) with Fn by the standard meridians it corresponds to the positively oriented boundary loop ∂ (The oriented boundary loop represents the ordered product of the standard meridians, Standard meridians of a punctured disk).

Proof

Proof technique: direct, by generators and preservation under composition and inversion.

1.1F1

The generator substitutions have the two properties. For each i and each sign, ρ(σi)±1 carries every basis letter xj to a conjugate of a generator: by [F1] the values are unchanged generators, xixi+1xi−1, or xi+1−1xixi+1, all of which are conjugates of generators (a generator is conjugate to itself via the empty word). Moreover ρ(σi)±1 fixes the ordered product δ=x1⋯xn: for ρ(σi) this is the last display of [F1], and for the inverse it follows by applying ρ(σi)−1 to the equality ρ(σi)(δ)=δ and using ρ(σi)−1ρ(σi)=id⁡.

1.2F1algebra

The two properties are preserved by composition and inversion. Let A,B∈Aut⁡(Fn) satisfy: A(xj) and B(xj) are conjugate to generators for every j, and A(δ)=B(δ)=δ. For the composite (A∘B), write B(xj)=Q−1xkQ with Q∈Fn; then (A∘B)(xj)=A(Q)−1 A(xk) A(Q), a conjugate of A(xk), which is a conjugate of a generator; and (A∘B)(δ)=A(B(δ))=A(δ)=δ. For the inverse, abelianisation sends each basis vector ek to some eπ(k); since the induced map is invertible, π is a permutation. Thus for every j there is a k with A(xk)=Q−1xjQ; applying A−1 and rearranging gives A−1(xj)=A−1(Q) xk A−1(Q)−1, a conjugate of a generator, and A−1(δ)=δ because A(δ)=δ.

2.1F2step 1.1step 1.2

Induction on the letters of the word. Let β be a braid word β1β2⋯βm with letters βk∈{σ1±1,…,σn−1±1}. If m=0, then β is the empty word and ρ(β)=id⁡, for which ρ(β)(xj)=xj is a conjugate of a generator and ρ(β)(δ)=δ. If m≥1, write β=β1β′; by [F2] ρ(β)=ρ(β1)∘ρ(β′), where ρ(β1)±1 is one of the automorphisms of step 1.1 and, by induction on m, ρ(β′) carries every basis letter to a conjugate of a generator and fixes δ. Step 1.2 applied to A=ρ(β1) and B=ρ(β′) then gives both properties for ρ(β).

3.1F3step 2.1∎

Conclusion. Steps 1.1, 1.2 and 2.1 show that every braid word β induces an automorphism carrying each xi to a conjugate of a generator and fixing δ=x1⋯xn; by [F3] this element is the one represented by the boundary loop ∂, which proves the statement. Every verification above was a finite computation with the displayed substitutions, so no choice principle is used.

Remarks

  • The two properties are exactly the necessary conditions of Artin's characterization of the braid subgroup of Aut⁡(Fn): see thm-artins-characterization-of-the-braid-subgroup-of-aut-f-n.
  • Only the direction from the word to the automorphism is asserted here; the converse, that every automorphism with the two properties comes from a braid word, is thm-every-peripheral-boundary-preserving-free-group-automorphism-is-an-artin-automorphism.

Depends on

Used by

Dependency tree · two levels

23 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