# Zulip Chat Archive

## 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, by giving three pieces of data:`C`

are the objects of some category

(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`

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

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 `Q`

be 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`

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

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