Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unbiasing symmetric monoidal categories in Lean

Robin Carlier

TL;DR

A formalization in Lean 4 of the unbiasing process for symmetric monoidal categories is presented by extending the data of a symmetric monoidal category to a Cat-valued pseudofunctor from the (2,1)-category of spans of finite sets, encoding tensor products of higher arities and their coherences.

Abstract

We present a formalization in Lean 4, within the framework of the mathematical library Mathlib, of the unbiasing process for symmetric monoidal categories. This is realized by extending the data of a symmetric monoidal category to a Cat-valued pseudofunctor from the (2,1)-category of spans of finite sets, encoding tensor products of higher arities and their coherences. The construction relies on a formalization of Mac Lane's coherence theorem using Piceghello's presentation of free symmetric monoidal categories as symmetric lists, and uses an encoding of universal formulas via an appropriate Kleisli bicategory.

Unbiasing symmetric monoidal categories in Lean

TL;DR

A formalization in Lean 4 of the unbiasing process for symmetric monoidal categories is presented by extending the data of a symmetric monoidal category to a Cat-valued pseudofunctor from the (2,1)-category of spans of finite sets, encoding tensor products of higher arities and their coherences.

Abstract

We present a formalization in Lean 4, within the framework of the mathematical library Mathlib, of the unbiasing process for symmetric monoidal categories. This is realized by extending the data of a symmetric monoidal category to a Cat-valued pseudofunctor from the (2,1)-category of spans of finite sets, encoding tensor products of higher arities and their coherences. The construction relies on a formalization of Mac Lane's coherence theorem using Piceghello's presentation of free symmetric monoidal categories as symmetric lists, and uses an encoding of universal formulas via an appropriate Kleisli bicategory.
Paper Structure (20 sections, 13 theorems, 44 equations)

This paper contains 20 sections, 13 theorems, 44 equations.

Table of Contents

  1. Introduction
  2. The coherence theorem
  3. Symmetric lists: presenting a category via generators and relations
  4. Studying morphisms of symmetric lists
  5. Coxeter groups of type $\mathrm{A}_n$ and permutation groups
  6. Morphisms of symmetric lists and permutations
  7. From symmetric lists to the coherence theorem
  8. Free symmetric monoidal categories
  9. The symmetric monoidal structure on symmetric lists
  10. The inclusion functor and the equivalence
  11. Symmetric lists and finite types
  12. Pseudofunctors out of the pith of bicategories of spans
  13. Bicategories of spans
  14. Building pseudofunctors out of the pith of spans
  15. Packaging symmetric monoidal categories as pseudofunctors
  16. ...and 5 more sections

Key Result

Theorem 1.1

Let $\left( \mathsf{C}, \otimes_{\mathsf{C}}, \mathbb{1}_{\mathsf{C}}, \alpha^{\mathsf{C}}, \lambda^{\mathsf{C}}, \rho^{\mathsf{C}}, \beta^{\mathsf{C}}\right)$ be a symmetric monoidal category. There exists a pseudofunctor that sends a finite set $J$ to the product category $\mathsf{C}^{J}$, and sends a span \begin{tikzcd} & {A} \\ {J} && {K} \arrow["{f}"', from=1-2, to=2-1] \arro

Theorems & Definitions (29)

  • Theorem 1.1
  • Remark 1.2
  • Theorem 1.3
  • Definition 2.1
  • Remark 2.2
  • Lemma 2.3
  • Remark 2.4
  • Lemma 2.5
  • Definition 2.6
  • Theorem 2.8
  • ...and 19 more