TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Rouquier complexes form a coherent braid group action

Statement

For every braid $v \in B_{n}$ choose a signed word $t (v)$ representing it, taking $t (1)$ to be the empty word, and put $G_{v} : = F (t (v))$ , with $G_{1} : = R$ . For the action on $K^{b} (R -grmod)$ , set $F_{1} = Id$ and, for $v \neq 1$ , set $F_{v} : = G_{v} \otimes_{R} -$ . For $v, w \in B_{n}$ let $m_{v, w} ⁣ : G_{v} \otimes_{R} G_{w} ⟶ G_{v w}$ be the unique homotopy class whose derived image is the graph-multiplication comparison, transported through the associativity and unit isomorphisms of Bounded bimodule tensor is associative, unital, and compatible with cones; equivalently $m_{v, w}$ is $γ_{t (v) t (w), t (v w)}$ in the normalization of Derived comparisons give unique normalized homotopy maps. Let $m_{1} ⁣ : G_{1} \to R$ be the identity of the unit complex. For $v, w \neq 1$ , the compositor $μ_{v, w} : F_{v} F_{w} \Rightarrow F_{v w}$ is induced by associating $G_{v} \otimes_{R} (G_{w} \otimes_{R} -)$ to $(G_{v} \otimes_{R} G_{w}) \otimes_{R} -$ and then applying $m_{v, w} \otimes_{R} -$ , followed by the left-unit identification $R \otimes_{R} - ≅ Id$ when $v w = 1$ . If either index is $1$ , use the canonical tensor unit identifications, so the compositor is the identity after those identifications; set $u : F_{1} \Rightarrow Id$ to the identity. Then $(F_{v}, μ_{v, w}, u)$ is a coherent action of $B_{n}$ on $K^{b} (R -grmod)$ in the sense of Coherent action of a group on a category: the functors are the exact left tensor functors $G_{v} \otimes_{R} -$ for $v \neq 1$ , with the identity functor at $1$ , and both composites of every pentagon have the same derived image, namely the same associative graph multiplication, so the pentagon commutes by uniqueness in degree $0$ ; both unit triangles hold by the canonical tensor unit identifications. Equivalently, $v \mapsto (F_{v}, μ_{v, w}, u)$ is a monoidal functor from the discrete strict monoidal category $(B_{n}, \cdot)$ to the strict monoidal category of endofunctors of $K^{b} (R -grmod)$ . The construction uses one chosen word per braid and no other choice; no choice principle is needed.

Facts & Assumptions

Given: A choice $v \mapsto t (v)$ of signed word for each braid $v \in B_{n}$ , the word complexes $G_{v} = F (t (v))$ , and the maps $γ$ of Derived comparisons give unique normalized homotopy maps.

[F1]

Well-definedness of the $m_{v, w}$ . For any two choices of words for the same braid the normalized maps agree up to the transitive system, and for the concatenated words $t (v) t (w)$ and $t (v w)$ the class $γ_{t (v) t (w), t (v w)}$ is the unique homotopy class with the prescribed derived image; hence $m_{v, w}$ is independent of the auxiliary choices of the words used to define the concatenation, by transitivity. (Normalized comparison isomorphisms are transitive, Derived comparisons give unique normalized homotopy maps)

[F2]

The relations. The generator complexes satisfy $F_{i} \otimes_{R} F_{i}^{- 1} ≃ R$ , the three-term relation and far commutativity, so the word complex attached to any two words for the same braid is independent of the word up to the canonical comparisons. (Opposite Rouquier generator complexes are homotopy inverse, Rouquier complexes satisfy far commutativity, Rouquier complexes satisfy the three-term braid relation)

[F3]

Associativity and units of the tensor. The balanced tensor totalization is associative and unital up to canonical chain isomorphisms satisfying the pentagon and unit triangles, and compatible with cones. (Bounded bimodule tensor is associative, unital, and compatible with cones)

[F4]

The model of a coherent action. A coherent action consists of functors $F_{g}$ with $F_{1} = i d$ , chosen compositors $μ_{f, g} : F_{f} F_{g} \Rightarrow F_{f g}$ and a unit $u$ satisfying the pentagon and the two unit triangles. (Coherent action of a group on a category)

Proof

technique · direct

1.1F1F2F3

For $v, w \in B_{n}$ the composite $G_{v} \otimes_{R} G_{w} = F (t (v)) \otimes_{R} F (t (w))$ is a word complex for the concatenated word $t (v) t (w)$ , which represents $v w$ ; by [F2] it is canonically compared to $G_{v w} = F (t (v w))$ , so the class $m_{v, w}$ of the statement exists as the normalized comparison and is a homotopy equivalence. If $v, w \neq 1$ , associativity identifies $F_{v} F_{w}$ with $(G_{v} \otimes_{R} G_{w}) \otimes_{R} -$ ; tensoring $m_{v, w}$ with the input complex gives the compositor, followed by the left-unit identification when $v w = 1$ . If an index is $1$ , the canonical unit identification gives the identity compositor.

2.1F1F2step 1.1

The maps $m_{v, w}$ are compatible with replacing the representatives: if $a_{v} : G_{v} \to {\tilde{G}}_{v}$ are their normalized comparisons, then $a_{v w} m_{v, w} = {\tilde{m}}_{v, w} (a_{v} \otimes a_{w})$ , after canonical reassociation. Both sides have the same derived graph multiplication, so normalized uniqueness proves this equality in the correctly typed Hom space.

3.1F1F3step 2.1

Pentagon: after the associativity and unit identifications in [F3], the two composites from $F_{v} F_{w} F_{u}$ to $F_{v w u}$ are induced by the two composites of normalized maps $m$ from $G_{v} \otimes_{R} G_{w} \otimes_{R} G_{u}$ to $G_{v w u}$ . Their derived images are both the triple graph multiplication, so uniqueness in internal degree $0$ makes them agree. This also covers unit indices, where the compositor is the canonical unit identification.

3.2F3F4step 2.1

Unit triangles: since $t (1)$ is empty, the normalized comparisons $m_{v, 1}$ and $m_{1, v}$ are the identity under the right and left tensor unit isomorphisms, respectively. With $F_{1} = Id$ and $u = i d$ , these identifications give separately $μ_{v, 1} = F_{v} u$ and $μ_{1, v} = u F_{v}$ , including $v = 1$ . Thus both unit axioms of [F4] hold.

4.1F2F4step 1.1step 2.1step 3.1step 3.2∎

By steps 1.1, 2.1, 3.1 and 3.2 the functors $F_{v}$ and compositors $μ_{v, w}$ satisfy the pentagon and both unit triangles of [F4]. Since each $G_{v}$ has finite free terms on both sides, $G_{v} \otimes_{R} -$ is exact on bounded complexes of finite graded projectives and descends to the derived category; the identity functor at $1$ is exact as well. Thus these data define the asserted coherent braid group action. The representative system can be specified without a choice axiom: order the finite signed alphabet and take the shortest, then lexicographically least word in each nonempty braid class. The construction uses this system or any given representative system.

Depends on

Used by

Dependency tree · two levels

41 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

Raphaël Rouquier, Categorification of the braid groups, arXiv:math/0409593v1 (30 September 2004), §3 "The 2-braid group" (standard reference, not scraped)
Eugene Gorsky, Oscar Kivinen, José Simental, Algebra and geometry of link homology: Lecture Notes from the IHES 2021 Summer School, Bull. London Math. Soc. 55 (2023) 537-591, §3.1 (standard reference, not scraped)