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.

The Rouquier complex is well defined up to canonical homotopy equivalence

Statement

Let $t, u$ be signed words for the same braid $v$ . Then the normalized map $γ_{t, u} ⁣ : F (t) ⟶ F (u)$ of Derived comparisons give unique normalized homotopy maps is a canonical homotopy equivalence, natural with respect to the multiplication maps: for every other braid $v^{'}$ with chosen words $t^{'}, u^{'}$ , the diagrams comparing $F (t) \otimes_{R} F (t^{'})$ with $F (u) \otimes_{R} F (u^{'})$ commute up to the canonical associativity isomorphisms, and $γ_{t, u}$ is the unique homotopy class with the prescribed derived image $c_{t, u}$ . Consequently the object $G_{v}$ of Rouquier complexes form a coherent braid group action is independent of the chosen representative up to canonical homotopy equivalence, and the notation $F (β)$ for the Rouquier complex of a braid element is well defined up to canonical isomorphism in $K^{b} (R^{e} -grmod)$ ; this is an isomorphism statement in the homotopy category, not an equality of complexes.

Facts & Assumptions

Given: Signed words $t, u$ for the same braid $v$ , words $t^{'}, u^{'}$ for a braid $v^{'}$ , and the normalized maps of Derived comparisons give unique normalized homotopy maps.

[F1]

Uniqueness and inverses. ${Hom}_{K^{b}} (F (t), F (u))$ is one-dimensional in degree $0$ , $γ_{t, u}$ is its unique element with derived image $c_{t, u}$ , $γ_{t, t} = i d$ and $γ_{u, t} γ_{t, u} = i d$ . (Derived comparisons give unique normalized homotopy maps, and the transitivity of the same system)

[F2]

The coherent action. The choices $G_{v} = F (t (v))$ and the normalized compositors $m_{v, w}$ assemble into a coherent action; in particular the composite of $m$ 's is associative and unital up to the canonical maps. (Rouquier complexes form a coherent braid group action)

Proof

technique · direct

1.1F1

By [F1] $γ_{t, u}$ is the unique degree-zero class with derived image $c_{t, u}$ and $γ_{u, t}$ is its two-sided homotopy inverse, so $γ_{t, u}$ is a canonical homotopy equivalence.

2.1F1F2step 1.1

Naturality: the composite $F (t) \otimes_{R} F (t^{'}) \to F (u) \otimes_{R} F (u^{'})$ given by $γ_{t, u} \otimes γ_{t^{'}, u^{'}}$ and the composite given by the compositors and the associator both lie in ${Hom}_{K^{b}}$ of one-dimensional degree-zero spaces, and their derived images are the same graph multiplication; by uniqueness they agree up to the canonical associativity isomorphism of [F2].

3.1F2step 2.1∎

The independence of the representative: replacing the word $t (v)$ by another word changes $G_{v}$ by $γ_{t, u}$ , a homotopy equivalence, and these comparisons are compatible with the compositors by step 2.1, so the object is well defined up to canonical isomorphism in $K^{b}$ .

Remarks

The statement is an isomorphism statement: $F (t)$ and $F (u)$ are generally not equal complexes, and the canonical comparison depends on the two words. No choice principle is used: the words are chosen, and the comparisons are then unique in internal degree $0$ . This is Rouquier's well-definedness statement underlying the construction of $G_{v}$ ; the coherent-action theorem is the finite form of the same statement.

Depends on

Used by

Khovanov's generator complexes for the HHH construction Definition
Decategorification of a Rouquier complex is the Hecke braid generator Proposition

Dependency tree · two levels

26 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)