# Zulip Chat Archive

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

#### Adam Topaz (Jun 16 2020 at 21:49):

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