TheoremStatement: 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 two-braid category is strict rigid monoidal

Statement

Let $B_{n}$ be the braid-indexed category with an object $v$ for each $v \in B_{n}$ and ${Hom}_{B_{n}} (v, w) : = {Hom}_{K^{b} (R^{e} -grmod)} (G_{v}, G_{w}),$ where $G_{v}$ is the chosen complex of Rouquier complexes form a coherent braid group action. Composition is the carrier composition. Its evaluation $v \mapsto G_{v}$ is fully faithful and has image the full subcategory on those complexes. Keep the braid labels even if two carriers coincide. Define $v ⊠ w = v w$ and, for $f : v \to v^{'}$ , $g : w \to w^{'}$ , define $f ⊠ g = m_{v^{'}, w^{'}} \circ (f \otimes_{R} g) \circ m_{v, w}^{- 1} .$ Then:

$B_{n}$ is strict monoidal, with unit label $1$ and identity associativity and unit constraints (Strict monoidal category);
$v^{- 1}$ is both a left and a right dual of $v$ . Evaluation and coevaluation are the identity of the unit label, with the tensor constraints $m$ furnishing their usual carrier realizations;
the isomorphism classes form a group under $⊠$ , with $[v] [w] = [v w]$ and $[v^{- 1}] = [v]^{- 1}$ . The same identities hold for their classes in the split Grothendieck ring of the additive envelope $B_{n}^{\oplus}$ : its objects are finite formal sums of labels, its morphisms are matrices of the above Hom spaces, and its tensor extends $⊠$ distributively (Split Grothendieck group of an additive category).

No Hecke-algebra identification, no faithfulness and no complete invariant of braids are asserted here; the decategorification of the complexes themselves is the subject of the decategorification proposition of this page.

Facts & Assumptions

Given: the carrier complexes $G_{v}$ and coherent comparisons $m_{v, w}$ of Rouquier complexes form a coherent braid group action, with $G_{1} = R$ .

[F1]

The comparisons are invertible and satisfy the tensor associativity pentagon and canonical unit constraints; they compare $G_{v} \otimes_{R} G_{w}$ to $G_{v w}$ (Rouquier complexes form a coherent braid group action).

[F2]

A strict monoidal category has associative and unital tensor on both objects and morphisms with identity constraints (Strict monoidal category).

[F3]

Left and right duals are evaluation and coevaluation pairs satisfying the triangle identities; an object with both is rigid (Left dual and right dual object, Rigid object and rigid monoidal category).

[F4]

The split Grothendieck group of an essentially small additive category is generated by object isomorphism classes modulo $[X \oplus Y] = [X] + [Y]$ . (Split Grothendieck group of an additive category).

Proof

technique · transport tensor along the coherent carrier comparisons, retaining formal braid labels

1.1F1F2algebra

The category structure is well defined since every Hom and composition is taken from the carrier homotopy category, and the evaluation is fully faithful by its Hom definition. The displayed morphism tensor preserves identity maps and composition: in the composite of two tensor maps the middle factors $m^{- 1} m$ cancel, and tensor composition is componentwise. The pentagon for $m$ makes the two transported products of three morphisms equal; on objects both are the label $v w u$ . The unit constraints for $m$ give $f ⊠ 1_{1} = f = 1_{1} ⊠ f$ . Thus the transported tensor is strictly associative and unital on morphisms as well as on labels, so [F2] applies.

2.1F1F3step 1.1

Set the dual label to $v^{- 1}$ . The product labels $v^{- 1} ⊠ v$ and $v ⊠ v^{- 1}$ both equal $1$ . Take the evaluation and coevaluation maps to be $1_{1}$ in both orders. By the morphism tensor just proved, their triangle composites are $1_{v}$ and $1_{v^{- 1}}$ ; in the carrier category the corresponding evaluation is $m_{v^{- 1}, v} : G_{v^{- 1}} \otimes_{R} G_{v} \to R$ and the corresponding coevaluation is $m_{v, v^{- 1}}^{- 1} : R \to G_{v} \otimes_{R} G_{v^{- 1}}$ , and [F1] supplies the same triangles under evaluation. Hence these are both duals as in [F3].

3.1F1F4step 1.1step 2.1∎

Since every label has this inverse, the isomorphism-class monoid is a group with the stated product and inverse identities. Finite formal sums and matrices form the additive envelope described in the Statement, and the tensor extends bilinearly. In its split Grothendieck group [F4], multiplication respects direct-sum relations, has unit $[1]$ , and satisfies $[v] [w] = [v w]$ and $[v] [v^{- 1}] = [1]$ . This gives the stated class identities without treating the invertible-object category itself as additive.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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