Alphabeta Math
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 internal-hom composition morphism

Statement

In a right-closed monoidal category there is a natural morphism

comp⁡X,Y,Z:[Y,Z]⊗[X,Y]→[X,Z]

obtained by transposing the double evaluation map. For every object X there is also a unit morphism

uX:1→[X,X],

and these satisfy the associativity and unit laws for composition.

Facts & Assumptions

Given: A right-closed monoidal category.

[L1]

The evaluation morphism ev⁡X,Y:[X,Y]⊗X→Y and the transpose bijection C(A⊗X,Y)≅C(A,[X,Y]) are part of the internal-hom data (The internal hom and its evaluation morphism).

Proof

technique · direct
1.1givenL1construct

Consider the composite ([Y,Z]⊗[X,Y])⊗X≅[Y,Z]⊗([X,Y]⊗X)→1⊗ev⁡X,Y[Y,Z]⊗Y→ev⁡Y,ZZ. Transposing it across the adjunction −⊗X⊣[X,−] gives a unique morphism comp⁡X,Y,Z:[Y,Z]⊗[X,Y]→[X,Z].

1.2L1construct

Transpose the left unitor λX:1⊗X→X across the same adjunction to obtain uX:1→[X,X].

2.1step 1.1L1algebra

To compare the two composites [Z,W]⊗[Y,Z]⊗[X,Y]⇉[X,W], tensor each with X and postcompose with ev⁡X,W. Both have the same transpose, namely the triple evaluation map [Z,W]⊗[Y,Z]⊗[X,Y]⊗X→W, so the transposition bijection of [L1] forces the two composites to be equal.

2.2step 1.1step 1.2L1algebra

The left and right unit laws are proved the same way: after tensoring with X and evaluating, both candidate composites have transpose ev⁡X,Y. Hence the transposition bijection identifies them, so u is a unit for comp⁡.

3.1step 2.1step 2.2∎

Therefore the internal hom carries a natural composition morphism and objectwise unit morphisms satisfying associativity and the unit laws.

Depends on

Used by

Dependency tree · two levels

3 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