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.

✓ 21 results · all verified · 10 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 11 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Braided and Symmetric Monoidal Categories

1 · Prerequisites

2 · Summary

This page adds the commutativity data that ordinary monoidal categories do not have. A braiding is not just a swap notation: it is a natural isomorphism with two hexagon axioms, and those axioms remain genuinely asymmetric until the symmetry relation cY,XcX,Y=1 is imposed.

The page then separates the two coherence theorems. In the symmetric case, canonical composites collapse to permutations and tensor words may be reordered freely. In the merely braided case, the surviving braid-group data is exactly what obstructs that stronger slogan, and it is also what makes the braid category the correct free object.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Braiding

Definition

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

A braiding on C is a natural isomorphism

cX,Y:X⊗Y⟶Y⊗X

natural in both variables (Natural isomorphism) such that, for all objects X,Y,Z,

αY,Z,X∘cX,Y⊗Z∘αX,Y,Z=(1Y⊗cX,Z)∘αY,X,Z∘(cX,Y⊗1Z),

and

αZ,X,Y−1∘cX⊗Y,Z∘αX,Y,Z−1=(cX,Z⊗1Y)∘αX,Z,Y−1∘(1X⊗cY,Z).

These are the two hexagon identities. The invertibility of each cX,Y is part of the data, not a consequence of the hexagons.

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

Braided monoidal category

Definition

A braided monoidal category is a monoidal category together with a chosen braiding in the sense of Braiding.

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

The inverse braiding is again a braiding

Statement

Let c be a braiding on a monoidal category C. Then the family

cX,Y′:=cY,X−1:X⊗Y⟶Y⊗X

is again a braiding on C.

Facts & Assumptions

Given: A braiding c on a monoidal category C.

[L1]

A braiding is a natural isomorphism cX,Y:X⊗Y→Y⊗X satisfying the two hexagon identities (Braiding).

Proof

technique · direct
1.1givenL1algebra

Because [L1] says each cX,Y is an isomorphism, the family cX,Y′=cY,X−1 is well defined. Inverting the naturality square for c and swapping the variable names shows that c′ is natural in both variables.

2.1L1step 1.1algebra

Substitute cX,Y′=cY,X−1 into the first hexagon for c′. After reversing the arrows, this equation is exactly the second hexagon for c from [L1] with the object names permuted. Hence the first hexagon holds for c′.

3.1L1step 2.1algebra∎

The same calculation with the roles of the two hexagons reversed shows that the second hexagon for c′ is the first hexagon for c written backwards. Therefore c′ satisfies both hexagon identities and is a braiding.

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

The braiding is compatible with the unit constraints

Statement

Let c be a braiding on a monoidal category C. Then for every object X,

ρX∘c1,X=λX,λX∘cX,1=ρX,

and consequently

c1,X=cX,1−1.

Facts & Assumptions

Given: A braided monoidal category with braiding c.

[F1]

In any braided monoidal category, Exercise 8.1.6 of EGNO derives the identities ρX∘c1,X=λX,λX∘cX,1=ρX.

[L1]

A braiding is, in particular, a family of isomorphisms satisfying the hexagons (Braiding).

Proof

technique · direct
1.1givenF1

The present hypotheses are exactly those of [F1], so the two displayed unit-compatibility identities hold for every object X.

2.1L1step 1.1algebra∎

By [L1], the morphisms c1,X and cX,1 are isomorphisms. Step 1.1 therefore gives c1,X=ρX−1λX,cX,1=λX−1ρX. These two formulas are inverse to each other, so c1,X=cX,1−1.

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

In a strict braided monoidal category the braiding satisfies the Yang-Baxter equation

Statement

Let C be a strict braided monoidal category. Then for all objects X,Y,Z,

(cY,Z⊗1X)∘(1Y⊗cX,Z)∘(cX,Y⊗1Z)=(1Z⊗cX,Y)∘(cX,Z⊗1Y)∘(1X⊗cY,Z).

In particular, when X=Y=Z, both sides are endomorphisms of X⊗X⊗X, and the relation becomes

(c⊗1)(1⊗c)(c⊗1)=(1⊗c)(c⊗1)(1⊗c).

Facts & Assumptions

Given: A strict braided monoidal category.

[L1]

A braided monoidal category carries a braiding satisfying the two hexagon identities (Braided monoidal category).

[L2]

In a strict monoidal category, the associator and both unitors are identity morphisms (Strict monoidal category).

Proof

technique · direct
1.1givenL1L2algebra

By [L2], both hexagon identities from [L1] lose all associators. They become cX,Y⊗Z=(1Y⊗cX,Z)∘(cX,Y⊗1Z) and cX⊗Y,Z=(cX,Z⊗1Y)∘(1X⊗cY,Z).

2.1L1step 1.1algebra

Naturality of cX,− with respect to the morphism cY,Z:Y⊗Z→Z⊗Y gives (cY,Z⊗1X)∘cX,Y⊗Z=cX,Z⊗Y∘(1X⊗cY,Z).

3.1step 1.1step 2.1algebra∎

Expand the left-hand occurrence of cX,Y⊗Z in step 2.1 by the first formula of step 1.1, and expand cX,Z⊗Y by the same formula with Y and Z interchanged. This yields (cY,Z⊗1X)∘(1Y⊗cX,Z)∘(cX,Y⊗1Z)=(1Z⊗cX,Y)∘(cX,Z⊗1Y)∘(1X⊗cY,Z), which is the stated Yang-Baxter relation. The special case X=Y=Z is the displayed braid equation.

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

Symmetric monoidal category

Definition

A symmetric monoidal category is a braided monoidal category (Braided monoidal category) whose braiding c satisfies

cY,X∘cX,Y=1X⊗Y

for all objects X,Y.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01Open item page →

In the presence of symmetry, one hexagon implies the other

Statement

Let C be a monoidal category equipped with a natural isomorphism cX,Y:X⊗Y→Y⊗X that satisfies one of the two braiding hexagons. If moreover

cY,X∘cX,Y=1X⊗Y

for all X,Y, then the other hexagon also holds. In particular, in a symmetric monoidal category either hexagon may be taken as the coherence axiom.

Facts & Assumptions

Given: A natural family cX,Y satisfying the symmetry equation and one braiding hexagon.

[L1]

In a symmetric monoidal category, the braiding satisfies cY,X∘cX,Y=1X⊗Y (Symmetric monoidal category).

Proof

technique · direct
1.1givenalgebra

Assume first that the given hexagon is αY,Z,X∘cX,Y⊗Z∘αX,Y,Z=(1Y⊗cX,Z)∘αY,X,Z∘(cX,Y⊗1Z). Inverting this equality gives αX,Y,Z−1∘cX,Y⊗Z−1∘αY,Z,X−1=(cX,Y−1⊗1Z)∘αY,X,Z−1∘(1Y⊗cX,Z−1).

2.1L1step 1.1algebra

Replace (X,Y,Z) in step 1.1 by (Z,X,Y). By [L1], the symmetry equation implies cU,V−1=cV,U for all objects U,V. After that substitution, step 1.1 becomes αZ,X,Y−1∘cX⊗Y,Z∘αX,Y,Z−1=(cX,Z⊗1Y)∘αX,Z,Y−1∘(1X⊗cY,Z), which is exactly the second braiding hexagon.

3.1step 2.1algebra∎

If instead the second hexagon is given, the same argument with the roles of the two hexagons reversed proves the first. Hence under the symmetry axiom either hexagon implies the other.

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

Braided monoidal functor

Definition

Let (C,c) and (D,c′) be braided monoidal categories (Braided monoidal category). A braided monoidal functor F:C→D is a strong monoidal functor (Lax, strong, and strict monoidal functors) with structure isomorphisms

JX,Y:F(X)⊗F(Y)⟶≅F(X⊗Y),J0:1D⟶≅F(1C),

such that for all objects X,Y,

JY,X∘cF(X),F(Y)′=F(cX,Y)∘JX,Y.

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

Being braided is a property of a strong monoidal functor

Remark

For a fixed strong monoidal functor, no extra coherence map has to be chosen in order to make it braided: one merely checks whether the already chosen tensor constraint satisfies the compatibility equation from Braided monoidal functor. In that sense, braidedness is a property of a strong monoidal functor rather than a second layer of structure.

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

The cartesian swap braiding is a symmetry

Statement

Let C be a category with finite products, regarded as a monoidal category under cartesian product. Then the swap maps

τX,Y:X×Y⟶Y×X,τX,Y(x,y)=(y,x),

form a braiding, and this braiding is symmetric.

Facts & Assumptions

Given: A category C with finite products.

[L1]

A category with finite products is monoidal under cartesian product (A category with finite products is monoidal).

[L2]

A symmetric monoidal category is a braided monoidal category whose braiding squares to the identity (Symmetric monoidal category).

[L3]

A braiding is a natural isomorphism satisfying the two hexagons (Braiding).

Proof

technique · direct
1.1givenL1L3construct

For each pair X,Y, the two coordinate projections from X×Y define a unique morphism τX,Y:X×Y→Y×X with first projection π2 and second projection π1. The same universal property defines its inverse τY,X, so the family is a natural isomorphism.

2.1step 1.1L1L3algebra

To check the first hexagon, compare both composites from X×(Y×Z) to (Y×Z)×X after composing with the three product projections. Each route sends (x,y,z) to (y,z,x), so the two maps are equal. The second hexagon is the same coordinate permutation written on ((X×Y)×Z) and is checked in the same way.

3.1L2step 1.1step 2.1algebra∎

Swapping twice returns every pair to itself, so τY,X∘τX,Y=1X×Y. By [L2], the cartesian swap braiding is therefore a symmetry.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01Open item page →

The double-braiding center is a symmetric monoidal subcategory

Statement

Let (C,c) be a braided monoidal category. Let Z2(C) be the full subcategory on those objects X such that

cY,X∘cX,Y=1X⊗Y

for every object Y of C. Then Z2(C) is closed under tensor product and unit, and the inherited braiding makes Z2(C) into a symmetric monoidal category.

Facts & Assumptions

Given: A braided monoidal category (C,c).

[L1]

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

[L2]

By definition, a braided monoidal category is symmetric exactly when cY,X∘cX,Y=1X⊗Y for all objects X,Y (Symmetric monoidal category).

[L3]

The braiding is compatible with the unit constraints, so c1,X=cX,1−1 (The braiding is compatible with the unit constraints).

[L4]

Canonical reassociations and unit insertions between fixed parenthesised tensor words are unique (Mac Lane coherence in canonical-map form).

Proof

technique · direct
1.1L3givenalgebra

The tensor unit belongs to Z2(C): for every Y, [L3] gives cY,1−1=c1,Y, hence cY,1∘c1,Y=11⊗Y.

1.2L1L4givenalgebra

Suppose X and Y lie in Z2(C), and let Z be arbitrary. By [L4], the canonical associators in the two hexagons may be suppressed after transporting both sides between the same parenthesised source and target. In that coherent notation, the hexagons give cZ,X⊗Y∘cX⊗Y,Z=(1X⊗cZ,Y)(cZ,X⊗1Y)(cX,Z⊗1Y)(1X⊗cY,Z).

2.1step 1.2givenalgebra

Transparency of X gives (cZ,X⊗1Y)(cX,Z⊗1Y)=1X⊗Z⊗1Y. Substituting this into step 1.2 leaves (1X⊗cZ,Y)(1X⊗cY,Z)=1X⊗(cZ,Y∘cY,Z), which is the identity by transparency of Y. Hence X⊗Y lies in Z2(C).

3.1L2step 1.1step 2.1algebra∎

Because the subcategory is full and is closed under tensor product by step 2.1 and under the unit by step 1.1, tensor products of its morphisms and the ambient associator and unitors all remain in it. The ambient braiding also restricts to it. For central objects X,Y, their defining condition says cY,X∘cX,Y=1X⊗Y. By the definition in [L2], the restricted braiding is therefore a symmetry. Thus Z2(C) is symmetric monoidal.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01Open item page →

Every braided monoidal category is monoidally equivalent to a strict braided one

Statement

Let (C,c) be a braided monoidal category. Then there exists a strict monoidal category D, a braiding cstr on D, and a monoidal equivalence F:C→D such that F is a braided monoidal functor.

Facts & Assumptions

Given: A braided monoidal category (C,c).

[L1]

Mac Lane strictification gives a monoidal equivalence from C to a strict monoidal category (Mac Lane strictification).

[L2]

A monoidal equivalence consists of a strong monoidal functor with strong monoidal quasi-inverse data (Monoidal equivalence and monoidal quasi-inverse data).

[L3]

A braided monoidal functor is a strong monoidal functor whose tensor constraint intertwines the two braidings (Braided monoidal functor).

[F1]

The braided strictification theorem in the cited monoidal-category source states that Mac Lane's strictification carries a unique transported braiding for which the strictification equivalence is braided monoidal.

Proof

technique · direct
1.1L1L2F1givenchoose

Apply [L1] and [L2] to obtain a monoidal equivalence F:C→D with D strict. By [F1], the braiding c transports across the full strong monoidal equivalence to a braiding cstr on D.

2.1L3F1step 1.1∎

The transported braiding is characterized by the compatibility square JY,X∘cF(X),F(Y)str=F(cX,Y)∘JX,Y. Thus [L3] makes F braided monoidal, and C is braided-monoidally equivalent to the strict braided monoidal category (D,cstr).

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

The braid group by Artin presentation

Definition

For n≥2, the braid group Bn is the group with generators σ1,…,σn−1 and relations

σiσi+1σi=σi+1σiσi+1(1≤i≤n−2),

σiσj=σjσi(1≤i,j≤n−1, ∣i−j∣>1).

Equivalently,

Bn=⟨σ1,…,σn−1∣σiσi+1σi=σi+1σiσi+1 (1≤i≤n−2), σiσj=σjσi (1≤i,j≤n−1, ∣i−j∣>1)⟩,

interpreted in the sense of Group presentation by generators and relations and Relators and relations; finitely generated, finitely related, and finite presentations.

For n=0 and n=1, there are no generators, and Bn is the trivial group given by the empty presentation.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-09-26 (gpt-6-sol)Open item page →

The two-strand braid group is infinite cyclic

Statement

The braid group B2 is cyclic, generated by σ1, and σ1 has infinite order. Hence B2 is an infinite cyclic group.

Facts & Assumptions

Given: The Artin presentation of the braid groups.

[L1]

The group B2 is presented by one generator σ1 and no braid relations (The braid group by Artin presentation).

[L2]

In the free group on an alphabet, reduced words are the elements, the empty word is the identity, and two reduced words represent the same element only when they are identical (Reduced words form the free group on an alphabet).

Proof

technique · direct
1.1givenL1algebra

By [L1], the presentation of B2 has one generator and no defining relator, so every element of B2 is a power of σ1. Thus B2 is cyclic.

2.1L1L2step 1.1

With no relators present, the presented group is the free group on the singleton alphabet {σ1}. For m>0 the power σ1m is represented by a word of m copies of σ1; for m<0 it is represented by ∣m∣ copies of the formal inverse. Each is a nonempty reduced word, distinct from the empty identity word by [L2]. Hence σ1m≠1 for every nonzero integer m.

3.1step 1.1step 2.1∎

Therefore the cyclic group B2=⟨σ1⟩ is infinite, so it is infinite cyclic.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-29Open item page →

The symmetric group has the Coxeter presentation

Statement

For n≥2, the symmetric group Sn has the presentation

Sn=⟨s1,…,sn−1∣si2=1, sisi+1si=si+1sisi+1, sisj=sjsi (∣i−j∣>1)⟩,

where, after relabelling the underlying set n={0,…,n−1} as {1,…,n}, si corresponds to the adjacent transposition (i i+1). For n=0,1, the trivial group has the empty presentation.

Facts & Assumptions

Given: The symmetric group Sn and the adjacent transpositions τi=(i i+1).

[L1]

The group Sn is defined on n={0,…,n−1}; conjugating by the order-preserving bijection k↦k+1 identifies it with the conventional symmetric group on {1,…,n} and transports adjacent transpositions (The finite symmetric group Sn, one-line notation, and cycle notation).

[F1]

The adjacent transpositions generate Sn for n≥2 (Adjacent transpositions generate the finite symmetric group Sn).

[F2]

A map from the generators of a presented group to a group extends to a homomorphism when the relators hold, and the extension is onto when the images generate the target (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

Proof

technique · direct
1.1F1F2F3

Fix n≥2 and let Gn be the group given by the displayed generators and relations. The adjacent transpositions τi=(i i+1) satisfy τi2=1. Transpositions with disjoint supports commute, and the two length-three words in τi,τi+1 both exchange i with i+2 and fix i+1. Thus every relator holds in Sn. By [F2] there is a homomorphism πn:Gn→Sn sending si to τi, and [F1] makes it surjective.

1.2algebra

Put H=⟨s1,…,sn−2⟩≤Gn, with H={1} when n=2. For 1≤j<n set rj=sn−1sn−2⋯sj, and set rn=1. The defining relations give the following right-multiplication rules for 1≤i<n: if i≤j−2, then rjsi=sirj by commuting si past every factor of rj; if i=j−1, then rjsi=rj−1; if i=j, then rjsi=rj+1 by sj2=1; and if i>j, then rjsi=si−1rj. For the last rule commute the final si left past sj,…,si−2, replace sisi−1si by si−1sisi−1, and commute the leading si−1 left past si+1,…,sn−1. For j=n, the rules are rnsi=sirn when i≤n−2 and rnsn−1=rn−1. Every coefficient on the left of a resulting rk lies in H.

2.1F2F3L1step 1.1step 1.2

The union T=⋃j=1nHrj contains 1=rn and, by step 1.2, is stable under right multiplication by every generator si. Since each si is its own inverse, every word in the generators lies in T, so Gn=T and ∣Gn∣≤n∣H∣. The defining relations of the presented group Gn−1 hold among s1,…,sn−2, hence [F2] gives a surjection Gn−1↠H; this includes G1={1} when n=2. Induction yields ∣Gn∣≤n!. Independently, a bijection of an n-element set has n choices for the first image, then n−1 for the second, and so on, hence ∣Sn∣=n! by [F3]. The surjection πn of step 1.1 is therefore a bijection and an isomorphism. Transport it through [L1] to obtain exactly the stated presentation on the library's underlying set.

3.1F3L1∎

If n=0 or 1, there are no adjacent transpositions and the only bijection of the underlying set is the identity. Its group is presented by the empty set of generators and relators.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passOpen item page →

The braid group surjects onto the symmetric group

Statement

For n≥2, use the one-based model Sn(1):=Sym⁡({1,…,n}), identified with the library's Sn=Sym⁡({0,…,n−1}) by conjugation with κn(k)=k+1 (The finite symmetric group Sn, one-line notation, and cycle notation, Adjacent transpositions generate the finite symmetric group Sn). Write Sn in this transported model below. The assignment σi↦(i i+1) extends to a surjective homomorphism

πn:Bn⟶Sn.

In the library's zero-based model, the same map is σi↦(i−1 i), obtained by conjugating πn with κn−1.

Facts & Assumptions

Given: The Artin presentation of Bn and the adjacent transpositions in the one-based model fixed in the Statement.

[L1]

The braid group Bn has generators σ1,…,σn−1 with the Artin braid and distant-commutativity relations (The braid group by Artin presentation).

[L2]

The adjacent transpositions generate Sn (Adjacent transpositions generate the finite symmetric group Sn).

[L3]

The symmetric group satisfies the Coxeter relations for adjacent transpositions (The symmetric group has the Coxeter presentation).

[L4]

A map of generators satisfying the relators extends uniquely from a presented group (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

Proof

technique · direct
1.1L1L3L4givenconstruct

By [L3], the adjacent transpositions in Sn satisfy the braid relations and the distant-commutativity relations from [L1]. Therefore [L4] extends the assignment σi↦(i i+1) to a homomorphism πn:Bn→Sn.

2.1L2step 1.1∎

The image of πn contains every adjacent transposition in the one-based model, so the transported generation clause of [L2] makes πn surjective. Conjugating its values by κn−1 preserves multiplication and surjectivity and sends (i i+1) to (i−1 i), giving the stated zero-based version.

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

The braid category

Definition

The braid category B is the category defined as follows.

  • Its objects are the natural numbers 0,1,2,….
  • For m≠n, there are no morphisms m→n.
  • For each n, the endomorphism group End⁡B(n) is the braid group Bn from The braid group by Artin presentation.

Composition is the group multiplication in each Bn. The tensor product on objects is addition. On morphisms, juxtaposition is the homomorphism Bm×Bn→Bm+n sending the first block generators σi to σi and the second block generators σj to σm+j. The Artin relations show directly that this is well defined, strictly associative, and unital. Thus B is a strict monoidal category (Strict monoidal category).

The standard block crossing βm,n moves the first m strands over the last n strands. Isotopy of braid diagrams, equivalently the Artin braid relations, gives naturality and the two block hexagons, so these crossings form a braiding (Braided monoidal category). Under this convention β1,1=σ1∈B2.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01Open item page →

Symmetric coherence

Statement

Let C be a symmetric monoidal category. For any two parenthesised tensor words built from the same finite list of objects, possibly in different orders, there is a unique canonical natural isomorphism between them determined only by the induced permutation of the letters. Canonical symmetric composites therefore depend only on the underlying permutation.

Facts & Assumptions

Given: A symmetric monoidal category C and two parenthesised tensor words on the same finite list of letters.

[L1]

A symmetric monoidal category is a braided monoidal category with involutive braiding (Symmetric monoidal category).

[L2]

Under the symmetry axiom, one braiding hexagon implies the other (In the presence of symmetry, one hexagon implies the other).

[L3]

Every braided monoidal category is braided-monoidally equivalent to a strict braided one (Every braided monoidal category is monoidally equivalent to a strict braided one).

[L4]

The symmetric group is generated by adjacent transpositions subject exactly to the Coxeter relations (The symmetric group has the Coxeter presentation).

[L5]

A parenthesised tensor word records an ordering and a bracketing of finitely many tensor factors (Parenthesised tensor words and their evaluation functors).

[F1]

In a strict symmetric monoidal category, the elementary adjacent swaps on tensor factors satisfy the Coxeter relations: si2=1 by symmetry, distant swaps commute by naturality, and the braid relation is the Yang-Baxter identity specialized to an involutive braiding.

Proof

technique · direct
1.1L1L3givenchoose

By [L1] and [L3], choose a braided monoidal equivalence from C to a strict braided monoidal category D. Because the braiding of C is involutive, the transported braiding on D is also involutive, so D is strict symmetric.

2.1L4L5F1step 1.1algebra

In the strict symmetric category D, every canonical map between two tensor words with the same ordered letters is built from adjacent swaps of neighboring factors. By [F1] and [L4], the resulting composite depends only on the permutation carrying the source word to the target word, not on the chosen decomposition of that permutation into adjacent transpositions.

3.1L2L3step 1.1step 2.1algebra∎

Transport this canonical map back across the equivalence chosen in step 1.1. Faithfulness of an equivalence preserves uniqueness, so the resulting canonical map in C depends only on the same permutation. Hence any two canonical symmetric composites with the same source, target, and underlying permutation are equal.

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

Labelled unbracketed and unordered tensor strings are well defined in a symmetric monoidal category

Statement

In a symmetric monoidal category, once a finite tensor product is regarded as a labelled list of occurrences X1,…,Xn, it may be written without specifying either a bracketing or an order: any two parenthesised reorderings of that same labelled list are canonically and uniquely identified.

Facts & Assumptions

Given: A symmetric monoidal category and a labelled finite list of tensor factor occurrences.

[L1]

Symmetric coherence supplies a unique canonical natural isomorphism between any two parenthesised reorderings of the same finite list of labelled factor occurrences (Symmetric coherence).

Proof

technique · direct
1.1givenalgebra

Any two written forms of the same labelled tensor expression differ only by a choice of brackets and a permutation of the listed occurrences.

2.1L1step 1.1∎

By [L1], those two parenthesised reorderings are canonically and uniquely isomorphic. Therefore suppressing both the brackets and the order does not change the resulting labelled tensor expression except by that unique canonical identification.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01Open item page →

Braided coherence fails in the symmetric form

Statement

There exists a braided monoidal category in which the canonical endomorphisms

1, cX,X2, cX,X4,…

of X⊗X are pairwise distinct. Consequently the symmetric slogan "every diagram built from associators and braidings commutes" is false for braided monoidal categories.

Facts & Assumptions

Given: The braid category B.

[L1]

In the braid category, the braiding on 1⊗1=2 is the generator σ1∈B2 (The braid category).

[L2]

The group B2 is infinite cyclic, so its distinct powers of σ1 are distinct morphisms (The two-strand braid group is infinite cyclic).

Proof

technique · direct
1.1givenL1algebra

Take X:=1 in the braid category. By [L1], the canonical braiding on X⊗X is σ1, so its even powers are the endomorphisms σ12m of the object 2.

2.1L2step 1.1algebra

By [L2], the elements 1,σ12,σ14,… are pairwise distinct in B2. Therefore the canonical endomorphisms 1,cX,X2,cX,X4,… are pairwise distinct in this braided monoidal category.

3.1step 2.1contradiction∎

If every formal diagram built from associators and braidings commuted in every braided monoidal category, then the morphisms in step 2.1 would all agree. They do not, so the symmetric-form coherence slogan fails in the braided setting.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01Open item page →

The braid category is the free strict braided monoidal category on one generator

Statement

Let C be a strict braided monoidal category and let X be an object of C. Then there is a unique strict braided monoidal functor

FX:B⟶C

from the braid category B such that FX(1)=X. Thus B is the free strict braided monoidal category on one generator.

Facts & Assumptions

Given: A strict braided monoidal category C and an object X∈C.

[L1]

A braided monoidal functor is determined by its action on objects and by compatibility with the braidings and tensor products (Braided monoidal functor).

[L2]

The braid category has objects the natural numbers and endomorphism groups Bn, with tensor product given by addition and juxtaposition (The braid category).

[L3]

In a strict braided monoidal category, the local braidings satisfy the Yang-Baxter equation (In a strict braided monoidal category the braiding satisfies the Yang-Baxter equation).

[L4]

A map of generators satisfying the relators extends uniquely from a presented group (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

Proof

technique · direct
1.1givenL2construct

Define FX(n):=X⊗n on objects, with FX(0):=1. For each generator σi∈Bn, define FX(σi) to be the morphism 1X⊗(i−1)⊗cX,X⊗1X⊗(n−i−1):X⊗n→X⊗n, where the braiding acts only on the ith and (i+1)st tensor factors.

2.1L3L4step 1.1algebra

By [L3], the neighboring generators from step 1.1 satisfy the braid relation. Local braidings on disjoint tensor factors commute because in a strict monoidal category they act on separate coordinates. Therefore the Artin relations of Bn hold, and [L4] extends the assignment of step 1.1 uniquely to a homomorphism Bn→Aut⁡(X⊗n) for every n.

3.1L1L2step 1.1step 2.1algebra

The family from step 2.1 defines a functor B→C because morphisms exist only between equal objects in B, and group multiplication in each Bn is respected by the constructed homomorphism. By construction FX(m+n)=FX(m)⊗FX(n) on objects, the tensor of braids is sent to juxtaposition of local braidings, and the standard braiding βm,n of B is sent to the corresponding block braiding in C. Hence FX is strict braided monoidal.

4.1L1L2step 3.1algebra∎

Any strict braided monoidal functor B→C sending 1 to X must send n=1⊗n to X⊗n and each generator σi to the local braiding on the ith and (i+1)st factors. Since the σi generate every Bn, such a functor must equal FX. Therefore FX is unique.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-01Open item page →

Braided coherence is controlled by underlying braids

Statement

Let C be a braided monoidal category and let X be an object of C. Each formal canonical composite on X⊗n built from associators, unitors, braidings, and their inverses has an underlying braid in Bn. If two such formal composites have equal underlying braids, then their interpreted morphisms in C are equal. Different formal braids may, of course, have the same interpretation in a particular braided category.

Facts & Assumptions

Given: A braided monoidal category C, an object X∈C, and two canonical braided endomorphisms of X⊗n.

[L1]

Every braided monoidal category is braided-monoidally equivalent to a strict braided one (Every braided monoidal category is monoidally equivalent to a strict braided one).

[L2]

The braid category is the free strict braided monoidal category on one generator (The braid category is the free strict braided monoidal category on one generator).

[L3]

A braided monoidal functor preserves canonical composites built from the braiding and tensor structure (Braided monoidal functor).

Proof

technique · direct
1.1L1givenchoose

By [L1], replace the given braided monoidal category by a braided-monoidally equivalent strict one. Equality may be checked there because an equivalence is faithful on morphisms.

2.1L2step 1.1construct

In the strict model, every formal canonical endomorphism of X⊗n is built only from the local braidings of adjacent copies of X, together with identities, tensoring, and composition. Reading those local crossings before interpretation gives a braid word and hence an element of Bn. By [L2], interpreting the formal composite is exactly applying the unique strict braided monoidal functor from the braid category that sends the generating object to X.

3.1L3step 1.1step 2.1algebra∎

If the two formal canonical composites have the same underlying braid, then step 2.1 identifies their interpretations as the images of the same morphism in the free braid category under the same braided functor. Hence they are equal in the strict model, and therefore equal in the original braided category by step 1.1 and [L3].

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

Two canonical braided composites agree exactly when their underlying braids agree

Statement

For a fixed object X and a fixed tensor power X⊗n, two canonical braided endomorphisms of X⊗n agree in every braided monoidal category if and only if their underlying braids are equal in Bn.

Facts & Assumptions

Given: Two canonical braided endomorphisms of the same tensor power X⊗n.

[L1]

Canonical braided endomorphisms of a fixed tensor power with the same underlying braid are equal (Braided coherence is controlled by underlying braids).

[L2]

The braid category realizes braid-group elements as actual canonical braided morphisms (The braid category).

Proof

technique · direct
1.1L1given

If the two underlying braids are equal, then [L1] says the two canonical composites agree in every braided monoidal category.

2.1L2step 1.1algebra

Conversely, suppose the two canonical composites agree in every braided monoidal category. Apply this to the braid category from [L2]. There the canonical composites are literally the corresponding braids, so equality of the composites forces equality of the underlying braids.

3.1step 1.1step 2.1∎

Therefore the two universal statements are equivalent.

RemarkRemark: AI-adaptedProof: Not applicableaudited 2026-09-01Open item page →

The symmetric and braided coherence theorems compare S_n with B_n

Remark

Symmetric coherence says that canonical symmetric composites are governed by permutations, hence by Sn. The braided analogue Braided coherence is controlled by underlying braids replaces those permutations by braids, hence by Bn. The quotient map of The braid group surjects onto the symmetric group is exactly the formal operation of imposing σi2=1, which is why the symmetric theorem is stronger: forgetting the pure-braid kernel is what turns many distinct braided composites into one permutation class.

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

Monoid objects in a braided monoidal category form a monoidal category

Statement

Let (C,⊗,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⊗B, unit ηA⊗ηB, and multiplication

μA⊗B=(μA⊗μB)∘(1A⊗cB,A⊗1B),

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⊗B the multiplication and unit displayed in the statement. The formula is typed because 1A⊗cB,A⊗1B rewrites A⊗B⊗A⊗B as A⊗A⊗B⊗B, after which μA⊗μB lands in A⊗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⊗B is again a monoid object.

3.1L1L2F1step 2.1algebra∎

If f:A→A′ and g:B→B′ are monoid morphisms, then f⊗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.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-01Open item page →

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

Statement

If C is a symmetric monoidal category, then Mon⁡(C) is symmetric monoidal under the tensor product of Monoid objects in a braided monoidal category form a monoidal category.

Facts & Assumptions

Given: A symmetric monoidal category C.

[L1]

A symmetric monoidal category is, in particular, braided (Symmetric monoidal category).

[L2]

In a braided monoidal category, monoid objects form a monoidal category under the braided tensor product (Monoid objects in a braided monoidal category form a monoidal category).

Proof

technique · direct
1.1L1L2given

By [L1] and [L2], Mon⁡(C) is already a monoidal category.

2.1L1L2step 1.1algebra∎

The ambient symmetry cA,B:A⊗B→B⊗A is a monoid morphism between the tensor-product monoids because the symmetry is involutive and natural, so it commutes with the braided interchange formula defining multiplication. Its square is the identity because it already is in C. Therefore these maps provide a symmetric braiding on Mon⁡(C).

5 · Examples, counterexamples and false statements

CounterexampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

The braid category is braided but not symmetric

Statement refuted

Every braided monoidal category is symmetric.

Facts & Assumptions

Given: The braid category B.

[L1]

The braid category is braided monoidal by construction (The braid category).

[L2]

The group B2 is infinite cyclic, generated by σ1 (The two-strand braid group is infinite cyclic).

Counterexample

technique · direct
1.1givenL1algebra

By [L1], B is a braided monoidal category. Its braiding on the generating object 1⊗1=2 is the crossing braid σ1∈B2.

2.1L2step 1.1algebra

By [L2], σ1 has infinite order, so in particular σ12≠12. Therefore the square of the braiding on 1⊗1 is not the identity.

3.1step 2.1algebra∎

A symmetric braiding must square to the identity on every tensor product. Step 2.1 shows that this fails in B, so B is braided but not symmetric.

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

FALSE: every diagram built from the associator and the braiding commutes

Statement

False claim: in every braided monoidal category, every diagram whose edges are built only from associators, unitors, braidings, and their inverses commutes.

Facts & Assumptions

Given: The failure theorem for braided coherence in the symmetric form.

[L1]

There is a braided monoidal category with pairwise distinct canonical endomorphisms 1,cX,X2,cX,X4,… of one tensor square (Braided coherence fails in the symmetric form).

Refutation

technique · direct
1.1givenassume-contra

If the displayed claim were true, then any two canonical endomorphisms of the same tensor word built from associators and braidings would agree.

2.1L1step 1.1contradiction

The morphisms 1,cX,X2,cX,X4,… from [L1] are all such canonical endomorphisms of X⊗X, yet [L1] says they are pairwise distinct in a specific braided monoidal category. This contradicts step 1.1.

3.1step 2.1discharge-contradiction∎

Therefore the claim is false.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

FALSE: every braided monoidal category is equivalent to a strict commutative one

Statement

False claim: every braided monoidal category is braided-monoidally equivalent to a strict braided monoidal category whose braiding is the identity on every tensor product.

Facts & Assumptions

Given: The braid category and strict braided strictification.

[L1]

The braid category is braided but not symmetric (The braid category is braided but not symmetric).

[L2]

Every braided monoidal category is braided-monoidally equivalent to some strict braided monoidal category (Every braided monoidal category is monoidally equivalent to a strict braided one).

Refutation

technique · direct
1.1L1givenassume-contra

Apply the claim to the braid category from [L1]. Then there would exist a braided monoidal equivalence from B to a strict braided category D whose braiding is the identity.

2.1L2step 1.1algebra

A strict braided category with identity braiding is symmetric, because its braiding certainly squares to the identity. Transporting that symmetric structure back across the supposed braided equivalence would make B symmetric as well.

3.1L1step 2.1discharge-contradiction∎

Step 2.1 contradicts [L1], which says the braid category is not symmetric. Therefore the claim is false.

Sources