pith. sign in

arxiv: 2605.03113 · v1 · submitted 2026-05-04 · 🧮 math.CO · math.CT· math.QA

Linearly distributive coherence in the absence of units

Max Demirdilek , Christian Reiher , Christoph Schweigert This is my paper

Pith reviewed 2026-05-08 17:45 UTC · model grok-4.3

classification 🧮 math.CO math.CTmath.QA
keywords linearly distributive categoriescoherenceassociahedramultiplihedradistributorsFrobenius functorstensor productsstructural isomorphisms
0
0 comments X

The pith

Linearly distributive categories without units are coherent.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that linearly distributive categories, equipped with two tensor products and non-invertible distributors relating them, satisfy coherence when units are absent: every pair of morphisms built from associators and distributors with the same source and target must be equal. This matters because it guarantees that all diagrams formed from these structural maps commute, so proofs no longer require separate verification of each composite equality. The same coherence is shown for Frobenius linearly distributive functors lacking units. The argument proceeds by translating the categorical statement into an equivalent claim about directed paths in associahedra and multiplihedra.

Core claim

Coherence in a monoidal category asserts that all morphisms built from structural isomorphisms with a fixed source and target coincide. Linearly distributive categories carry two tensor products, with structural morphisms given by associators and distributors relating the two tensor products. In several examples, including Grothendieck--Verdier categories, also known as *-autonomous categories, these distributors need not be invertible. We give a self-contained proof that linearly distributive categories without units are coherent, while units may obstruct coherence. With the same techniques, we also establish an analogous coherence result for Frobenius linearly distributive functors without

What carries the argument

Reformulation of coherence as equality of all directed paths between given vertices in associahedra and multiplihedra.

If this is right

  • All diagrams composed solely of associators and distributors commute in linearly distributive categories without units.
  • The identical coherence statement holds for Frobenius linearly distributive functors that lack units.
  • Coherence reduces to showing that every pair of directed paths in the associahedron or multiplihedron between matching vertices are equal.
  • The combinatorial path description supplies an explicit criterion that can be checked without enumerating all possible composites.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The specific obstructions that units introduce could be isolated and classified in a follow-up analysis.
  • The path reformulation may transfer to coherence questions for other two-tensor structures whose diagrams admit polyhedral models.
  • Categories arising in linear logic without unit objects would inherit automatic commutation of all structural diagrams.

Load-bearing premise

The categories and functors are strictly without units, because the paper notes that units can create obstructions to coherence.

What would settle it

A linearly distributive category without units in which two distinct morphisms built only from associators and distributors share the same source and target.

Figures

Figures reproduced from arXiv: 2605.03113 by Christian Reiher, Christoph Schweigert, Max Demirdilek.

Figure 1.1
Figure 1.1. Figure 1.1: The graph of multiplication for the string of elements a, b, c, d in an associative monoid. Each such graph is connected; hence finite products are independent of the bracketing. 1.1. Monoidal categories. A monoidal category C comes equipped with a tensor product b : C ˆ C ÝÑ C . (1.1) Associativity is not imposed as equality but via isomorphisms αA,B,C : A b pB b Cq ÝÝÑÐÝÝ pA b Bq b C : α ´1 A,B,C , (1.… view at source ↗
Figure 1.2
Figure 1.2. Figure 1.2: The pentagon diagram for a string of objects A, B, C, D in a monoidal category. In a monoidal category, one requires that, for any string of four objects, this diagram commutes in the following sense: the composites of morphisms corresponding to any two parallel directed paths coincide. Two paths are parallel if they have the same initial and terminal vertices. It suffices to impose this condition for a … view at source ↗
Figure 1.3
Figure 1.3. Figure 1.3: A pentagon involving distributors; see Diagram (P6). view at source ↗
Figure 1.4
Figure 1.4. Figure 1.4: The directed associahedron for the unbracketed expression A & B b C b D & E. Our original motivation for studying the coherence of linearly distributive categories and their functors comes from the surface-diagrammatic calculus developed in [DS25]. The coher￾ence theorems simplify computations in this calculus. For example, one of our main results (Theorem 5.7) implies that any two surface diagrams with … view at source ↗
Figure 1.5
Figure 1.5. Figure 1.5: The hexagon diagram for a string of objects A, B, C in a monoidal category C and a strong monoidal functor F : C Ñ D. Coherence for these functors asserts that all parallel morphisms built from µ and µ ´1 , the associators of C and D, and their inverses coincide [Pow89]; see also [Eps66, MP22, GJ25]. Functorial coherence can also be phrased in terms of paths on polytopes; we now explain this for the clas… view at source ↗
Figure 1.6
Figure 1.6. Figure 1.6: The directed multiplihedron for the unbracketed expression FpAq b FpBq b FpCq & FpDq. Coherence for Frobenius linearly distributive functors then asserts that any two parallel directed paths in any directed multiplihedron can be transformed by polygonal flips. The techniques developed in this article are strong enough to show such a coherence result. 1.9. Summary and main results. In the rest of this int… view at source ↗
Figure 5.1
Figure 5.1. Figure 5.1: Two natural transformations pL ˝ Rq 2 Ñ L ˝ R. To make this explicit, consider the LD category of bimodules over the three-dimensional C-algebra S :“ Crx, ys{xx 2 , y2 , xyy, with the two tensor products introduced in Example 1.1. This algebra does not admit the structure of a Frobenius algebra. In particular, the unit S of b and S ˚ of & are not isomorphic bimodules, and consequently the functors L and … view at source ↗
read the original abstract

Coherence in a monoidal category asserts that all morphisms built from structural isomorphisms with a fixed source and target coincide. These structural isomorphisms include, in particular, the associators. Linearly distributive categories carry two tensor products, with structural morphisms given by associators and distributors relating the two tensor products. In several examples, including Grothendieck--Verdier categories, also known as $\ast$-autonomous categories, these distributors need not be invertible. We give a self-contained proof that linearly distributive categories without units are coherent, while units may obstruct coherence. With the same techniques, we also establish an analogous coherence result for Frobenius linearly distributive functors without units. These results admit a reformulation in terms of directed paths in associahedra and multiplihedra.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper claims to provide a self-contained proof that linearly distributive categories without units are coherent, meaning all structural morphisms built from associators and distributors with fixed source and target coincide. It states that units may obstruct coherence. Using the same techniques, it establishes an analogous coherence result for Frobenius linearly distributive functors without units and reformulates both results in terms of directed paths in associahedra and multiplihedra.

Significance. If the central claims hold, the work is significant for coherence theory in monoidal and linearly distributive structures, particularly in non-unital settings relevant to *-autonomous categories and models of linear logic. The self-contained combinatorial proof avoids circularity with prior results, and the reformulation via directed paths in associahedra and multiplihedra provides a concrete geometric tool that strengthens the argument and may enable extensions.

minor comments (3)
  1. [Introduction] Introduction: the discussion of how units obstruct coherence would benefit from a brief concrete counterexample (even if sketched) to illustrate the distinction from the non-unital case.
  2. [Reformulation] The reformulation section: an explicit small example showing two distinct directed paths in an associahedron that are proven equal via the coherence argument would improve readability of the combinatorial equivalence.
  3. [Preliminaries] Notation: ensure consistent use of symbols for the two tensor products and the distributors throughout; a small table summarizing the structural morphisms would aid clarity.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and accurate summary of our manuscript, including the self-contained coherence proof for non-unital linearly distributive categories, the analogous result for Frobenius functors, and the reformulation via directed paths in associahedra and multiplihedra. We appreciate the recognition of the work's significance for coherence theory in non-unital settings and its potential extensions. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity; self-contained combinatorial proof

full rationale

The paper provides a direct, self-contained proof that all structural morphisms (associators and distributors) between fixed objects coincide in linearly distributive categories without units, with the same techniques yielding an analogous result for Frobenius linearly distributive functors without units. This is reformulated equivalently as directed paths in associahedra and multiplihedra, but the reformulation follows from the proof techniques rather than presupposing the result. The explicit statement that units may obstruct coherence treats their absence as a hypothesis that avoids known obstructions, not as a derived or fitted quantity. No load-bearing self-citations, self-definitional steps, or reductions of predictions to inputs appear in the argument structure; the central claim rests on combinatorial verification from the category axioms.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the standard definition of linearly distributive categories (two tensor products, associators, and distributors) and the combinatorial model of paths; no free parameters or invented entities are introduced.

axioms (1)
  • standard math Standard axioms of category theory, including associativity of composition and the definition of monoidal and linearly distributive structures.
    The proof builds directly on these background definitions without additional ad-hoc assumptions beyond the absence of units.

pith-pipeline@v0.9.0 · 5431 in / 1221 out tokens · 20267 ms · 2026-05-08T17:45:49.095131+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

57 extracted references · 57 canonical work pages

  1. [1]

    and Chapman, J

    Altenkirch, T. and Chapman, J. and Uustalu, T. , TITLE =. Log. Methods Comput. Sci. , FJOURNAL =. 2015 , NUMBER =

    work page 2015

  2. [2]

    Allen, R. , year=. Hopf algebroids and

    work page

  3. [3]

    and Lentner, S

    Allen, R. and Lentner, S. and Schweigert, C. and Wood, S. , title =. Sel. Math., New Ser. , issn =

    work page

  4. [4]

    Blute, R. F. and Cockett, J. R. B. and Seely, R. A. G. and Trimble, T. H. , title =. J. Pure Appl. Algebra , issn =

    work page

  5. [5]

    and Drinfeld, V

    Boyarchenko, M. and Drinfeld, V. , TITLE =. Quantum Topol. , FJOURNAL =. 2013 , NUMBER =

    work page 2013

  6. [6]

    and Garner, R

    Buckley, M. and Garner, R. and Lack, S. and Street, R. , TITLE =. Math. Proc. Cambridge Philos. Soc. , FJOURNAL =. 2015 , NUMBER =

    work page 2015

  7. [7]

    , title =

    Blanco, N. , title =. 2023 , school =

    work page 2023

  8. [8]

    , title =

    Blute, R. , title =. Theor. Comput. Sci. , issn =

    work page

  9. [9]

    and Zeilberger, N

    Blanco, N. and Zeilberger, N. , title =. Proceedings of the 36th conference on mathematical foundations of programming semantics, MFPS XXXVI, virtual conference, June 2--6, 2020 , pages =. 2020 , publisher =

    work page 2020

  10. [10]

    and Laplante-Anfossi, G

    Curien, P.-L. and Laplante-Anfossi, G. , TITLE =. Cah. Topol. G\'eom. Diff\'er. Cat\'eg. , FJOURNAL =

    work page

  11. [11]

    Cockett, J. R. B. and Seely, R. A. G. , TITLE =. J. Pure Appl. Algebra , FJOURNAL =. 1997 , NUMBER =

    work page 1997

  12. [12]

    Cockett, J. R. B. and Seely, R. A. G. , title =. J. Pure Appl. Algebra , issn =

    work page

  13. [13]

    and Kesten, J

    Czenky, A. and Kesten, J. and Quinonez, A. and Walton, C. , title =. Theory Appl. Categ. , issn =

    work page

  14. [14]

    , TITLE =

    Dehornoy, P. , TITLE =. J. Pure Appl. Algebra , FJOURNAL =. 2005 , NUMBER =

    work page 2005

  15. [15]

    Demirdilek, M. , year=. A lifting theorem for. 2601.14812 , note=

    work page arXiv

  16. [16]

    Demirdilek and C

    M. Demirdilek and C. Schweigert , year=

    work page

  17. [17]

    Proof-net categories , isbn =

    Do. Proof-net categories , isbn =. 2007 , publisher =

    work page 2007

  18. [18]

    Proof-theoretical coherence , fseries =

    Do. Proof-theoretical coherence , fseries =. 2004 , publisher =

    work page 2004

  19. [19]

    and Vicary, J

    Dunn, L. and Vicary, J. , title =. Log. Methods Comput. Sci. , issn =

    work page

  20. [20]

    Epstein, D. B. A. , TITLE =. 1966 , PAGES =

    work page 1966

  21. [21]

    and Gubkin, S

    Fiedorowicz, Z. and Gubkin, S. and Vogt, R. M. , title =. Algebr. Geom. Topol. , issn =

    work page

  22. [22]

    and Laugwitz, R

    Flake, J. and Laugwitz, R. and Posur, S. , title =. Adv. Math. , issn =

    work page

  23. [23]

    , title =

    Forcey, S. , title =. Topology Appl. , issn =

    work page

  24. [24]

    and Schaumann, G

    Fuchs, J. and Schaumann, G. and Schweigert, C. and Wood, S. , title =. Quantum symmetries tensor categories, TQFTs, and vertex algebras. 2025 , publisher =

    work page 2025

  25. [25]

    and Schaumann, G

    Fuchs, J. and Schaumann, G. and Schweigert, C. and Wood, S. , title =. Adv. Math. , issn =. 2025 , language =

    work page 2025

  26. [26]

    and Schweigert, C

    Fuchs, J. and Schweigert, C. and Yang, Y. , title =. Theory Appl. Categ. , issn =

    work page

  27. [27]

    , TITLE =

    Girard, J.-Y. , TITLE =. Theoret. Comput. Sci. , FJOURNAL =. 1987 , NUMBER =

    work page 1987

  28. [28]

    and Johnson, N

    Gurski, N. and Johnson, N. , TITLE =. Compositionality , FJOURNAL =. 2025 , NUMBER =

    work page 2025

  29. [29]

    , title =

    Haiman, M. , title =. 1984 , note =

    work page 1984

  30. [30]

    and Vicary, J

    Heunen, C. and Vicary, J. , title =. 2019 , publisher =

    work page 2019

  31. [31]

    , title =

    Houston, R. , title =. 2007 , school =

    work page 2007

  32. [32]

    Hughes, D. J. D. , title =. J. Pure Appl. Algebra , issn =

    work page

  33. [33]

    and Yadav, H

    Jaklitsch, D. and Yadav, H. , title =. Int. Math. Res. Not. , issn =

    work page

  34. [34]

    , TITLE =

    Kapranov, M. , TITLE =. J. Pure Appl. Algebra , FJOURNAL =. 1993 , NUMBER =

    work page 1993

  35. [35]

    Kelly, G. M. and MacLane, S. , title =. J. Pure Appl. Algebra , issn =

    work page

  36. [36]

    Laplaza, M. L. , title =. J. Pure Appl. Algebra , issn =. 1972 , language =

    work page 1972

  37. [37]

    and Strassburger, L

    Lamarche, F. and Strassburger, L. , title =. Log. Methods Comput. Sci. , issn =

    work page

  38. [38]

    , title =

    Lewis, G. , title =. 1972 , language =

    work page 1972

  39. [39]

    and Street, R

    Lack, S. and Street, R. , TITLE =. Theory Appl. Categ. , FJOURNAL =. 2012 , PAGES =

    work page 2012

  40. [40]

    and Street, R

    Lack, S. and Street, R. , TITLE =. Adv. Math. , FJOURNAL =. 2014 , PAGES =

    work page 2014

  41. [41]

    and Winkler, T

    Lincoln, P. and Winkler, T. , title =. Theor. Comput. Sci. , issn =

    work page

  42. [42]

    and Ponto, K

    Malkiewich, C. and Ponto, K. , TITLE =. Theory Appl. Categ. , FJOURNAL =. 2022 , PAGES =

    work page 2022

  43. [43]

    and Rietsch, K

    Majid, S. and Rietsch, K. , title =. 2021 , eprint =

    work page 2021

  44. [44]

    and Woodward, C

    Ma'u, S. and Woodward, C. , title =. Compos. Math. , issn =

    work page

  45. [45]

    and Pourcelot, H

    Melani, V. and Pourcelot, H. , title =. 2026 , note =

    work page 2026

  46. [46]

    and Poliakova, D

    Pilaud, V. and Poliakova, D. , title =. Math. Ann. , issn =

    work page

  47. [47]

    Power, A. J. , TITLE =. J. Pure Appl. Algebra , FJOURNAL =. 1989 , NUMBER =

    work page 1989

  48. [48]

    Monoidal

    Rom. Monoidal. 2024 , school =

    work page 2024

  49. [49]

    and Umble, R

    Saneblidze, S. and Umble, R. , title =. Homology Homotopy Appl. , issn =

    work page

  50. [50]

    , title =

    Simpson, C. , title =. 1998 , eprint =

    work page 1998

  51. [51]

    , title =

    Stasheff, J. , title =. Trans. Am. Math. Soc. , issn =. 1963 , language =

    work page 1963

  52. [52]

    , title =

    Stasheff, J. , title =. 1970 , publisher =

    work page 1970

  53. [53]

    and Street, R

    Joyal, A. and Street, R. , title =. Adv. Math. , issn =

    work page

  54. [54]

    , TITLE =

    Szlach\'anyi, K. , TITLE =. Adv. Math. , FJOURNAL =. 2012 , NUMBER =

    work page 2012

  55. [55]

    , title =

    Tamari, D. , title =. 1951 , school =

    work page 1951

  56. [56]

    , title =

    Trimble, T. , title =. 1994 , school =

    work page 1994

  57. [57]

    , title =

    Yadav, H. , title =. Proc. Am. Math. Soc. , issn =

    work page