Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Products in double categories, revisited

Evan Patterson

Abstract

Products in double categories, as found in cartesian double categories, are an elegant concept with numerous applications, yet also have a few puzzling aspects. In this paper, we revisit double-categorical products from an unbiased perspective, following up an original idea by Paré to employ a double-categorical analogue of the family construction, or free product completion. Defined in this way, double categories with finite products are strictly more expressive than cartesian double categories, while being governed by a single universal property that is no more difficult to work with. We develop the basic theory and examples of such products and, by duality, of coproducts in double categories. As an application, we introduce finite-product double theories, a categorification of finite-product theories that extends recent work by Lambert and the author on cartesian double theories, and we construct the virtual double category of models of a finite-product double theory.

Products in double categories, revisited

Abstract

Products in double categories, as found in cartesian double categories, are an elegant concept with numerous applications, yet also have a few puzzling aspects. In this paper, we revisit double-categorical products from an unbiased perspective, following up an original idea by Paré to employ a double-categorical analogue of the family construction, or free product completion. Defined in this way, double categories with finite products are strictly more expressive than cartesian double categories, while being governed by a single universal property that is no more difficult to work with. We develop the basic theory and examples of such products and, by duality, of coproducts in double categories. As an application, we introduce finite-product double theories, a categorification of finite-product theories that extends recent work by Lambert and the author on cartesian double theories, and we construct the virtual double category of models of a finite-product double theory.
Paper Structure (13 sections, 35 theorems, 139 equations)

This paper contains 13 sections, 35 theorems, 139 equations.

Table of Contents

  1. Introduction
  2. Conventions
  3. Acknowledgments
  4. Review of the family construction
  5. The family construction for double categories
  6. Coproducts in double categories
  7. Functors between double categories with coproducts
  8. Lax products in double categories
  9. Iso-strong products in double categories
  10. Restrictions in double categories with products
  11. Lax functors between double categories with products
  12. Finite-product double theories
  13. Higher morphisms and double categories of models

Key Result

proposition 2

A category $\mathsf{C}$ has all (small) coproducts if and only if the functor $\Delta: \mathsf{C} \to \mathsf{Fam}(\mathsf{C})$ has a left adjoint:

Theorems & Definitions (85)

  • proposition 2: Coproducts as left adjoints
  • proof
  • proposition 3: Coproduct-preserving functors
  • proof
  • theorem 4: Free coproduct completion
  • proof
  • example 5: Spans of categories
  • proposition 8: Families of spans
  • proof
  • corollary 9
  • ...and 75 more