| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Monoidal Categories
| Title: | Monoidal Categories |
| Author: | Eugene W. Stark (stark /at/ cs /dot/ stonybrook /dot/ edu) |
| Submission date: | 2017-05-04 |
| Abstract: | Building on the formalization of basic category theory set out in the author's previous AFP article, the present article formalizes some basic aspects of the theory of monoidal categories. Among the notions defined here are monoidal category, monoidal functor, and equivalence of monoidal categories. The main theorems formalized are MacLane's coherence theorem and the constructions of the free monoidal category and free strict monoidal category generated by a given category. The coherence theorem is proved syntactically, using a structurally recursive approach to reduction of terms that might have some novel aspects. We also give proofs of some results given by Etingof et al, which may prove useful in a formal setting. In particular, we show that the left and right unitors need not be taken as given data in the definition of monoidal category, nor does the definition of monoidal functor need to take as given a specific isomorphism expressing the preservation of the unit object. Our definitions of monoidal category and monoidal functor are stated so as to take advantage of the economy afforded by these facts. |
| Change history: | [2017-05-18]:
Integrated material from MonoidalCategory/Category3Adapter into Category3/ and deleted adapter.
(revision 015543cdd069) [2018-05-29]: Modifications required due to 'Category3' changes. Introduced notation for "in hom". (revision 8318366d4575) [2020-02-15]: Cosmetic improvements. (revision a51840d36867) |
| BibTeX: |
@article{MonoidalCategory-AFP,
author = {Eugene W. Stark},
title = {Monoidal Categories},
journal = {Archive of Formal Proofs},
month = may,
year = 2017,
note = {\url{http://isa-afp.org/entries/MonoidalCategory.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Category3 |
| Used by: | Bicategory |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |