TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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 tensor unit is an internal-hom unit

Statement

In a right-closed monoidal category there is a natural isomorphism $[1, Y] ≅ Y$ for every object $Y$ . Consequently there is a natural bijection

$C (1, [X, Y]) ≅ C (X, Y) .$

Facts & Assumptions

Given: A right-closed monoidal category.

[L1]

The right internal hom $[X, -]$ is right adjoint to $- \otimes X$ , with transposition bijection $C (A \otimes X, Y) ≅ C (A, [X, Y])$ (The internal hom and its evaluation morphism).

[L2]

Right adjoints to a fixed functor are unique up to unique natural isomorphism (The internal hom is unique up to a unique adjunction-compatible natural isomorphism).

Proof

technique · direct

1.1

The right unitor gives natural isomorphisms $A \otimes 1 ≅ A$ . Applying the transposition bijection of [L1] with $X = 1$ therefore gives natural bijections $C (A, Y) ≅ C (A \otimes 1, Y) ≅ C (A, [1, Y])$ . So the identity functor is also a right adjoint to $- \otimes 1$ . Since $[1, -]$ is another right adjoint to the same functor, [L2] gives $[1, Y] ≅ Y$ naturally in $Y$ .

givenL1L2

2.1

Apply the transposition bijection of [L1] with $A = 1$ . Because $1 \otimes X ≅ X$ , this gives $C (X, Y) ≅ C (1, [X, Y])$ . Rewriting the bijection in the opposite direction yields the displayed form.

step 1.1L1algebra

3.1

Thus the tensor unit recovers the external hom-set from the internal hom.

step 1.1step 2.1∎

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

G. M. Kelly, Basic Concepts of Enriched Category Theory, equations (1.25) and (1.26) (standard reference, not scraped)