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.

A ribbon object defines a unique framed-tangle evaluation functor

Statement

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $C$ be a ribbon category (Twist and ribbon structure) with chosen left duals (Left dual and right dual object), braiding $c$ (Braiding) and twist $θ$ , and let $X \in C$ . Write $X_{+ 1} : = X$ and $X_{- 1} : = X^{\lor}$ . In a strict model of $C$ (Every braided monoidal category is monoidally equivalent to a strict braided one) there is a unique strict monoidal functor

$F_{X} ⁣ : T ⟶ C$

from the framed oriented tangle category $T$ with

$F_{X} (+) = X, F_{X} (-) = X^{\lor},$

$F_{X} (X_{ε, ε^{'}}^{+}) = c_{X_{ε}, X_{ε^{'}}}, F_{X} (X_{ε, ε^{'}}^{-}) = (c_{X_{ε^{'}}, X_{ε}})^{- 1}, F_{X} (\cup_{+ 1}) = {coev}_{X}, F_{X} (\cap_{+ 1}) = {ev}_{X}, F_{X} (φ_{+ 1}^{\pm 1}) = θ_{X}^{\pm 1},$

where the cup and cap are the coevaluation and evaluation maps attached to the chosen left duals and the signs are the blackboard conventions of The framed oriented tangle category. The remaining elementary tangles of $T$ , those carrying a negative sign at a cup, cap or twist, receive the values forced by these data through the relations. Explicitly put $j_{X} = u_{X} θ_{X} : X \to X^{\lor \lor}$ , with $u$ as in A braided rigid category has a Drinfeld morphism. Then

$F_{X} (\cup_{-}) = (1_{X^{\lor}} \otimes j_{X}^{- 1}) {coev}_{X^{\lor}}, F_{X} (\cap_{-}) = {ev}_{X^{\lor}} (j_{X} \otimes 1_{X^{\lor}}), F_{X} (φ_{-}^{\pm 1}) = θ_{X^{\lor}}^{\pm 1} .$

These are the right coevaluation and evaluation on $X$ induced by the ribbon structure; they need no identification $X^{\lor \lor} = X$ on objects. For a general ribbon category the same assignment determines a strong monoidal functor, unique up to the canonical coherence isomorphisms of the strictification. Isotopic framed tangles are equal morphisms of $T$ , so $F_{X}$ is an invariant of framed tangles. Uniqueness needs no choice.

Facts & Assumptions

Given: ${A C}_{ω}$ , a ribbon category $C$ with chosen left duals, braiding $c$ , twist $θ$ and an object $X$ .

[L1]

The reduced and redundant generator presentation, including its crossing sign dictionary, is Framed oriented tangles have the ribbon generator-and-relation presentation.

[L2]

Braided strictification is Every braided monoidal category is monoidally equivalent to a strict braided one. A strong monoidal equivalence transports evaluation, coevaluation and twist along its tensor constraints; applying its faithful underlying functor checks the zig-zag, balancing and ribbon-duality equations in the target.

[L3]

The left-dual zig-zags, braiding hexagons, and natural dual-compatible twist are those of Left dual and right dual object, Braiding and Twist and ribbon structure. The Drinfeld composite is A braided rigid category has a Drinfeld morphism.

[F1]

Turaev, Chapter I Theorem 2.5, printed pp. 39--40, and its deduction §3.5, printed pp. 53--55, construct the strict monoidal evaluator and prove uniqueness. The reduction to one color and the crossing dictionary are [L1]. The proof checks the Yang--Baxter, zig-zag, inverse and slide relations, proves the bent-crossing formulas from hexagons and evaluation naturality, and proves (3.2.h) from balancing and dual-compatibility. Formulas (2.5.d)--(2.5.e) are the reversed cups and caps; after expansion of $u θ$ they are exactly the displayed right-dual maps.

Proof

technique · direct

1.1L1L2L3givenconstruct

Transport the structure. Use [L2] to work in a strict braided model and transport the chosen duals and twist by its strong monoidal constraints. The equations in [L3] are preserved by that transport. Send a signed word to the ordered tensor product of $X$ and $X^{\lor}$ , with the empty word sent to the unit, and use the displayed generator values. Their sources and targets agree with the elementary tangles; in particular $\cap_{-}$ has input $X \otimes X^{\lor}$ and $\cup_{-}$ has output $X^{\lor} \otimes X$ .

2.1L1L3F1step 1.1algebra

Check the exact presentation. In the dictionary of [L1], the reduced crossing $Z^{+}$ receives $(c_{X^{\lor}, X})^{- 1}$ , rather than $c_{X, X^{\lor}}$ ; this is the mixed-orientation value of [F1]. The reduced generator assignment is consequently precisely [F1] under the same axioms [L3]. Its complete algebraic check therefore proves every reduced relation, and its formulas for the redundant generators give all remaining values. For clarity, the twist-square check begins with $(θ_{X}^{2} \otimes 1_{X^{\lor}}) {coev}_{X} = c_{X, X^{\lor}}^{- 1} c_{X^{\lor}, X}^{- 1} {coev}_{X}$ : naturality of $θ$ at coevaluation gives balancing on $X \otimes X^{\lor}$ , and dual-compatibility moves the second twist to the first factor. Tensor with $1_{X}$ , apply a cap and use the zig-zag and bent-crossing identities, as in [F1], to obtain exactly the twist-square relation in [L1].

3.1L1F1step 1.1step 2.1construct

Extend and prove uniqueness. Since the values satisfy a complete presentation, they define a strict monoidal functor on all words. Two such functors agree on reduced generators, hence on every word; the redundant values are forced by their defining expressions. Thus the strict-model evaluator exists and is unique.

4.1L1L2step 3.1∎

Return to the original category. Compose with the strong monoidal quasi-inverse in [L2], identify its strand values with $X$ and $X^{\lor}$ using the unit of the equivalence, and transport generator values along those isomorphisms. The resulting functor has the anchor values interpreted through its tensor and unit constraints. Any other strong monoidal evaluator with these normalized values is compared on each signed word by its iterated tensor constraint; those comparisons commute with each generator and therefore with every word by [L1]. They form the canonical monoidal natural isomorphism identifying the two evaluators. Finally, equal framed tangles are equal morphisms in $T$ , so their evaluations agree. Countable choice enters through the presentation [L1]; uniqueness and the generator computations introduce no further choice.

Depends on

Used by

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

V. G. Turaev, Quantum Invariants of Knots and 3-Manifolds (de Gruyter Studies in Mathematics 18, 1994) (standard reference, not scraped)
P. Etingof, S. Gelaki, D. Nikshych, and V. Ostrik, Tensor Categories (AMS Mathematical Surveys and Monographs 205), author's final version (standard reference, not scraped)