Skip to content

Mac Lane's coherence theorem

In a monoidal category, every well-formed diagram composed only of associators and left or right unitors commutes; equivalently, every monoidal category is monoidally equivalent to a strict one.

Version
v1 · 2026-09-28 · History
Domain-specific #
10513
Domain group
Formal Sciences
Origin domain
Mathematics
Subdomain
Category Theory → Mathematics

Core Idea

Mac Lane's coherence theorem makes canonical rebracketing and unit bookkeeping path-independent in monoidal categories.

Associators and unitors are genuine morphisms, so tensor expressions are not literally equal in the original category. Coherence says any two canonical composites with the same endpoints agree when generated by those structural maps.

Strictification is equivalence, not identity: calculations may be performed in a strict monoidal category without erasing the categorical distinction between equivalence and literal equality.

Structural Signature

Sig role-phrases:

  • monoidal category. Supplies objects, morphisms, tensor product, and unit. Constitutive setting. If altered: Without monoidal structure there are no relevant coherence maps.
  • associator. Naturally identifies alternative tensor bracketings. Constitutive isomorphism. If altered: Removing it destroys canonical reassociation.
  • left/right unitors. Insert or remove the tensor unit coherently. Constitutive isomorphisms. If altered: Without them unit expressions are not connected.
  • pentagon and triangle axioms. Constrain basic composites. Constitutive law. If altered: Arbitrary isomorphisms need not be path-independent.
  • canonical diagram/path. Composes only structural isomorphisms and inverses. Theorem domain. If altered: Adding arbitrary morphisms exceeds the basic statement.
  • commutativity/strictification conclusion. Establishes equality of canonical paths and strict model equivalence. Theorem output. If altered: Literal equality in the original category is not asserted for all objects.

What It Is Not

  • Not every commuting diagram. Only canonical associator/unitor diagrams are covered.
  • Not literal strictness. The original category need not be strict.
  • Not braided coherence automatically. Braiding adds generators and conditions.
  • Not a rewrite implementation. The theorem warrants normalization but is not an algorithm by itself.

Scope of Application

Mac Lane's coherence theorem applies in category theory and related work only when its carrier, rules, and evidence boundary are explicit.

  • Category theory. Controls monoidal expressions.
  • Tensor categories. Suppresses bracket bookkeeping.
  • Algebra and topology. Supports structured tensor constructions.
  • Proof formalization. Normalizes canonical composites.
  • Categorical semantics. Ensures presentation-independent interpretation.

Clarity

State the category, tensor product, unit object, associator, unitors, naturality/coherence axioms, diagram generators, source and target, and whether the conclusion is equality, unique canonical isomorphism, or equivalence. Do not extend the theorem to arbitrary arrows.

Manages Complexity

Without coherence, every change of parentheses creates a combinatorial family of composites whose equality would need separate proof. The theorem compresses that family into local axioms: pentagon and triangle imply global agreement for canonical paths. This is a permission to omit parentheses and unit bookkeeping in many arguments, but only because the suppressed isomorphisms are uniquely determined. Strictification reduces complexity further by replacing a monoidal category with a monoidally equivalent strict one; equivalence preserves the relevant categorical content while changing presentation. The gain can be abused if ordinary morphisms, braidings, dualities, or higher coherence data are smuggled into the canonical class. Proof assistants and rewriting systems also need an orientation and termination strategy even when the mathematical equality is guaranteed. Coherence therefore manages representational proliferation while keeping exact boundaries around the structural vocabulary it licenses.

Abstract Reasoning

  1. Type the monoidal objects and structural maps.
  2. Reduce each path to associator/unitor generators.
  3. Check pentagon, triangle, naturality, and endpoints.
  4. Invoke coherence only for canonical composites.
  5. Use strictification as equivalence, not identity.

Knowledge Transfer

The theorem transfers across monoidal categories because the tensor, unit, associator, and unitor roles remain literal. It does not transfer to any collection of 'consistent rearrangements' by analogy; braided, symmetric, bicategorical, and higher settings require their own coherence theorems.

Examples

Canonical

For four objects, two composites of associators carry ((A⊗B)⊗C)⊗D to A⊗(B⊗(C⊗D)); pentagon coherence makes the canonical composites equal.

Mapped back: monoidal category → declared C; associator → rebracketing arrows; left/right unitors → available structural maps; pentagon and triangle axioms → satisfied; canonical diagram/path → two associator composites; commutativity/strictification conclusion → equal morphisms.

Applied / In Practice

A tensor-category proof suppresses inserted unit objects and parentheses, with every omitted conversion reconstructible uniquely from associators and unitors before a nonstructural morphism is applied.

Mapped back: monoidal category → tensor category; associator → implicit rebracketing; left/right unitors → implicit unit removal; pentagon and triangle axioms → coherence basis; canonical diagram/path → reconstructed conversions; commutativity/strictification conclusion → presentation-independent proof step.

Structural Tensions

T1: notational freedom vs. typed rigor. Coherence removes clutter but can hide which maps are structural. Diagnostic: Can every suppressed arrow be reconstructed from associators and unitors?

T2: strict model vs. original weak structure. Strictification simplifies proof while equivalence is not literal identity. Diagnostic: Which statement is invariant under monoidal equivalence?

T3: local axioms vs. global diagrams. Few coherence laws govern indefinitely many composites. Diagnostic: Does the diagram stay inside the generated canonical class?

Structural–Framed Character

Mac Lane coherence is highly structural but formally framed. Its vocabulary travels across categorical substrates; evaluative weight and human practice are absent; temporal order is compositional; robustness holds under monoidal equivalence. Its path-independence skeleton is a future-prime candidate. Its character: local coherence axioms force global agreement of canonical tensor rebracketings.

Structural Core vs. Domain Accent

Skeletal core. Multiple formally generated paths between the same structured expressions collapse to one result under local compatibility laws.

Domain-bound accent. Monoidal categories, tensor products, natural isomorphisms, associators, unitors, pentagon, triangle, and monoidal equivalence are essential.

Why not prime. Path coherence travels, but this theorem's truth and diagnostics remain tied to categorical axioms.

  • Related — category theory. The theorem is a central result inside the field, not a kind of the field.
  • Related — equivalence. Strictification preserves monoidal content up to a specified equivalence.

Neighborhood in Abstraction Space

Mac Lane's coherence theorem sits in a crowded region of the domain-specific corpus (36th percentile for distinctiveness): several abstractions share nearly its structure, so a description that fits it tends to fit its neighbors too.

Family — Abstract Algebra & Category Theory (24 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • Strict monoidal category. Tell: Original structure strict or equivalent to a strict presentation?
  • Commutative diagram. Tell: Canonical coherence guarantee or separately proved diagram?
  • Braided coherence. Tell: Only associators/unitors or braiding as well?
  • Associativity law. Tell: Literal equality or natural isomorphism?

References

  • Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/Mac_Lane%27s_coherence_theorem (revision 1347477096).
  • Preserved source candidate: https://doi.org/10.1007/978-3-642-99902-4_22
  • Preserved source candidate: https://ncatlab.org/nlab/files/JoyalStreet-BraidedMonoidal.pdf
  • Preserved source candidate: https://hdl.handle.net/1911/62865
  • Preserved source candidate: https://nilesjohnson.net/En-monoidal.html
  • Preserved source candidate: http://eudml.org/doc/121925
  • Preserved source candidate: https://unapologetic.wordpress.com/2007/06/29/mac-lanes-coherence-theorem/
  • Preserved source candidate: https://ocw.mit.edu/courses/18-769-topics-in-lie-theory-tensor-categories-spring-2009/resources/mit18_769s09_lec03/
  • Preserved source candidate: https://ncatlab.org/nlab/show/coherence+theorem+for+monoidal+categories

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.