Zulip Chat Archive

Stream: new members

Topic: Help finding some category definitions


Dean Young (Aug 31 2022 at 20:30):

Hi Folks! I'm looking to start a project on categories here at the Lean community. I was wondering if anyone could help me out with finding a few of the basic constructions... maybe you know where to look.
I'd like to be able to:
1) Create a category given a type for the objects, morphisms, etc. (or some variation of this)
2) Create the opposite category
3) Product and internal hom of categories
4) Isomorphism classes of natural transformations.
5) Simplicial C w/ for a category C
6) Full subcategory consisting of objects matching a certain condition
7) Equalizer and coequilizer of functors.

Adam Topaz (Aug 31 2022 at 21:17):

I'm happy to help bu the questions are a bit vague. Let's start with an example for 1 -- what category do you want to construct?

Adam Topaz (Aug 31 2022 at 21:18):

In general, we have an extensive category theory library as part of mathlib, available in the src/category_theory folder of mathlib.

Adam Topaz (Aug 31 2022 at 21:19):

All of the constructions you asked for are there in some form.


Last updated: Dec 20 2023 at 11:08 UTC