TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Monoid objects in a braided monoidal category form a monoidal category

Statement

Let $(C, \otimes, 1, c)$ be a braided monoidal category. Then the category $Mon (C)$ of monoid objects in $C$ is monoidal. For monoid objects $(A, μ_{A}, η_{A})$ and $(B, μ_{B}, η_{B})$ , the tensor product monoid has underlying object $A \otimes B$ , unit $η_{A} \otimes η_{B}$ , and multiplication

$μ_{A \otimes B} = (μ_{A} \otimes μ_{B}) \circ (1_{A} \otimes c_{B, A} \otimes 1_{B}),$

with brackets suppressed by coherence.

Facts & Assumptions

Given: A braided monoidal category $C$ and monoid objects $A, B$ in it.

[L1]

A braided monoidal category is a monoidal category with a braiding $c$ (Braided monoidal category).

[L2]

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

[L3]

After coherence, monoid-object axioms may be written without displaying associators or unitors (The monoid-object axioms may be written without associators).

[F1]

EGNO Exercise 8.8.2(iv) checks that the braided interchange formula above defines the tensor product of monoid objects and that the ambient associator and unit object make $Mon (C)$ monoidal.

Proof

technique · direct

1.1L1L2L3givenconstruct

Using [L3], define on $A \otimes B$ the multiplication and unit displayed in the statement. The formula is typed because $1_{A} \otimes c_{B, A} \otimes 1_{B}$ rewrites $A \otimes B \otimes A \otimes B$ as $A \otimes A \otimes B \otimes B$ , after which $μ_{A} \otimes μ_{B}$ lands in $A \otimes B$ .

2.1F1step 1.1algebra

The associativity and unit axioms for this multiplication are exactly the braided interchange identities proved in [F1]: one repeatedly moves the middle $B$ -tensorand past the middle $A$ -tensorand by the braiding, and the two possible threefold rearrangements agree because the hexagons express the Yang-Baxter compatibility needed for those moves. Hence $A \otimes B$ is again a monoid object.

3.1L1L2F1step 2.1algebra∎

If $f : A \to A^{'}$ and $g : B \to B^{'}$ are monoid morphisms, then $f \otimes g$ preserves the units and multiplications because tensoring respects composition and the braiding is natural. Thus tensoring extends to morphisms. The ambient associator and unit object of $C$ are monoid morphisms by the same coherence computation recorded in [F1], so they supply the associator and unit data for $Mon (C)$ . Therefore $Mon (C)$ is monoidal.

Depends on

Used by

Monoid objects in a symmetric monoidal category form a symmetric monoidal category Corollary

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

P. Etingof, S. Gelaki, D. Nikshych, and V. Ostrik, Tensor Categories, Exercise 8.8.2(iv) (standard reference, not scraped)