TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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.

Duality yields adjunctions of tensoring functors

Statement

If $V^{\lor}$ is a left dual of $V$ , then the functor $V^{\lor} \otimes -$ is left adjoint to $V \otimes -$ . Equivalently, for all objects $U, W$ there is a natural bijection

$Hom (V^{\lor} \otimes U, W) ≅ Hom (U, V \otimes W) .$

Dually, $- \otimes V^{\lor}$ is right adjoint to $- \otimes V$ .

Facts & Assumptions

Given: A monoidal category and a left dual $(V^{\lor}, {ev}_{V}, {coev}_{V})$ of $V$ .

[L1]

An adjunction is unit-counit data satisfying the two triangle identities (Adjunction by unit, counit, and the triangle identities).

[L2]

The pair $(V^{\lor}, {ev}_{V}, {coev}_{V})$ satisfies the zig-zag identities (Left dual and right dual object).

Proof

technique · direct

1.1

For each object $U$ , define a unit $η_{U} : U \to V \otimes (V^{\lor} \otimes U)$ by $U \overset{λ_{U}^{- 1}}{\to} 1 \otimes U \overset{{coev}_{V} \otimes 1_{U}}{\to} (V \otimes V^{\lor}) \otimes U \overset{α_{V, V^{\lor}, U}}{\to} V \otimes (V^{\lor} \otimes U) .$ For each object $W$ , define a counit $ε_{W} : V^{\lor} \otimes (V \otimes W) \to W$ by $V^{\lor} \otimes (V \otimes W) \overset{α_{V^{\lor}, V, W}^{- 1}}{\to} (V^{\lor} \otimes V) \otimes W \overset{{ev}_{V} \otimes 1_{W}}{\to} 1 \otimes W \overset{λ_{W}}{\to} W .$

givenL1L2construct

2.1

The composite $(V \otimes ε_{W}) \circ η_{V \otimes W}$ is exactly the first zig-zag for $V^{\lor}$ tensored with $W$ , and the composite $ε_{V^{\lor} \otimes U} \circ (V^{\lor} \otimes η_{U})$ is exactly the second zig-zag for $V^{\lor}$ tensored with $U$ . By [L2], both are identities.

step 1.1L2

3.1

Steps 1.1 and 2.1 provide an adjunction $V^{\lor} \otimes - ⊣ V \otimes -$ by [L1]. Transposition under this adjunction gives the displayed hom-set bijection, and the statement for right tensoring is the mirrored construction.

step 2.1L1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

P. Etingof, S. Gelaki, D. Nikshych, and V. Ostrik, Tensor Categories, Proposition 2.10.8 (standard reference, not scraped)