Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31
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 endomorphisms of the tensor unit form a commutative monoid

Statement

If (C,⊗,1,α,λ,ρ) is a monoidal category, then End⁡C(1) is a commutative monoid. Its multiplication may be taken to be composition, and it agrees with the transport of tensor product along λ1. In particular, a strict one-object monoidal category has a commutative endomorphism monoid.

Facts & Assumptions

Given: A monoidal category (C,⊗,1,α,λ,ρ).

[L1]

A monoidal category has a bifunctor ⊗, unit object 1, and unit isomorphisms λ1:(1⊗1)→1 and ρ1:(1⊗1)→1 (Monoidal category).

[L2]

The two unitors agree on the unit object: λ1=ρ1 (The two unitors agree on the tensor unit).

[L3]

A unital associative operation is a monoid operation (Semigroup and monoid).

[L4]

Two unital operations with the same unit and the interchange law coincide and are commutative (Eckmann–Hilton: two unital operations satisfying interchange coincide and are commutative).

Proof

technique · direct
1.1givenL1L2

On End⁡C(1) let f∘g be ordinary composition and define f∗g:=λ1∘(f⊗g)∘λ1−1. Composition is associative with unit 11. Naturality of λ at f gives λ1∘(11⊗f)=f∘λ1, so 11∗f=f. Naturality of ρ at f gives ρ1∘(f⊗11)=f∘ρ1, and [L2] identifies ρ1 with λ1. Hence f∗11=f as well, so ∗ has the same unit 11.

2.1step 1.1L1algebra

For f,g,h,k∈End⁡C(1), one has ((f∘g)∗(h∘k))=λ1∘((f∘g)⊗(h∘k))∘λ1−1=λ1∘((f⊗h)∘(g⊗k))∘λ1−1=(f∗h)∘(g∗k), so the interchange law holds.

3.1step 1.1step 2.1L3L4

By [L4], the operations ∘ and ∗ coincide and their common value is commutative. Since composition is already associative and unital, [L3] shows that composition makes End⁡C(1) into a commutative monoid.

4.1step 3.1L5

If C is strict and has one object, then tensor and composition on endomorphisms are the same literal operation. Thus its endomorphism monoid is commutative; [L5] supplies the converse comparison with an ordinary one-object category.

5.1step 3.1step 4.1∎

Therefore the endomorphisms of the tensor unit form a commutative monoid.

Depends on

Used by

Dependency tree · two levels

15 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