Stream: Is there code for X?
Topic: The category of finite sets
Adam Topaz (Jun 16 2020 at 21:02):
Does mathlib have something like the category of finite sets (as a category)?
Jalex Stark (Jun 16 2020 at 21:04):
this introduces the category_theory library
Adam Topaz (Jun 16 2020 at 21:08):
Thanks, I looked at this, but the word "finite" is not mentioned there. I am aware of the "category of types" here:
I guess I'm looking for something similar where the objects are finite types.
Reid Barton (Jun 16 2020 at 21:09):
I don't think it currently exists.
Reid Barton (Jun 16 2020 at 21:14):
Should be easy to define using
induced_category plus your favorite notion of finite set.
Adam Topaz (Jun 16 2020 at 21:25):
So something like this?
import data.fintype.basic import category_theory.full_subcategory structure fin_types := (carrier : Type*) (is_fintype : fintype carrier) open category_theory -- the category of finite types def fin_type := induced_category _ fin_types.carrier
Adam Topaz (Jun 16 2020 at 21:27):
Oh. There's some stuff about full subcategories. I guess that's good enough in this case.
Adam Topaz (Jun 16 2020 at 21:32):
But this takes a predicate as an input, so I guess this is a roundabout way to make it work:
def fin_type := category_theory.full_subcategory (λ A, nonempty (fintype A))
Reid Barton (Jun 16 2020 at 21:37):
Yep, either of these will work but for the second one you will need to
fintype whenever you need it. In cases like this one where
fintype is a subsingleton, you have a full subcategory in math but in Lean it's probably better to use the first approach--you don't quite have a subcategory, instead you have a category whose "fibers" of objects are subsingletons, if that makes sense.
Bhavik Mehta (Jun 16 2020 at 21:39):
I was thinking about this earlier today actually - might it be nicer to use
bundled fintype instead?
Adam Topaz (Jun 16 2020 at 21:43):
Do bundled fintypes already exist in mathlib?
Bhavik Mehta (Jun 16 2020 at 21:43):
bundled exists already, and fintype exists already
Adam Topaz (Jun 16 2020 at 21:44):
Oh. I'm not familiar with
bundled where is this?
Bhavik Mehta (Jun 16 2020 at 21:45):
import category_theory.concrete_category.bundled open category_theory def Fintype := bundled fintype
Adam Topaz (Jun 16 2020 at 21:47):
Ah! Awesome. Yes, so I guess something like this is equivalent to the first construction:
import data.fintype.basic import category_theory.full_subcategory import category_theory.concrete_category.bundled open category_theory def FinType := induced_category _ (λ A : bundled fintype, A.1)
Bhavik Mehta (Jun 16 2020 at 21:48):
Sure, but I feel like you could just use
def Fintype := bundled fintype as the category of finite types, without using
induced_category or anything
Adam Topaz (Jun 16 2020 at 21:49):
Bhavik Mehta (Jun 16 2020 at 21:51):
Take a look at
algebra.category.Group (and friends) to see examples of how to use
Chris Hughes (Jun 16 2020 at 21:56):
bundled fintype will be a large category right?, which might be undesirable.
Adam Topaz (Jun 16 2020 at 22:00):
I think this is necessary for what I'd like to eventually do, since I will eventually need to consider the "usual embedding from the category of finite sets to sets".
Bhavik Mehta (Jun 16 2020 at 22:01):
I think the other alternatives above would also give a large category
Reid Barton (Jun 16 2020 at 22:02):
If you want a small category you can make it out of
Reid Barton (Jun 16 2020 at 22:02):
Functors don't have to go between categories with the same universe parameters
Adam Topaz (Jun 16 2020 at 22:03):
Ah ok, so it's not a restriction!
Bhavik Mehta (Jun 16 2020 at 22:04):
It's a restriction, but not when it comes to considering functors
Adam Topaz (Oct 27 2020 at 15:29):
:ping_pong: Did the category of finite sets ever make it into mathlib?
Bhavik Mehta (Oct 27 2020 at 16:31):
Not that I know of!
Adam Topaz (Oct 27 2020 at 18:26):
Okay, I sketched some code for
It's all very basic for now, but I did add the equivalence of
FinType with its skeletal version (objects indexed by nat).
Last updated: May 16 2021 at 05:21 UTC