Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Realization of relational presheaves

Yorgo Chamoun, Samuel Mimram

TL;DR

The work extends presheaf theory to relational presheaves valued in ${\mathcal Rel}$, introducing lax functors to capture partial and multi-boundary behaviours relevant to true concurrency. It develops a realization framework by interpreting relational presheaves as models of a cartesian theory ${\mathbb T}_{{\mathcal C}}^{\mathrm{Rel}}$ and showing cocontinuous realizations correspond to Lex-models in the opposite category, leveraging Ind- completions and left Kan extensions. The paper then demonstrates how these realizations yield a combinatorial description of the blowup operation for precubical sets, linking discrete combinatorics to directed geometric topology. Overall, relational presheaves provide a robust semantic and combinatorial toolkit for modeling and analyzing concurrency, with precise realizations connecting syntactic and geometric perspectives.

Abstract

Relational presheaves generalize traditional presheaves by going to the category of sets and relations (as opposed to sets and functions) and by allowing functors which are lax. This added generality is useful because it intuitively allows one to encode situations where we have representables without boundaries or with multiple boundaries at once. In particular, the relational generalization of precubical sets has natural application to modeling concurrency. In this article, we study categories of relational presheaves, and construct realization functors for those. We begin by observing that they form the category of set-based models of a cartesian theory, which implies in particular that they are locally finitely presentable categories. By using general results from categorical logic, we then show that the realization of such presheaves in a cocomplete category is a model of the theory in the opposite category, which allows characterizing situations in which we have a realization functor. Finally, we explain that our work has applications in the semantics of concurrency theory. The realization namely allows one to compare syntactic constructions on relational presheaves and geometric ones. Thanks to it, we are able to provide a syntactic counterpart of the blowup operation, which was recently introduced by Haucourt on directed geometric semantics, as way of turning a directed space into a manifold.

Realization of relational presheaves

TL;DR

The work extends presheaf theory to relational presheaves valued in , introducing lax functors to capture partial and multi-boundary behaviours relevant to true concurrency. It develops a realization framework by interpreting relational presheaves as models of a cartesian theory and showing cocontinuous realizations correspond to Lex-models in the opposite category, leveraging Ind- completions and left Kan extensions. The paper then demonstrates how these realizations yield a combinatorial description of the blowup operation for precubical sets, linking discrete combinatorics to directed geometric topology. Overall, relational presheaves provide a robust semantic and combinatorial toolkit for modeling and analyzing concurrency, with precise realizations connecting syntactic and geometric perspectives.

Abstract

Relational presheaves generalize traditional presheaves by going to the category of sets and relations (as opposed to sets and functions) and by allowing functors which are lax. This added generality is useful because it intuitively allows one to encode situations where we have representables without boundaries or with multiple boundaries at once. In particular, the relational generalization of precubical sets has natural application to modeling concurrency. In this article, we study categories of relational presheaves, and construct realization functors for those. We begin by observing that they form the category of set-based models of a cartesian theory, which implies in particular that they are locally finitely presentable categories. By using general results from categorical logic, we then show that the realization of such presheaves in a cocomplete category is a model of the theory in the opposite category, which allows characterizing situations in which we have a realization functor. Finally, we explain that our work has applications in the semantics of concurrency theory. The realization namely allows one to compare syntactic constructions on relational presheaves and geometric ones. Thanks to it, we are able to provide a syntactic counterpart of the blowup operation, which was recently introduced by Haucourt on directed geometric semantics, as way of turning a directed space into a manifold.

Paper Structure

This paper contains 11 sections, 3 theorems, 9 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Presheaves.
  3. Presheaves to relations.
  4. Higher dimensional automata.
  5. Relational presheaves.
  6. Realization.
  7. Blowup.
  8. Previous work.
  9. Plan of the paper.
  10. Preliminaries: some categorical logic
  11. Relational presheaves as models of a cartesian theory

Key Result

proposition thmcounterproposition

Let $\mathbb{T}$ be a cartesian theory. There is a cartesian category $\mathcal{C}_\mathbb{T}$, called the cartesian syntactic category of $\mathbb{T}$, such that there is an equivalence for every cartesian category $\mathcal{D}$, natural in $\mathcal{D}$. Moreover, $\mathcal{C}_\mathbb{T}^{op}$ is equivalent to the category of finitely presented set-based models of $\mathbb{T}$.

Figures (2)

  • Figure :
  • Figure :

Theorems & Definitions (7)

  • definition thmcounterdefinition
  • proposition thmcounterproposition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • proposition thmcounterproposition
  • proof
  • corollary thmcountercorollary