## 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
https://leanprover-community.github.io/theories/category_theory.html

#### 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:
https://leanprover-community.github.io/mathlib_docs/category_theory/types.html
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 choose a 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

hmm....

#### 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 fin.

#### 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 FinType here:
https://github.com/leanprover-community/mathlib/blob/FinSet/src/category_theory/FinType.lean
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