Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Bénabou-Roubaud theorem via string diagrams

Jovana Obradović

TL;DR

This work presents a complete, graphical proof of the Bénabou–Roubaud descent theorem using string-diagram calculus for bifibrations with Beck–Chevalley. By encoding the pseudofunctorial pullbacks and adjoints as a string-diagrammatic 2-category ${\mathsf{BiFib}}_{\mathcal{C}}$, it unifies three descent-data descriptions—Eilenberg–Moore algebras ${\mathsf{EM}}_{p}(f)$, descent data ${\mathsf{Desc}}_{p}(f)$, and internal-category actions ${\mathsf{Act}}_{p}^{\mathsf{Eq}(f)}$—via explicit diagrammatic isomorphisms and a monadicity argument. The core contribution is a transparent, geometry-first proof that links the original descent and monadic viewpoints through the internal category ${\mathsf{Eq}}(f)$, providing conceptual clarity and potential applicability to dependent-type-theory semantics. The approach emphasizes coherence, explicit Beck–Chevalley data, and a minimal syntactic presentation that absorbs associativity, functoriality, and naturality into the diagrammatic language. This offers a robust alternative to purely algebraic proofs and highlights the utility of string diagrams in categorical descent theory.

Abstract

We give a complete proof of the Bénabou-Roubaud monadic descent theorem using the graphical calculus of string diagrams. Our proof links the monadic and Grothendieck's original viewpoint on descent via an internal-category-based characterization of the category of descent data, equivalent to the one of Janelidze and Tholen.

The Bénabou-Roubaud theorem via string diagrams

TL;DR

This work presents a complete, graphical proof of the Bénabou–Roubaud descent theorem using string-diagram calculus for bifibrations with Beck–Chevalley. By encoding the pseudofunctorial pullbacks and adjoints as a string-diagrammatic 2-category , it unifies three descent-data descriptions—Eilenberg–Moore algebras , descent data , and internal-category actions —via explicit diagrammatic isomorphisms and a monadicity argument. The core contribution is a transparent, geometry-first proof that links the original descent and monadic viewpoints through the internal category , providing conceptual clarity and potential applicability to dependent-type-theory semantics. The approach emphasizes coherence, explicit Beck–Chevalley data, and a minimal syntactic presentation that absorbs associativity, functoriality, and naturality into the diagrammatic language. This offers a robust alternative to purely algebraic proofs and highlights the utility of string diagrams in categorical descent theory.

Abstract

We give a complete proof of the Bénabou-Roubaud monadic descent theorem using the graphical calculus of string diagrams. Our proof links the monadic and Grothendieck's original viewpoint on descent via an internal-category-based characterization of the category of descent data, equivalent to the one of Janelidze and Tholen.
Paper Structure (14 sections, 3 theorems, 23 equations, 10 figures)

This paper contains 14 sections, 3 theorems, 23 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Conventions.
  3. Preliminaries
  4. The pseudofunctorial structure of a bifibration
  5. String diagrams in category theory
  6. The string-diagrammatic 2-category $\mathsf{BiFib}_{\mathcal{C}}$
  7. The 2-category $\mathsf{Fib}_{\mathcal{C}}$ encoding pseudofunctoriality
  8. The 2-category $\mathsf{BiFib}_{\mathcal{C}}$ encoding the full bifibrational structure
  9. The Bénabou-Roubaud theorem
  10. The three categories of descent data
  11. The Eilenberg–Moore category ${\mathsf{EM}}_p(T_f)$
  12. The category of descent data ${\mathsf{Desc}}_{p}(f)$
  13. The category ${\mathsf{Act}}_p^{\mathsf{Eq}(f)}$ of actions of the internal category ${\mathsf{Eq}(f)}$ on $p$
  14. The proof

Key Result

Lemma 1

The following equalities of string diagrams hold in ${\mathsf{Fib}}_{\mathcal{C}}$:

Figures (10)

  • Figure 2.1: An example of Poincaré duality between pasting diagrams and string diagrams: 0-cells $A$, $B$, $C$, $D$ and $E$, and the 2-cell $\alpha:f_3 f_2 f_1\Rightarrow g_2 g_1$, swap their dimension. In the string-diagram representation, $\alpha$ is given by a vertex in the plane whose input strings correspond to factors of its domain, and whose output strings correspond to the factors of its codomain; in particular, a diagram is read top-down. The 0-cells are identified with the 2-dimensional regions delimited by the strings.
  • Figure 4.2: The proof of the equality $\psi\circ \varphi={\text{id}}_{f_1^{\ast}X}$.
  • Figure 4.3: Derivation of (DD1).
  • Figure 4.4: Derivation of (DD2).
  • Figure 4.5: Derivation of (AC1).
  • ...and 5 more figures

Theorems & Definitions (15)

  • Remark 1: Fibration-first
  • Definition 1: The pseudofunctorial signature $\Sigma^{\ast}_{{\mathcal{C}}}$
  • Definition 2: The string–diagrammatic 2-category $\mathsf{Fib}_{\mathcal{C}}$
  • Remark 2
  • Lemma 1
  • proof
  • Theorem 1: $\chi$-coherence
  • proof
  • Definition 3: The full bifibrational string-diagrammatic category ${\mathsf{BiFib}}_{\mathcal{C}}$
  • Remark 3: Mate construction and Beck--Chevalley transformation in ${\mathsf{BiFib}}_{\mathcal{C}}$
  • ...and 5 more