The category of finite sets

Stream: Is there code for X?

[Adam Topaz]

Does mathlib have something like the category of finite sets (as a category)?

[Jalex Stark]

this introduces the category_theory library
https://leanprover-community.github.io/theories/category_theory.html

[Adam Topaz]

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]

I don't think it currently exists.

[Reid Barton]

Should be easy to define using induced_category plus your favorite notion of finite set.

[Adam Topaz]

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]

Oh. There's some stuff about full subcategories. I guess that's good enough in this case.

[Adam Topaz]

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]

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]

I was thinking about this earlier today actually - might it be nicer to use bundled fintype instead?

[Adam Topaz]

Do bundled fintypes already exist in mathlib?

[Bhavik Mehta]

bundled exists already, and fintype exists already

[Adam Topaz]

Oh. I'm not familiar with bundled where is this?

[Bhavik Mehta]

import category_theory.concrete_category.bundled

open category_theory

def Fintype := bundled fintype

[Adam Topaz]

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]

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]

hmm....

[Bhavik Mehta]

Take a look at algebra.category.Group (and friends) to see examples of how to use

[Chris Hughes]

bundled fintype will be a large category right?, which might be undesirable.

[Adam Topaz]

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]

I think the other alternatives above would also give a large category

[Reid Barton]

If you want a small category you can make it out of fin.

[Reid Barton]

Functors don't have to go between categories with the same universe parameters

[Adam Topaz]

Ah ok, so it's not a restriction!

[Bhavik Mehta]

It's a restriction, but not when it comes to considering functors

[Adam Topaz]

:ping_pong: Did the category of finite sets ever make it into mathlib?

[Bhavik Mehta]

Not that I know of!

[Adam Topaz]

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).