Alphabeta Math
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.

In a rigid category every morphism of monoidal functors is an isomorphism

Statement

Let F,G:CD be strong monoidal functors from a rigid monoidal category C to a monoidal category D. Then every monoidal natural transformation η:FG is a natural isomorphism.

Facts & Assumptions

Given: A rigid monoidal category C, a monoidal category D, strong monoidal functors F,G:CD, and a monoidal natural transformation η:FG.

[L1]

Every object of C has chosen duals because C is rigid (Rigid object and rigid monoidal category).

[L2]

A monoidal natural transformation respects both the tensor structure and the unit structure (Monoidal natural transformation).

[L4]

Compatible maps between two left duals of the same object are unique (Duals are unique up to a unique compatible isomorphism).

Proof

technique · direct
1.1

Because C is rigid, choose for each object X a left dual X. Since F and G are strong monoidal, they send the duality maps of X to duality maps of F(X) and G(X): after transporting the images of evX and coevX across the strong monoidal structure isomorphisms, F(X) is a left dual of F(X) and G(X) is a left dual of G(X).

givenL1construct
2.1

Define ξX:G(X)F(X) using the transported duality maps by the composite G(X)1G(X)coevF(X)1F(X)F(X)G(X)1ηX1F(X)G(X)G(X)1evG(X)F(X)1F(X). This construction uses F(X) and G(X) as left duals of F(X) and G(X) from step 1.1; it does not identify a left dual of F(X) with F(X).

step 1.1L2construct
3.1

Expand ξXηX using step 2.1. Naturality of η, together with its tensor and unit compatibility from [L2], moves ηX across the coevaluation and evaluation; the remaining composite is the zig-zag identity for the dual pair F(X),F(X). Hence ξXηX=1F(X). The mirrored calculation uses the zig-zag identity for G(X),G(X) and gives ηXξX=1G(X). Thus every component ηX is an isomorphism, so η is a natural isomorphism.

step 1.1step 2.1L2L4

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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