## Stream: general

### Topic: categorical quotients

#### Scott Morrison (Apr 29 2018 at 23:25):

Is everyone ready for a new puzzle about how to formalise things mathematicians use without thinking about? :-)

#### Scott Morrison (Apr 29 2018 at 23:25):

I would like to define a notion of a "categorical quotient".

#### Scott Morrison (Apr 29 2018 at 23:25):

Recall that a quotient of a type X by a relation R is a type Y, which is pretty much useless, _except_ that we can construct functions Y -> Z by giving two pieces of data:

#### Scott Morrison (Apr 29 2018 at 23:25):

1. a function f : X -> Z, and
2. a proof that R x x' -> (f x = f x').

#### Scott Morrison (Apr 29 2018 at 23:25):

I want instead a categorical quotient of a type X by a relation R, let's call it Q which is useless except that we can construct functions Q -> C, where C are the objects of some category, by giving three pieces of data:

#### Scott Morrison (Apr 29 2018 at 23:26):

1. a function f : X -> C,
2. for each R x x', an isomorphism φ x x' : f x ≅ f x', and
3. for each x x' x'' so that R x x' and R x' x'' (and so automatically R x x''), we have φ x x' composed with φ x' x'' is equal to φ x x''.

#### Scott Morrison (Apr 29 2018 at 23:26):

This says: you are only allowed to make functions out of Q that are independent of choices of representative _up to coherent isomorphisms_.

#### Scott Morrison (Apr 29 2018 at 23:26):

So --- how do I do this in Lean?

#### Scott Morrison (Apr 29 2018 at 23:26):

(The point of course is hygiene: we can sometimes help make our programs more correct by only using quotient types, when that's all that's needed. Unfortunately quotient types are a bit too restrictive for what actually happens in the real world.)

#### Scott Morrison (Apr 29 2018 at 23:26):

(And no, it not useful in this situation to merely define functions to the isomorphism classes of objects of C, which is something you could do with a plain quotient and data 1-3.)

#### Scott Morrison (Apr 29 2018 at 23:33):

(A categorical quotient is at least as good as a quotient: you can take C to be a discrete category, where the only (iso)morphisms are identities, and this recovers the usually construction of function out of a quotient.)

#### Kevin Buzzard (Apr 30 2018 at 06:58):

Is this a non-trivial problem in dependent type theory?

#### Kevin Buzzard (Apr 30 2018 at 06:58):

Is there a chance that it is not possible to define such a quotient?

#### Kevin Buzzard (Apr 30 2018 at 07:00):

Note that Scott's question is really flagging the difference between and equivalence relation, and equiv. The statement that two terms in a setoid are equivalent is a proposition. However an instance of equiv x y really is data, and to a mathematician sometimes that data really is important.

#### Mario Carneiro (Apr 30 2018 at 07:03):

There is a piece missing from the specification: what property do you get from those lift functions Q -> C?

#### Johan Commelin (Apr 30 2018 at 07:04):

They fit in a commutative diagram

#### Mario Carneiro (Apr 30 2018 at 07:06):

of course, but what is it exactly?

#### Johan Commelin (Apr 30 2018 at 07:06):

So, there is a quotient map q : X -> Q, and the map g : Q -> C that you have obtained is such that f is equal to g \circ q

#### Johan Commelin (Apr 30 2018 at 07:06):

I guess that equal does not mean defeq but only provable equality in a set of morphisms in the category

#### Mario Carneiro (Apr 30 2018 at 07:11):

What prevents the definition Q := X and lift f := f?

#### Mario Carneiro (Apr 30 2018 at 07:14):

I guess in the plain quotient case you have quot.sound : R x y -> q x = q y, so here you want sound : R x y -> q x ~= q y; then presumably transport (lift f φ) (sound (h : R x y)) = φ x y

#### Johan Commelin (Apr 30 2018 at 07:20):

Wait, so now we are merging two themes? (-;

#### Johan Commelin (Apr 30 2018 at 07:21):

But, to answer your question about Q := X. I should have added that the quotient map q should also satisfy points 2 and 3 from Scott's post.

#### Johan Commelin (Apr 30 2018 at 07:22):

So Q is the universal gadget among all the data that satisfies 1, 2, and 3

#### Johan Commelin (Apr 30 2018 at 07:23):

Also, it does not need to exist in all situations. Its existence is a theorem that has to be proven.

#### Mario Carneiro (Apr 30 2018 at 07:46):

How can its existence be conditional? It doesn't have a category as input, so either Lean can prove these things exist in general or not

#### Johan Commelin (Apr 30 2018 at 07:47):

I want instead a categorical quotient of a type X by a relation R, let's call it Q which is useless except that we can construct functions Q -> C, where C are the objects of some category, by giving three pieces of data:

(emphasis mine)

#### Johan Commelin (Apr 30 2018 at 07:47):

So, there is some category lurking in the background

#### Scott Morrison (Apr 30 2018 at 07:47):

But Johan, it's not a fixed category.

#### Scott Morrison (Apr 30 2018 at 07:47):

(I think? Maybe I'm confused about my own question. I wanted that description to hold for any category C.)

#### Johan Commelin (Apr 30 2018 at 07:47):

Ok... then I'm confused

#### Mario Carneiro (Apr 30 2018 at 07:48):

C plays the role of beta in quot.lift

Yes.

#### Johan Commelin (Apr 30 2018 at 07:49):

So, maybe Q always exists, but it is not always an object of some category

#### Johan Commelin (Apr 30 2018 at 07:49):

Because it only lives in some cocompletion of said category

#### Mario Carneiro (Apr 30 2018 at 07:49):

I don't think there is a requirement that Qbe an element of C

#### Mario Carneiro (Apr 30 2018 at 07:50):

It's just some type, with a function to the objects of C

#### Mario Carneiro (Apr 30 2018 at 07:50):

it's the index category for a diagram in C

Ok, got it

#### Mario Carneiro (Apr 30 2018 at 07:52):

Hm, there's a problem interpreting Q as a category: what are the equivs?

#### Mario Carneiro (Apr 30 2018 at 07:54):

If Q is the universal thing satisfying 1-3, then we can slot q in for f, Q for C, and sound for φ to get the properties expected of Q itself, but then this means that sound x x' : q x ~= q x' and this doesn't make any sense since q x : Q` is not a type

#### Johan Commelin (Apr 30 2018 at 07:57):

Ok, I'm confused again...

#### Johan Commelin (Apr 30 2018 at 07:57):

First I thought that Scott was trying to formalise some colimit inside some category

#### Johan Commelin (Apr 30 2018 at 07:57):

But now it seems he wants to do something more general?

#### Johan Commelin (Apr 30 2018 at 07:59):

Scott, is this an example of what you try to achieve: taking the quotient of all groups by the relation of isomorphism?

#### Johan Commelin (Apr 30 2018 at 07:59):

But that is not coherent, I guess

#### Mario Carneiro (Apr 30 2018 at 07:59):

I suspect what Scott wants to do is not possible unless you make a lot of non-canonical choices, but I await a full specification first

#### Kevin Buzzard (May 02 2018 at 17:51):

This is very much related to all this canonical stuff I'm thinking about, so I would be interested in bumping this thread. I've only seen the notion of categorical quotient in algebraic geometry, where it looks like this: https://en.wikipedia.org/wiki/Categorical_quotient

#### Kevin Buzzard (May 02 2018 at 17:54):

But here it's not just a relation on the object X you want to quotient, there is a group action. @Scott Morrison did you need something more general than this? Note that X isn't a type in the version I know, it's an object in the category.

Last updated: May 08 2021 at 05:14 UTC