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

✓ 24 results · all verified · 11 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 13 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Monoidal Categories and Monoidal Functors

1 · Prerequisites

2 · Summary

This page introduces monoidal categories with the pentagon and triangle as the only axioms, then records the first places where they come from: finite products, endofunctor categories, module tensor products, and finite-meet posets. It also isolates the unit-constraint redundancies, because later pages need those formulas before coherence is available.

The second half fixes the functorial vocabulary. Lax, strong, and strict monoidal functors are kept separate; monoid objects and their modules are defined with all bracketings explicit; and the page ends by making the bracketing discipline itself formal. Until the next coherence page, only parenthesised tensor expressions are defined.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Monoidal category

Definition

A monoidal category is a category C equipped with:

such that the following two equations hold for all objects W,X,Y,Z∈C.

The pentagon axiom is

αW,X,Y⊗Z∘αW⊗X,Y,Z=(1W⊗αX,Y,Z)∘αW,X⊗Y,Z∘(αW,X,Y⊗1Z).

The triangle axiom is

(1X⊗λY)∘αX,1,Y=ρX⊗1Y.

This page imposes no further axiom. In particular, the equality λ1=ρ1 is not built into the definition; it is derived later on this page.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Mac Lane writes the associator in the opposite direction

Mac Lane's convention is the inverse of the one fixed in Monoidal category. This page writes

αX,Y,Z:((X⊗Y)⊗Z)⟶X⊗(Y⊗Z),

while Mac Lane's aX,Y,Z points

aX,Y,Z:X⊗(Y⊗Z)⟶(X⊗Y)⊗Z.

Thus aX,Y,Z=αX,Y,Z−1 and αX,Y,Z=aX,Y,Z−1. The page keeps this warning separate so that a reader comparing formulas with Mac Lane does not mistake a convention change for a mathematical disagreement.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The pentagon axiom and the triangle axiom are independent

Statement

Neither the pentagon axiom nor the triangle axiom follows from the other.

Facts & Assumptions

Given: The one-object category Z with End⁡Z(∗)=Z, composition m∘n=m+n, and tensor on morphisms m⊗n=m+n.

[L1]

A monoidal category consists of a bifunctor, a unit object, natural isomorphisms α,λ,ρ, and exactly the pentagon and triangle equations from Monoidal category.

Proof

technique · direct
1.1givenL1

In Z, every integer is invertible for composition, so any chosen integers can serve as the components of α,λ,ρ. The tensor prescription is a bifunctor because ((m′⊗n′)∘(m⊗n))=(m′+n′)+(m+n)=(m′+m)+(n′+n)=((m′∘m)⊗(n′∘n)). Thus only the pentagon and triangle equations need to be checked.

2.1step 1.1L1algebra

First choose α=0, λ=1, and ρ=0. Then the pentagon reads 0+0=0+0+0, so it holds, while the triangle becomes 0+1=0, namely 1=0, so it fails. Hence the pentagon does not imply the triangle.

2.2step 1.1L1algebra

Now choose α=1, λ=0, and ρ=1. Then the triangle reads 1+0=1, so it holds, while the pentagon becomes 1+1=1+1+1, namely 2=3, so it fails. Hence the triangle does not imply the pentagon.

3.1step 2.1step 2.2∎

The two witnesses prove that neither axiom is a consequence of the other.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Strict monoidal category

Definition

A strict monoidal category is a monoidal category (C,⊗,1,α,λ,ρ) (Monoidal category) in which

((X⊗Y)⊗Z)=X⊗(Y⊗Z),1⊗X=X,X⊗1=X

as literal equalities of objects, and the constraint isomorphisms are identities:

αX,Y,Z=1X⊗(Y⊗Z),λX=1X,ρX=1X.

Thus a strict monoidal category does not merely identify the two bracketings up to a specified isomorphism; it makes them equal on the nose.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The reverse and the opposite of a monoidal category

Definition

Let (C,⊗,1,α,λ,ρ) be a monoidal category (Monoidal category).

Its reverse monoidal category Crev has the same underlying category and unit object, but tensor

X⊗revY:=Y⊗X.

On morphisms, f:X→X′ and g:Y→Y′ are sent to f⊗revg:=g⊗f:Y⊗X⟶Y′⊗X′.

The associator of Crev is

αX,Y,Zrev:((X⊗revY)⊗revZ)=Z⊗(Y⊗X)→αZ,Y,X−1(Z⊗Y)⊗X=X⊗rev(Y⊗revZ),

and its unit constraints are

λXrev:=ρX,ρXrev:=λX.

Its opposite monoidal category Cop is the opposite category (Opposite category Cop) with the same objects, the same unit object, and tensor bifunctor defined on morphisms by fop⊗gop:=(f⊗g)op. Its structure maps are obtained from the inverse original isomorphisms:

αX,Y,Zop:=((αX,Y,Z−1)op):((X⊗Y)⊗Z)→X⊗(Y⊗Z),

λXop:=((λX−1)op):(1⊗X)→X,ρXop:=((ρX−1)op):(X⊗1)→X,

where passage to Cop reverses the direction of the original inverse isomorphisms.

These two constructions are different: reversing the tensor order is not the same operation as reversing all morphisms.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31Open item page →

A category with finite products is monoidal

Statement

If a category C has binary products and a terminal object, then C is monoidal with tensor product × and unit object any terminal object 1. Dually, if C has binary coproducts and an initial object, then C is monoidal with tensor product ⊔ and unit object any initial object.

Facts & Assumptions

Given: A category C with binary products and a terminal object 1.

[L1]

A binary product X×Y represents pairs of arrows into X and Y, and a one-object product is canonically that object (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

[L2]

A terminal object receives a unique morphism from every object (Initial object, terminal object, and zero object).

[L3]

A monoidal category needs a bifunctor on C×C, natural isomorphisms α,λ,ρ, and the pentagon and triangle equations (Monoidal category).

Proof

technique · direct
1.1givenL1L2L3

Let X⊗Y:=X×Y and let the unit object be 1. On morphisms, define (f,g)↦f×g by the universal property of the binary product. Because product pairings are unique, identities and compositions are preserved componentwise, so ×:C×C→C is a bifunctor.

1.2L1L2construct

Let λX:(1×X)→X and ρX:(X×1)→X be the canonical product projections. If !X:X→1 is the unique map from [L2], then the inverse of λX is the pairing ⟨!X,1X⟩:X→1×X, and the inverse of ρX is ⟨1X,!X⟩:X→X×1. Hence λ and ρ are natural isomorphisms.

2.1step 1.1L1construct

For objects X,Y,Z, let αX,Y,Z:((X×Y)×Z)→X×(Y×Z) be the unique arrow whose three composite projections are the obvious first, second, and third projections. Define αX,Y,Z−1 similarly. By the same uniqueness argument, these arrows are inverse and natural.

3.1step 2.1step 1.2L1algebra

Both sides of the pentagon are arrows from (((W×X)×Y)×Z) to W×(X×(Y×Z)). They have the same four composites with the terminally iterated product projections, so [L1] makes them equal. The same argument on the two projections from (1×(X×Y)) to X and Y shows the triangle equation.

4.1step 3.1L1L2L3∎

Therefore (C,×,1,α,λ,ρ) is a monoidal category. The coproduct statement is proved by the same construction with pairings replaced by copairings and terminal replaced by initial, using the dual clauses already present in Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations and Initial object, terminal object, and zero object.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Set, Cat, and every complete category are cartesian monoidal

Statement

The categories Set and Cat are cartesian monoidal. More generally, every complete category is cartesian monoidal.

Facts & Assumptions

Given: The standard product structures on sets and on small categories.

[L1]

Any category with binary products and a terminal object is monoidal under that product (A category with finite products is monoidal).

[L2]

Sets and functions form the category Set (Sets and functions form the large locally small category Set), and small categories, functors, and natural transformations form the strict 2-category Cat (Small categories, functors, and natural transformations form the strict 2-category Cat).

[L3]

A complete category has all small limits and in particular a terminal object and binary products (Finite, small, and large limits and colimits; complete and cocomplete categories).

Proof

technique · direct
1.1L1L2

The cartesian product of sets and the singleton set give binary products and a terminal object in Set, so [L1] yields a monoidal structure on Set.

1.2L1L2

In Cat, the product category is the categorical binary product and the one-object category is terminal, so [L1] yields a monoidal structure on Cat.

1.3L1L3

If C is complete, then [L3] gives the required terminal object and binary products, and [L1] makes C cartesian monoidal.

2.1step 1.1step 1.2step 1.3∎

Therefore Set, Cat, and every complete category are cartesian monoidal.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31Open item page →

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.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31Open item page →

The endofunctor category of a small category is strict monoidal under composition

Statement

If C is a small category, then the endofunctors of C and their natural transformations form a strict monoidal category under functor composition, with tensor unit 1C.

Facts & Assumptions

Given: A small category C.

[L1]

When the source is small, functors C→C and natural transformations between them form the functor category [C,C] (Functor category [C,D]).

[L2]

If both source and target are small, that functor category is itself small (If C is small and D is locally small then [C,D] is locally small; if both are small it is small).

[L3]

A strict monoidal category has literal associativity and unit equalities and identity constraints (Strict monoidal category).

Proof

technique · direct
1.1givenL1L2

By [L1] and [L2], [C,C] is a legitimate category whose objects are endofunctors of C and whose morphisms are natural transformations.

2.1step 1.1construct

Define the tensor product on objects by F⊗G:=F∘G, and on morphisms by whiskered horizontal composition of natural transformations. The unit object is the identity functor 1C.

3.1step 2.1L3

Composition of functors is literally associative and unital, so ((F⊗G)⊗H)=F⊗(G⊗H) and 1C⊗F=F=F⊗1C on the nose. The associator and unitors are therefore identity transformations.

3.2step 2.1algebra

Whiskering respects identities and compositions, so the tensor on morphisms is a bifunctor.

4.1step 3.1step 3.2L3∎

Hence [C,C] is strict monoidal under composition.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A monoid object in a small endofunctor category is exactly a monad

Statement

Let C be a small category. Then the following are equivalent for an endofunctor T:C→C:

  1. T is a monad on C.
  2. In the strict monoidal category [C,C] under composition, T is equipped with morphisms η:1C⇒T,μ:T∘T⇒T satisfying the associativity and unit equations for a monoid object.

Facts & Assumptions

Given: A small category C and an endofunctor T:C→C.

[L1]

A monad on C is an endofunctor together with natural transformations η:1C⇒T and μ:T2⇒T satisfying the monad associativity and unit equations (Monad on a category).

[L2]

The phrase "monoid object in the endofunctor category" is used only when that category exists; in particular it is valid for a small source category (The monoid description of a monad requires an endofunctor category).

[L3]

For a small category, [C,C] is strict monoidal under composition (The endofunctor category of a small category is strict monoidal under composition).

Proof

technique · direct
1.1givenL2L3

By [L2] and [L3], the endofunctors of C form a strict monoidal category whose tensor is composition and whose unit is 1C. Thus a monoid-object structure on T is exactly data η:1C⇒T and μ:T∘T⇒T with the usual associative and unital diagrams, because the associator and unitors are identities.

2.1step 1.1L1

The equations described in step 1.1 are precisely μ∘Tμ=μ∘μT and μ∘Tη=1T=μ∘ηT, which are exactly the monad laws in [L1]. Hence every monoid object in [C,C] is a monad.

2.2L1step 1.1

Conversely, if (T,η,μ) is a monad, then [L1] gives exactly the same two diagrams, so the same data make T a monoid object in [C,C].

3.1step 2.1step 2.2∎

Therefore the two notions are equivalent for small C.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Monoid objects and comonoid objects in a monoidal category

Definition

Let (C,⊗,1,α,λ,ρ) be a monoidal category (Monoidal category).

A monoid object in C is an object M together with morphisms

μ:M⊗M⟶M,η:1⟶M,

such that

μ∘(μ⊗1M)=μ∘(1M⊗μ)∘αM,M,M,

μ∘(η⊗1M)=λM,μ∘(1M⊗η)=ρM.

A comonoid object in C is an object C together with morphisms

Δ:C⟶C⊗C,ε:C⟶1,

such that

(αC,C,C)∘(Δ⊗1C)∘Δ=(1C⊗Δ)∘Δ,

(ε⊗1C)∘Δ=λC−1,(1C⊗ε)∘Δ=ρC−1.

The associator and unitors are written explicitly because this page does not yet identify different bracketings automatically.

DefinitionDefinition: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Modules over a monoid object, their morphisms, and their category

Definition

Let M be a monoid object in a monoidal category (C,⊗,1,α,λ,ρ) (Monoid objects and comonoid objects in a monoidal category).

A left M-module is an object X together with an action morphism

a:M⊗X⟶X

such that

a∘(μ⊗1X)=a∘(1M⊗a)∘αM,M,X,

a∘(η⊗1X)=λX.

A morphism of left M-modules from (X,a) to (Y,b) is a morphism f:X→Y in C such that

f∘a=b∘(1M⊗f).

Facts & Assumptions

Given: A monoid object (M,μ,η) and left M-modules (X,a), (Y,b), and (Z,c).

[L1]

Verification

technique · direct
1.1givenL1

For every module (X,a), the identity 1X is a module morphism because 1X∘a=a=a∘(1M⊗1X). Thus identities exist.

1.2givenL1algebra

If f:(X,a)→(Y,b) and g:(Y,b)→(Z,c) are module morphisms, then (g∘f)∘a=g∘(f∘a)=g∘b∘(1M⊗f)=c∘(1M⊗g)∘(1M⊗f)=c∘(1M⊗(g∘f)), so g∘f is again a module morphism.

2.1step 1.1step 1.2L1∎

Because composition in C is associative by [L1], the module morphisms with these identities and composites form a category.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Monoid objects in a cartesian category are internal monoids; in Set they are ordinary monoids

Statement

Let C have finite products and let M be an object of C. With the cartesian monoidal structure from A category with finite products is monoidal, a monoid object structure on M is exactly a multiplication morphism μ:M×M→M and a unit morphism e:1→M satisfying the ordinary associativity and unit equations after the canonical product rebracketings are inserted. In particular, in Set these are exactly ordinary monoids in the sense of Semigroup and monoid.

Facts & Assumptions

Given: A category C with finite products and an object M.

[L1]

The cartesian monoidal structure on C uses product as tensor and a terminal object as unit (A category with finite products is monoidal).

[L2]

A monoid object is an object with multiplication and unit maps satisfying associativity and unit equations with the monoidal associator and unitors written explicitly (Monoid objects and comonoid objects in a monoidal category).

[L3]

An ordinary monoid is a set with an associative unital binary operation (Semigroup and monoid).

Proof

technique · direct
1.1givenL1L2

By [L1], the tensor is M×M and the unit is a terminal object 1. So [L2] says exactly that a monoid object on M is data μ:M×M→M and e:1→M satisfying the usual associative and left and right unit diagrams, with the only extra notation being the canonical rebracketing isomorphism ((M×M)×M)≅M×(M×M).

2.1step 1.1L3algebra

In Set, a morphism 1→M is the choice of an element e∈M, and a morphism M×M→M is a binary operation on the underlying set. The three diagrams from step 1.1 then say exactly μ(μ(x,y),z)=μ(x,μ(y,z)) and μ(e,x)=x=μ(x,e) for all x,y,z∈M.

3.1step 1.1step 2.1L2L3∎

Therefore monoid objects in a cartesian monoidal category are associative unital multiplications internal to that cartesian structure, and in Set they are exactly ordinary monoids.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31Open item page →

Abelian groups are monoidal under the tensor product

Statement

The category Ab of abelian groups is monoidal with tensor product ⊗Z and unit object Z. The associator and unitors are the canonical tensor-product isomorphisms over the commutative ring Z, and a morphism A⊗ZB→C is exactly the same data as a bilinear map A×B→C.

Facts & Assumptions

Given: Abelian groups A,B,C,D.

[L1]

Abelian groups and Z-modules have the same objects and morphisms (Abelian groups and Z-modules have the same objects and morphisms).

[L2]

The category of abelian groups already exists as an abelian category (Abelian groups form an abelian category).

[L4]

Over a commutative ring there are natural symmetry and associativity isomorphisms for tensor products (Symmetry and associativity isomorphisms for tensor products over a commutative ring).

[L5]

For modules over a unital ring, homomorphisms out of A⊗RB are in bijection with balanced maps out of A×B (Universal property of the tensor product for balanced maps into abelian groups).

Proof

technique · direct
1.1givenL1

By [L1], every abelian group is a Z-module and every group homomorphism is Z-linear. Thus the tensor product over Z of two abelian groups is again an abelian group, and the tensor-product maps are morphisms in Ab.

1.2L3L4

The associativity isomorphism ((A⊗ZB)⊗ZC)≅A⊗Z(B⊗ZC) and the unit isomorphisms Z⊗ZA≅A and A⊗ZZ≅A are exactly the maps supplied by [L3] and [L4] for the commutative ring Z.

2.1step 1.1step 1.2L1L5

By [L5], homomorphisms A⊗ZB→C are the same as balanced maps A×B→C. By step 1.1 and [L1], balanced over Z is exactly bilinear for abelian groups, so the same universal property identifies homomorphisms A⊗ZB→C with bilinear maps A×B→C. Together with step 1.2 this is the monoidal structure on Ab.

3.1step 1.1step 1.2step 2.1L2L3L4L5∎

Therefore Ab is monoidal under ⊗Z with unit object Z.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Monoid objects in abelian groups are rings

Statement

Facts & Assumptions

Given: An abelian group A.

[L1]

A monoid object in a monoidal category is an object with multiplication and unit morphisms satisfying associative and unital diagrams (Monoid objects and comonoid objects in a monoidal category).

[L2]

In Ab the tensor product is ⊗Z, the unit object is Z, and maps A⊗ZA→A correspond exactly to bilinear maps A×A→A (Abelian groups are monoidal under the tensor product).

[L3]

A ring is an abelian group under addition together with an associative unital multiplication distributing over addition on both sides (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).

Proof

technique · direct
1.1givenL1L2

By [L1] and [L2], a monoid object structure on A is a homomorphism μ:A⊗ZA→A and a homomorphism η:Z→A. The map μ corresponds to a bilinear operation (x,y)↦x⋅y on A, and η is determined by the element 1:=η(1)∈A.

2.1step 1.1L1L2L3

The monoid-object associativity and unit diagrams from [L1] translate under the correspondence in [L2] to (x⋅y)⋅z=x⋅(y⋅z) and 1⋅x=x=x⋅1. Because μ is a group homomorphism in each variable, the operation is bilinear, hence distributes over the abelian-group addition on both sides.

3.1step 2.1L2L3

Thus the additive abelian-group structure on A, together with multiplication ⋅ and unit 1, satisfies exactly the axioms in [L3], so A is a ring. Conversely, any ring yields such a bilinear multiplication and unit homomorphism, hence a monoid object in Ab.

4.1step 3.1L3∎

Therefore monoid objects in abelian groups are exactly rings.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31Open item page →

Modules over a commutative ring form a monoidal category

Statement

If R is a commutative ring, then the category R-Mod is monoidal with tensor product ⊗R and unit object R.

Facts & Assumptions

Given: A commutative ring R and R-modules L,M,N.

[L1]

R is a commutative ring in the sense of Commutative ring, and its modules and module homomorphisms form the category R-Mod (Left modules over a fixed ring and module homomorphisms form the large locally small category R-Mod).

[L2]

Tensor products of compatible bimodules are associative and have the regular module as tensor unit (Associativity of tensor products for compatible bimodules, The regular module is a tensor unit: R⊗RN≅N and M⊗RR≅M).

[L3]

Over a commutative ring the tensor product admits the natural symmetry and associativity isomorphisms (Symmetry and associativity isomorphisms for tensor products over a commutative ring).

[L4]

Module homomorphisms induce tensor-product homomorphisms functorially (Module homomorphisms induce tensor-product homomorphisms functorially).

Proof

technique · direct
1.1givenL1

By [L1], the modules under discussion already form a category. Because R is commutative, every left R-module is canonically an (R,R)-bimodule, so M⊗RN is again an R-module.

1.2L2L3

The associator ((L⊗RM)⊗RN)→L⊗R(M⊗RN) and the unitors R⊗RM→M and M⊗RR→M are exactly the isomorphisms supplied by [L2] and [L3].

2.1step 1.1step 1.2L1L2L3L4

By [L4], tensoring homomorphisms is functorial in each variable, so ⊗R is a bifunctor on R-Mod. Steps 1.1 and 1.2 therefore provide the data of a monoidal category.

3.1step 2.1∎

Hence modules over a commutative ring form a monoidal category under tensor product.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A poset with finite meets is a strict monoidal category

Statement

Let P be a poset with a top element ⊤ and binary meets. Then the category associated to P is a strict monoidal category with tensor product x⊗y:=x∧y and unit object ⊤.

Facts & Assumptions

Given: A poset P with top element ⊤ and binary meet operation ∧.

[L1]

A lattice supplies binary meets, written ∧ (Lattices, distributive lattices, and order ideals).

[L2]

A preorder, and hence a poset, determines a category with at most one morphism between two objects (A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps).

[L3]

A strict monoidal category has literal associativity and unit equalities and identity constraints (Strict monoidal category).

Proof

technique · direct
1.1givenL2

By [L2], P becomes a category whose objects are the elements of P and whose morphisms are the order relations.

2.1step 1.1L1L2

Define x⊗y:=x∧y on objects. Because meet is monotone in each variable, the unique arrows x→x′ and y→y′ induce the unique arrow x∧y→x′∧y′, so ⊗ is a bifunctor.

3.1step 2.1L1L2L3

The universal property of meet gives (x∧y)∧z=x∧(y∧z) and ⊤∧x=x=x∧⊤ as equalities of objects in the poset. Since each hom-collection has at most one arrow, the associator and unitors are automatically identity morphisms.

4.1step 3.1L3∎

Therefore the associated category is strict monoidal.

TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The left unitor of a tensor product is determined by the associator

Statement

In any monoidal category,

λX⊗Y=(λX⊗1Y)∘α1,X,Y

for all objects X,Y.

Facts & Assumptions

Given: A monoidal category and objects X,Y.

[L1]

The monoidal-category axioms are the pentagon and triangle from Monoidal category.

[F1]

Proposition 2.2.4 of EGNO proves that, under those axioms and with the same associator orientation as this page, the left unitor satisfies λX⊗Y=(λX⊗1Y)∘α1,X,Y.

Proof

technique · direct
1.1givenL1F1

The hypotheses of [F1] are exactly those in [L1], so [F1] applies to the present monoidal category.

2.1step 1.1F1∎

Therefore the displayed identity holds for every pair X,Y.

TheoremStatement: Literature-sourcedProof: Literature-sourcedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The right unitor of a tensor product is determined by the associator

Statement

In any monoidal category,

ρX⊗Y∘αX,Y,1=1X⊗ρY

for all objects X,Y.

Facts & Assumptions

Given: A monoidal category and objects X,Y.

[L1]

The monoidal-category axioms are the pentagon and triangle from Monoidal category.

[F1]

Proposition 2.2.4 of EGNO proves that, under those axioms and with the same associator orientation as this page, the right unitor satisfies ρX⊗Y∘αX,Y,1=1X⊗ρY.

Proof

technique · direct
1.1givenL1F1

The hypotheses of [F1] are exactly those in [L1], so [F1] applies to the present monoidal category.

2.1step 1.1F1∎

Therefore the displayed identity holds for every pair X,Y.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The two unitors agree on the tensor unit

Statement

In any monoidal category,

λ1=ρ1.

Facts & Assumptions

Given: A monoidal category with tensor unit 1.

[L1]

The left unitor satisfies λ1⊗1=(λ1⊗11)∘α1,1,1 (The left unitor of a tensor product is determined by the associator).

[L2]

The right unitor satisfies ρ1⊗1∘α1,1,1=11⊗ρ1 (The right unitor of a tensor product is determined by the associator).

[F1]

Corollary 2.2.5 of EGNO proves that, under the same monoidal-category axioms and associator convention, one has λ1=ρ1.

Proof

technique · direct
1.1givenL1L2F1

The monoidal-category hypotheses required by [F1] are exactly the ones under which [L1] and [L2] were proved, so [F1] applies to the present category.

2.1step 1.1F1

Therefore λ1=ρ1.

3.1step 2.1∎

Therefore the two unitors agree on the tensor unit.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

How Mac Lane's original coherence conditions reduce to this page's two axioms

Mac Lane's 1963 Theorem 5.2 lists five coherence conditions involving the associator and unit constraints. The present page starts from only the pentagon and triangle of Monoidal category. The gap is closed by the three later items on this page:

So the page's two axioms and Mac Lane's larger historical package define the same notion; the extra conditions become theorems rather than axioms.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The unit-constraint redundancies are cited mathematically through EGNO

The mathematical source used on this page for the unit-constraint redundancies is EGNO: Proposition 2.2.4 is the pair of formulas proved in The left unitor of a tensor product is determined by the associator and The right unitor of a tensor product is determined by the associator, and Corollary 2.2.5 is The two unitors agree on the tensor unit.

EGNO's bibliographical notes attribute Proposition 2.2.4 to Kelly. This page therefore cites EGNO for the mathematics and Kelly only for that historical attribution. It does not claim to quote Kelly's own wording or numbering.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Lax, strong, and strict monoidal functors

Definition

Let (C,⊗,1,α,λ,ρ) and (D,⊠,1′,α′,λ′,ρ′) be monoidal categories (Monoidal category).

A lax monoidal functor is a functor F:C→D (Covariant functor, identity functor, composite functor, and contravariant functor) together with natural transformations (Natural transformation and its components)

F2;X,Y:F(X)⊠F(Y)⟶F(X⊗Y),

and

the morphism

F0:1′⟶F(1),

such that, for all X,Y,Z,

F(αX,Y,Z)∘F2;X⊗Y,Z∘(F2;X,Y⊠1F(Z))=F2;X,Y⊗Z∘(1F(X)⊠F2;Y,Z)∘αF(X),F(Y),F(Z)′,

F(λX)∘F2;1,X∘(F0⊠1F(X))=λF(X)′,

F(ρX)∘F2;X,1∘(1F(X)⊠F0)=ρF(X)′.

A lax monoidal functor is strong monoidal when the natural transformation F2 is a natural isomorphism (Natural isomorphism)—equivalently, every component F2;X,Y is an isomorphism—and F0 is an isomorphism.

A strong monoidal functor is strict monoidal when the functor preserves the unit and tensor on the nose and every structure map above is an identity.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Why the bare phrase 'monoidal functor' is ambiguous across sources

Remark

The term "monoidal functor" is not source-stable. Mac Lane's Chapter XI.2 and the older lax-oriented literature use it for what this page calls a lax monoidal functor. EGNO's Definition 2.4.1 uses it only for the strong case.

For that reason this library does not use the phrase bare. It writes "lax monoidal", "strong monoidal", or "strict monoidal" explicitly, as in Lax, strong, and strict monoidal functors.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Monoidal natural transformation

Definition

Let F,G:C→D be lax monoidal functors (Lax, strong, and strict monoidal functors). A monoidal natural transformation θ:F⇒G is a natural transformation (Natural transformation and its components) such that

θX⊗Y∘F2;X,Y=G2;X,Y∘(θX⊠θY)

for all objects X,Y, and

G0=θ1∘F0.

Thus θ is compatible both with the binary structure maps and with the unit map.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

Lax monoidal functors compose, and composition preserves strength and strictness

Statement

The composite of two lax monoidal functors is again lax monoidal. If both functors are strong, the composite is strong; if both are strict, the composite is strict.

Facts & Assumptions

Given: Lax monoidal functors F:C→D and G:D→E.

[L1]

A lax monoidal functor is a functor together with structure maps F2,F0 satisfying associativity and unit equations; strong means those maps are isomorphisms and strict means they are identities (Lax, strong, and strict monoidal functors).

[L2]

A monoidal natural transformation is compatible with the binary and unit structure maps (Monoidal natural transformation).

Proof

technique · direct
1.1givenL1construct

Define the composite structure maps by (GF)0:=G(F0)∘G0 and (GF)2;X,Y:=G(F2;X,Y)∘G2;F(X),F(Y). These are the only typed composites from G(F(X))⊗G(F(Y)) to GF(X⊗Y) and from the unit of E to GF(1).

2.1step 1.1L1L2

Paste the associativity square for G with the image under G of the associativity square for F. The outside rectangle is exactly the associativity axiom for (GF)2. Pasting the two unit squares gives the left and right unit axioms for (GF)0. Hence GF is lax monoidal.

3.1step 1.1step 2.1L1

If both F and G are strong, then every map used in step 1.1 is an isomorphism, so (GF)0 and (GF)2 are isomorphisms. If both are strict, those maps are identities, so the composite structure maps are identities too.

4.1step 2.1step 3.1∎

Therefore composition preserves laxness, strength, and strictness.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-31Open item page →

A lax monoidal functor carries monoid objects to monoid objects

Statement

Let F:C→D be a lax monoidal functor. If (M,μ,η) is a monoid object in C, then F(M) is a monoid object in D with multiplication

F(M)⊠F(M)→F2;M,MF(M⊗M)→F(μ)F(M)

and unit

1′→F0F(1)→F(η)F(M).

Facts & Assumptions

Given: A lax monoidal functor F:C→D and a monoid object (M,μ,η) in C.

[L1]

A lax monoidal functor has structure maps F2 and F0 satisfying associativity and unit compatibility (Lax, strong, and strict monoidal functors).

[L2]

A monoid object is defined by multiplication and unit maps satisfying associativity and unit diagrams (Monoid objects and comonoid objects in a monoidal category).

Proof

technique · direct
1.1givenL1L2construct

Define μ′:=F(μ)∘F2;M,M and η′:=F(η)∘F0. These are the only typed maps with the displayed source and target.

2.1step 1.1L1L2

For associativity, paste the lax associativity square for F with the image under F of the monoid-object associativity square for μ. Both composites from (F(M)⊠F(M))⊠F(M) to F(M) equal F(μ∘(1M⊗μ)∘αM,M,M) with the same inserted F2-maps. Hence μ′ is associative.

2.2step 1.1L1L2

The left and right unit diagrams for η′ are obtained in the same way by pasting the lax unit squares with the image under F of the two unit diagrams for (M,μ,η). Thus η′ is a two-sided unit for μ′.

3.1step 2.1step 2.2L2∎

Therefore (F(M),μ′,η′) is a monoid object in D.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Monoidal equivalence and monoidal quasi-inverse data

Definition

A monoidal equivalence from C to D is a strong monoidal functor F:C→D (Lax, strong, and strict monoidal functors) together with:

  • a strong monoidal functor G:D→C;
  • monoidal natural isomorphisms η:1C⇒GF,ε:FG⇒1D (Monoidal natural transformation).

Here GF and FG carry the composite strong monoidal structures of Lax monoidal functors compose, and composition preserves strength and strictness, and each identity functor carries the strict monoidal structure whose binary and unit maps are identities. Thus both displayed transformations are between specified lax monoidal functors.

Thus the underlying functor F is an equivalence of categories in the sense of Equivalence, quasi-inverse, and adjoint equivalence of categories, but the monoidal quasi-inverse G is part of the data and not a canonical construction. By Every equivalence of categories can be equipped as an adjoint equivalence, one may choose the underlying equivalence data so that the triangle identities also hold, but that extra choice is not built into the base definition here.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Parenthesised tensor words and their evaluation functors

Definition

Fix symbols x1,…,xn. A parenthesised tensor word on these letters is formed recursively by:

  • each xi is a word;
  • the unit symbol 1 is a word;
  • if u and v are words, then (u⊗v) is a word;

subject to the condition that, after deleting every 1 and every pair of parentheses, the letters x1,…,xn appear exactly once and in that order.

If C is a monoidal category (Monoidal category), each such word determines an evaluation functor Eu:Cn→C recursively:

  • Exi is the ith projection;
  • E1 is the constant functor at the unit object;
  • E(u⊗v) is the composite of (Eu,Ev):Cn→C×C with the tensor bifunctor.

These evaluation functors are the only tensor expressions regarded as defined on this page before coherence is proved.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Parenthesised tensor words of a fixed length are counted by the Catalan numbers

Statement

For n≥1, let an be the number of parenthesised tensor words on the letters x1,…,xn with no inserted unit symbol. Then a1=1 and

an=∑k=1n−1akan−k(n≥2).

Equivalently, an=Cn−1, where the Catalan numbers are defined by C0=1 and

Cm=∑k=0m−1CkCm−1−k(m≥1).

Facts & Assumptions

Given: The recursive formation rule for parenthesised tensor words.

[L1]

A parenthesised tensor word is either one letter or a composite (u⊗v) built recursively, with the letters kept in order (Parenthesised tensor words and their evaluation functors).

Proof

technique · direct
1.1givenL1

For n=1 there is only the word x1, so a1=1.

1.2L1

If n≥2, every word has a unique outermost decomposition (u⊗v), where u uses the first k letters and v uses the remaining n−k letters for a unique k with 1≤k≤n−1. Conversely, every such pair (u,v) produces a word on n letters.

2.1step 1.2algebra

Therefore the words on n letters are partitioned by the value of k, and for fixed k there are akan−k choices. Summing over k gives an=∑k=1n−1akan−k.

3.1step 1.1step 2.1algebra∎

The recurrence in step 2.1 is exactly the Catalan recurrence after the index shift an=Cn−1, and step 1.1 matches the initial value C0=1. Hence an=Cn−1 for all n≥1.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Unbracketed tensor strings are not yet defined on this page

Remark

Before coherence is proved, an unbracketed expression A1⊗⋯⊗An with n≥3 has no meaning by itself on this page. A two-fold product is already defined by the tensor bifunctor; for three or more factors, what is defined is a parenthesised tensor word and its evaluation functor from Parenthesised tensor words and their evaluation functors.

So later pages that write an unbracketed string must depend on the coherence page that licenses suppressing the parentheses. On the present page, every triple or longer tensor expression is written with its brackets shown.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Isbell's warning that isomorphic objects cannot simply be identified

Remark

Mac Lane records Isbell's objection to the idea that one can make every monoidal category strict merely by identifying isomorphic objects. In a skeleton of Set, choose an infinite set D with D≅D×D and note that both projections from D×D are epic.

If one then tried to force the associator to be the identity in that skeleton, the projection formulas collapse so far that every two endomorphisms f,g:D→D become equal. That is absurd: the identity of D and any nontrivial constant endomorphism are different. So strictification is a theorem about equivalence, not a license to replace isomorphic objects by equal ones without changing the category.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

FALSE: every monoidal category is strict

Statement

False claim: every monoidal category is strict.

Facts & Assumptions

Given: A skeleton of Set containing an infinite set D with D≅D×D.

[L1]

A strict monoidal category makes associativity and unit equalities literal and all constraints identities (Strict monoidal category).

[L2]

In the Isbell skeleton example, forcing those identities collapses every endomorphism D→D to the same map, which is absurd (Isbell's warning that isomorphic objects cannot simply be identified).

Refutation

technique · direct
1.1L1

If every monoidal category were strict, then the monoidal structure on that skeleton of Set would satisfy the condition in [L1].

1.2L2

But [L2] says that in this example such an identification forces all endomorphisms D→D to be equal, contradicting the existence of distinct endomorphisms such as the identity and a constant map.

2.1step 1.1step 1.2∎

Therefore not every monoidal category is strict.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-31Open item page →

FALSE: the standard unit-constraint identities must all be imposed as independent axioms

Statement

False claim: besides the pentagon and triangle, the tensor-product formulas for the left and right unitors and the equality on the unit object must all be imposed as independent axioms.

Facts & Assumptions

Given: The unit-constraint formulas already proved on this page.

[L1]

The left unitor satisfies λX⊗Y=(λX⊗1Y)∘α1,X,Y (The left unitor of a tensor product is determined by the associator).

[L2]

The right unitor satisfies ρX⊗Y∘αX,Y,1=1X⊗ρY (The right unitor of a tensor product is determined by the associator).

[L3]

The two unitors agree on the tensor unit (The two unitors agree on the tensor unit).

Refutation

technique · direct
1.1L1L2

By [L1] and [L2], the two tensor-product formulas for the unitors follow from the monoidal axioms and are not independent axioms.

1.2L3

By [L3], even the remaining equality on the unit object is a theorem rather than an extra axiom.

2.1step 1.1step 1.2∎

Therefore the claim is false.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-31Open item page →

FALSE: every lax monoidal functor has invertible structure maps

Statement

False claim: every lax monoidal functor has invertible structure maps.

Facts & Assumptions

Given: The page's distinction between lax and strong monoidal functors and the cartesian monoidal category Set.

[L1]

A strong monoidal functor is a lax monoidal functor whose binary and unit structure maps are isomorphisms (Lax, strong, and strict monoidal functors).

[L2]

Different sources use the bare phrase "monoidal functor" differently, so this library avoids the bare phrase precisely to prevent that conflation (Why the bare phrase 'monoidal functor' is ambiguous across sources).

[L3]

The power set P(X) consists of all subsets of X (The power set P(x)={ z:z⊆x }).

[L4]

The category Set is cartesian monoidal (Set, Cat, and every complete category are cartesian monoidal).

Refutation

technique · direct
1.1L3L4constructalgebra

Let P:Set→Set send a function to its direct-image map on power sets. Define P2(A,B):=A×B and let P0:1→P(1) select the full singleton. Direct images preserve identities and composition, and (f×g)(A×B)=f(A)×g(B) proves naturality. Both associativity composites send (A,B,C) to A×B×C with the indicated bracketing, and the unit composites return A. Thus P is lax monoidal.

2.1L1step 1.1algebra

For X=Y={0,1}, the diagonal {(0,0),(1,1)}⊆X×Y is not A×B for any A⊆X and B⊆Y. Hence P2 is not surjective, so P is not strong by [L1].

3.1L1L2step 1.1step 2.1∎

The distinction in [L1] is therefore genuine, and the stated universal claim is false. The qualifier "lax" makes the claim source-stable, while [L2] explains why the bare phrase "monoidal functor" would not.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

FALSE: the pentagon axiom follows from the triangle axiom

Statement

False claim: the pentagon axiom follows from the triangle axiom.

Facts & Assumptions

Given: The independence theorem for the two axioms.

[L1]

There exists a monoidal-structure witness satisfying the triangle axiom while failing the pentagon axiom (The pentagon axiom and the triangle axiom are independent).

Refutation

technique · direct
1.1given

If the pentagon followed from the triangle, every structure satisfying the triangle would also satisfy the pentagon.

1.2L1

But [L1] supplies a witness satisfying the triangle and failing the pentagon.

2.1step 1.1step 1.2∎

Therefore the claim is false.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

FALSE: an unbracketed three-fold tensor product is already well defined in any monoidal category

Statement

False claim: in any monoidal category, the expression A⊗B⊗C is already a defined object before any coherence theorem is invoked.

Facts & Assumptions

Given: The bracketing discipline fixed on this page.

[L1]

Before coherence, only parenthesised tensor words are defined expressions; unbracketed strings are not yet defined (Unbracketed tensor strings are not yet defined on this page).

Refutation

technique · direct
1.1given

The claim suppresses the choice between (A⊗B)⊗C and A⊗(B⊗C).

1.2L1

But [L1] says the page does not identify those expressions automatically before coherence.

2.1step 1.1step 1.2∎

Therefore the claim is false.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-31Open item page →

FALSE: a monoid object in an endofunctor category is the definition of a monad

Statement

False claim: a monoid object in an endofunctor category is the definition of a monad.

Facts & Assumptions

Given: The endofunctor-category comparison theorem.

[L1]

A monad is defined directly by an endofunctor and unit and multiplication natural transformations, without assuming that an endofunctor category exists (Monad on a category).

[L2]

The equivalence with monoid objects in an endofunctor category is proved only when that category exists; this library forms it for small source categories (A monoid object in a small endofunctor category is exactly a monad, The monoid description of a monad requires an endofunctor category).

[L3]

Sets and functions form the large category Set (Sets and functions form the large locally small category Set).

Refutation

technique · direct
1.1L1construct

The identity endofunctor on the large category Set, with identity unit and multiplication, is a monad by [L1].

2.1L2L3

By [L3], Set is large, and [L2] says this library does not form its endofunctor category [Set,Set]. Thus the monad in step 1.1 exists here although the proposed monoid-object formulation is unavailable.

3.1step 1.1step 2.1∎

Therefore the claim is false.

Sources