pith. machine review for the scientific record. sign in

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

Recognition: 3 theorem links

· Lean Theorem

Linearly distributive coherence in the absence of units

Christian Reiher, Christoph Schweigert, Max Demirdilek

Authors on Pith no claims yet

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.

Reference graph

Works this paper leans on

57 extracted references · 1 canonical work pages

  1. [1]

    and Chapman, J

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

    2015

  2. [2]

    Allen, R. , year=. Hopf algebroids and

  3. [3]

    and Lentner, S

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

  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 =

  5. [5]

    and Drinfeld, V

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

    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 =

    2015

  7. [7]

    , title =

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

    2023

  8. [8]

    , title =

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

  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 =

    2020

  10. [10]

    and Laplante-Anfossi, G

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

  11. [11]

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

    1997

  12. [12]

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

  13. [13]

    and Kesten, J

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

  14. [14]

    , TITLE =

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

    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=

  17. [17]

    Proof-net categories , isbn =

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

    2007

  18. [18]

    Proof-theoretical coherence , fseries =

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

    2004

  19. [19]

    and Vicary, J

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

  20. [20]

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

    1966

  21. [21]

    and Gubkin, S

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

  22. [22]

    and Laugwitz, R

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

  23. [23]

    , title =

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

  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 =

    2025

  25. [25]

    and Schaumann, G

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

    2025

  26. [26]

    and Schweigert, C

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

  27. [27]

    , TITLE =

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

    1987

  28. [28]

    and Johnson, N

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

    2025

  29. [29]

    , title =

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

    1984

  30. [30]

    and Vicary, J

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

    2019

  31. [31]

    , title =

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

    2007

  32. [32]

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

  33. [33]

    and Yadav, H

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

  34. [34]

    , TITLE =

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

    1993

  35. [35]

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

  36. [36]

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

    1972

  37. [37]

    and Strassburger, L

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

  38. [38]

    , title =

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

    1972

  39. [39]

    and Street, R

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

    2012

  40. [40]

    and Street, R

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

    2014

  41. [41]

    and Winkler, T

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

  42. [42]

    and Ponto, K

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

    2022

  43. [43]

    and Rietsch, K

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

    2021

  44. [44]

    and Woodward, C

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

  45. [45]

    and Pourcelot, H

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

    2026

  46. [46]

    and Poliakova, D

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

  47. [47]

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

    1989

  48. [48]

    Monoidal

    Rom. Monoidal. 2024 , school =

    2024

  49. [49]

    and Umble, R

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

  50. [50]

    , title =

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

    1998

  51. [51]

    , title =

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

    1963

  52. [52]

    , title =

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

    1970

  53. [53]

    and Street, R

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

  54. [54]

    , TITLE =

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

    2012

  55. [55]

    , title =

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

    1951

  56. [56]

    , title =

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

    1994

  57. [57]

    , title =

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