categorical quotients

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

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]

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

[Scott Morrison]

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

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

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

They fit in a commutative diagram

[Mario Carneiro]

of course, but what is it exactly?

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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]

So, there is some category lurking in the background

[Scott Morrison]

But Johan, it's not a fixed category.

[Scott Morrison]

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

[Johan Commelin]

Ok... then I'm confused

[Mario Carneiro]

C plays the role of beta in quot.lift

[Scott Morrison]

Yes.

[Johan Commelin]

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

[Johan Commelin]

Because it only lives in some cocompletion of said category

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

it's the index category for a diagram in C

[Johan Commelin]

Ok, got it

[Mario Carneiro]

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

[Mario Carneiro]

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]

Ok, I'm confused again...

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

But that is not coherent, I guess

[Mario Carneiro]

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]

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]

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.