Stream: PR reviews

Topic: colimits

Scott Morrison (Apr 01 2019 at 22:29):

I'd like to make some plans for progress on colimits.

Scott Morrison (Apr 01 2019 at 22:29):

@Kenny Lau has a PR open that provides direct limits for rings and fields, but that is disconnected from the limits library. That PR builds direct limits by first taking coproducts, and then quotienting. As was pointed out in the comments there, this construction could be generalised further --- in fact all colimits in CommRing can be constructed this way, but some of the nice properties only hold for directed/filtered colimits. There is also an alternative construction, which takes the disjoint union (i.e. the colimit of the underlying types), which only works for filtered colimits. This construction hasn't been implemented by anyone, to my knowledge.

Scott Morrison (Apr 01 2019 at 22:29):

I would eventually like to see both constructions, using the API of the limits library, all written in a way that is easy and obvious to generalise from one algebraic category to the next (and possibly eventually with tactics that do most of the busy work).

Scott Morrison (Apr 01 2019 at 22:30):

(e.g. someday someone is going to want filtered colimits of semifoobiquandles, and in the long run it shouldn't be difficult)

Scott Morrison (Apr 01 2019 at 22:30):

That all said, I'm not opposed to getting Kenny's work merged sooner rather than later, as long as we have a roadmap to eventually achieve the nicer setup.

Scott Morrison (Apr 01 2019 at 22:32):

In Kenny's PR, he wrote

It is constructed as a quotient of the free module (for the module case) or quotient of
the free commutative ring (for the ring case) instead of a quotient of the disjoint union
so as to make the operations (addition etc.) "computable".

Can someone explain to me what this means?

Scott Morrison (Apr 01 2019 at 22:41):

So... what steps are on the roadmap? To hook Kenny's existing constructions up to the limits API, I think we would aspire to

• define has_coproduct and has_coequalizer (variants of these exist in branches; we should talk to @Reid Barton about which to go with),
• start providing instances --- I'd suggest actually doing the warm-up case of SemiGrpfirst, to get the structure right, and then go back through doing the relevant bits of the algebraic hierarchy
• provide has_coequalizers CommRing, which is straightforward.
• provide has_coproducts CommRing by plugging in the already known universal properties of the free constructions.
• state directly the construction of the colimit in CommRing as a quotient of a free product,
• prove has_coproducts + has_coequalizers -> has_coproducts in generality (this exists in branches, I think, but needs updating).
• prove that in CommRing this is definitionally equal to the construction given above
• finish providing the has_coproducts CommRing instance, checking along the way that we can make it agree with the abstract construction

Scott Morrison (Apr 01 2019 at 22:41):

The other half of the roadmap is to provide the disjoint union construction.

Kevin Buzzard (Apr 01 2019 at 22:42):

One way of defining the direct limit of rings is to take the disjoint union of the rings (which is not a ring) and then quotient out by the smallest equivalence relation which relates $a$ to $f(a)$ for all morphisms $f:A\to B$ in the direct limit diagram and all $a\in A$. To add two elements $a_1$ and $a_2$ in the quotient one first rings rings $A_1$ and $A_2$ that they're in, one then randomly chooses a ring further down the structure, say $A_1\to B$ and $A_2\to B$, pushes $a_1$ and $a_2$ down to $B$ and then adds there. This involves choices.

Another way, which I think you have to use when doing general colimits, is to take the disjoint union of the rings, form the polynomial ring with coefficents in $\mathbb{Z}$ over this set, and then quotient out by the ideal generated by elements of the form $f(a)-b$ regarded as degree 1 elements in this big ring. Now one can define addition on the quotient without making choices...perhaps?

Scott Morrison (Apr 01 2019 at 22:42):

Here the work to be done is of a different nature. The main work is to take the colimit of underlying types, and equip that with the relevant algebraic structure.

Scott Morrison (Apr 01 2019 at 22:43):

(as Kevin said in the meantime)

Scott Morrison (Apr 01 2019 at 22:43):

Now, I think one can make this really smooth.

Scott Morrison (Apr 01 2019 at 22:44):

There are two steps. We need to construct operations on the colimit type (e.g. multiplication, defined as Kevin just said), and we need to check axioms.

Scott Morrison (Apr 01 2019 at 22:45):

The work of checking that the operations are well-defined, and that the axioms are satisfied, is of a quite similar nature.

Kevin Buzzard (Apr 01 2019 at 22:45):

In the disjoint union case one still has to choose a random point further down the line.

Scott Morrison (Apr 01 2019 at 22:45):

We have two elements in the disjoint union, and we are trying to show that they are equal in the quotient.

Scott Morrison (Apr 01 2019 at 22:46):

As an example, let's consider checking associativity of multiplication.

Kevin Buzzard (Apr 01 2019 at 22:46):

In the quotient ring case one just uses the usual quotient.lift or whatever it is.

Kevin Buzzard (Apr 01 2019 at 22:46):

Isn't Kenny's issue more with defining the structures than checking axioms?

Scott Morrison (Apr 01 2019 at 22:47):

@Kevin Buzzard I was starting to talk here about the disjoint union construction, which Kenny wasn't doing.

Kevin Buzzard (Apr 01 2019 at 22:47):

So what I think he must not like is defining addition on the quotient.

Scott Morrison (Apr 01 2019 at 22:47):

So yes, he wasn't dealing with the issue I'm talking about now.

OK

Scott Morrison (Apr 01 2019 at 22:48):

Say we have a = (x, a_x), b = (y, b_y), z = (z, b_z). (The first element of the pair is the point in the colimit, then the second element is an element of the ring at that point.)

Scott Morrison (Apr 01 2019 at 22:49):

We're trying to prove (a*b)*c = a*(b*c).

Scott Morrison (Apr 01 2019 at 22:49):

But the chosen representatives of these multiplications sit in different pieces of the disjoint union.

Scott Morrison (Apr 01 2019 at 22:50):

So certainly we need to go to _some_ higher point in the colimit. But it's not enough to just go to some point higher than those two points.

Scott Morrison (Apr 01 2019 at 22:51):

say (a*b) was sitting over some point p, b*c was sitting over q, and (a*b)*c) sits over r, while a*(b*c) sits over s.

Scott Morrison (Apr 01 2019 at 22:52):

We now have this big messy diagram, with points x y z p q r s, and we want to use the fact that there is a cocone for that diagram, and pass to that point before trying to prove (a*b)*c = a*(b*c).

Scott Morrison (Apr 01 2019 at 22:55):

So what do we do? We identify that cocone point, called it w, and maps from each of x y z p q r s to w. We then say that we're going to proving the equality (a*b)*c = a*(b*c) by doing it over the point w, and then by repeating using the axiom that w really is a cone point, and that all the morphisms in sight are ring homomorphisms, we see this reduces to the equation (f(a_x)*g(b_y))*h(c_z) = f(a_x)*(g(b_y)*h(c_z)), where f g h are the morphisms from x y z respectively to w.

Scott Morrison (Apr 01 2019 at 22:55):

This goal we can finally discharge directly with mul_assoc.

Scott Morrison (Apr 01 2019 at 22:58):

This whole argument should in the first instance be written in a way so that it's completely clear that it was generic --- it barely mattered that we were proving multiplicative associativity rather than distributivity, the argument is always the same.

Scott Morrison (Apr 01 2019 at 22:58):

Later, we can write some tactics (like pi_instance) that do this work for us.

Scott Morrison (Apr 01 2019 at 23:00):

I think we may also want a tactic that "builds diagrams" for us, out of a collection of objects and morphisms in the local hypotheses. This would enable us to write a tactic that says "check that the goal is an equality in a colimit type; check the local environment for objects and morphisms in the indexing category, and build the cocone over all of them; now attempt to prove the equality by passing to the cocone point".

Scott Morrison (Apr 01 2019 at 23:03):

@Reid Barton, @Johan Commelin, @Kevin Buzzard, @Kenny Lau, I'd love to hear what you guys think of this plan!

Kevin Buzzard (Apr 02 2019 at 05:32):

I don't really understand what can be done with tactics but it sounds like a tactic can be used to generate this proof

Johan Commelin (Apr 02 2019 at 06:04):

I think this is really cool. There is just one uncomfortable feeling that is nagging at me: So far we haven't really been able to apply the category lib in other parts of the library. I don't know exactly why that is. But I'd first like to make sure that it is not because of some DTT/Lean issue that we aren't aware of. If it is one of those things that mathematicians handle transparently and aren't even aware of, but Lean gets hung up about, then we are doomed...

Johan Commelin (Apr 02 2019 at 06:05):

If it is only because category_theory/ is considered "high-level" and we don't want those imports in "lower-level" parts of the library, then we have some sort of social problem.

Kevin Buzzard (Apr 02 2019 at 06:23):

In practice I have an actual bunch of rings in the sense that they're types X i with [ring X i] and I want to take their actual direct limit and prove it's a ring and have access to the universal property, all by magic.

Reid Barton (Apr 02 2019 at 16:40):

I think the simplest/Lean-iest way to do these in general is: First, construct the colimit of an arbitrary diagram of (say) rings, as the quotient of an inductive type by an inductive proposition. Then check that when the input diagram is filtered, the object we built also has the following properties:

• Every element of the underlying inductive type is in the image of the map from one of the rings of the diagram.
• Every pair of elements of the original rings which become equal in the colimit (after forming the quotient) already become equal at some point in the diagram.

Both of these are easy inductions: the point is that each constructor of the inductive type and the inductive proposition is built from only finitely many smaller terms, so we can pass to a point in the diagram where the statement we are proving holds for all of them.

Once we check these two properties, then we can conclude by a general lemma that the colimit is isomorphic to the "disjoint union mod identifying elements with their images" construction, or that the colimit is preserved by the forgetful functor to sets, or whatever exact statement of that we want.

Johan Commelin (Apr 02 2019 at 16:42):

And can we provide easy glue with unbundled (say) rings? So that if you have X : I → Type and [\for i, ring (X i)], you can easily build a diagram in Ring?

Johan Commelin (Apr 02 2019 at 16:43):

Because otherwise we have a nice and abstract machine, but it becomes a pain to use in the rest of mathlib

Reid Barton (Apr 02 2019 at 16:43):

I think you just do it?

Johan Commelin (Apr 02 2019 at 16:44):

It shouldn't take more than half a line... and we want this for all bundled categories, I guess.

Johan Commelin (Apr 02 2019 at 16:44):

And we want it for indexed families, but also for single objects, and maybe other thingies?

Reid Barton (Apr 02 2019 at 16:50):

mk_ob makes a type with a ring instance into an object of Ring

Reid Barton (Apr 02 2019 at 16:50):

for a functor, obviously you'd have to provide all the fields: action on objects, action on morphisms, identity and composition laws; so it would be a little longer

Reid Barton (Apr 02 2019 at 16:50):

Ideally, you would be in a situation where you already have a functor

Johan Commelin (Apr 02 2019 at 16:51):

Yeah, but in the rest of mathlib you aren't in that ideal situation.

Johan Commelin (Apr 02 2019 at 16:52):

So mk_ob is good. We'll need similar things for the categories that are quasi-bundled. (Like CommRing, which doesn't use the machinery, even though it is an obvious candidate.)

Reid Barton (Apr 02 2019 at 16:55):

Yes, I suggest making CommRing.mk_ob, etc., which also helps Lean understand what category it's supposed to produce an object of--I'm not confident mk_ob would work in most cases without a type ascription

Johan Commelin (Apr 02 2019 at 17:03):

Can we replace bundled and concrete_category with some meta stuff that rolls all these categories for us?

Why?

Johan Commelin (Apr 02 2019 at 17:04):

It could also create a bunch of forgetful functors corresponding to classes that extend each other.

Johan Commelin (Apr 02 2019 at 17:04):

Because then we will have Ring.mk_ob and Group.mk_ob etc...

Johan Commelin (Apr 02 2019 at 17:05):

You can generate better code if you use some meta stuff.

Johan Commelin (Apr 02 2019 at 17:05):

Or am I dreaming?

Johan Commelin (Apr 02 2019 at 17:18):

Sadly something like this doesn't work either

import category_theory.instances.rings

universes u
variables {R : Type u} [ring R]

open category_theory category_theory.instances

@[reducible] def categorify : Type u → Type u := λ X, X

@[unify] def mk_Ring (X : Ring.{u}) : unification_hint :=
{ pattern := categorify R ≟ X.α,
constraints := [X ≟ mk_ob R] }


Reid Barton (Apr 02 2019 at 17:19):

I think that is trying to solve a problem we don't have yet. It's not hard to write such things by hand for now.

Johan Commelin (Apr 02 2019 at 17:24):

Yeah, that's true.

Scott Morrison (Apr 03 2019 at 00:34):

This sounds great, thanks @Reid Barton. So --- where do we start, and in particular what happens to #754?

Scott Morrison (Apr 03 2019 at 00:35):

It seems like the very first step is seeing if we can repackage Kenny's work into providing has_colimits CommRing.

Scott Morrison (Apr 03 2019 at 00:36):

It would have to be generalised, because we want it to construct arbitrary colimits, not just direct limits.

Scott Morrison (Apr 03 2019 at 00:36):

It would be nice if his construction of the colimit more obviously did so "as the quotient of an inductive type by an inductive proposition".

Scott Morrison (Apr 03 2019 at 12:08):

Okay, I just followed @Reid Barton's suggestions for implementing colimits (just the first half of the recipe, nothing about filtered colimits and disjoint unions yet), and did the special case of monoids.

Scott Morrison (Apr 03 2019 at 12:10):

https://github.com/leanprover-community/mathlib/blob/colimits/src/algebra/colimits.lean

Scott Morrison (Apr 03 2019 at 12:10):

I was very carefully to never ever think about monoids, however.

Scott Morrison (Apr 03 2019 at 12:11):

I claim that you could pipe #print monoid into a python script that would produce that file.

Scott Morrison (Apr 03 2019 at 12:11):

And if you piped #print comm_ring into the same script you'd end up with has_colimits CommRing.

Scott Morrison (Apr 03 2019 at 12:12):

(Well, ... maybe that's slightly optimistic. But pretty close!)

Scott Morrison (Apr 03 2019 at 12:13):

The proofs could be compressed a lot with some automation. (And that each such compression would make the python script for other algebraic structures easier to implement.)

Scott Morrison (Apr 03 2019 at 12:13):

It was all very pleasantly "downhill". You just do the obvious thing at every step.

Scott Morrison (Apr 03 2019 at 12:17):

On the other hand, the construction you get is absolutely awful. It looks nothing like a free monoid.

This is cool.

Johan Commelin (Apr 03 2019 at 12:23):

Is the next step to build the python script?

Johan Commelin (Apr 03 2019 at 12:24):

Or are you going for tactics directly?

Johan Commelin (Apr 03 2019 at 12:24):

I expressed a related sentiment/dream yesterday:

Can we replace bundled and concrete_category with some meta stuff that rolls all these categories for us?

https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/colimits/near/162353820

Scott Morrison (Apr 03 2019 at 12:34):

I think the next step if to wait until Reid has a chance to say if this is what he had in mind! If it is, then some tactics to cleanup, then attempting to do another example by hand, then ... asking Keeley if he knows a trick for defining new inductive types in commands. :-)

Kevin Buzzard (Apr 03 2019 at 13:15):

I once wrote python code which produced Lean code: https://xenaproject.wordpress.com/2018/07/26/617-is-prime/

Reid Barton (Apr 03 2019 at 15:21):

It might be better to add constructors making relation an equivalence relation and using quotient instead of quot, particularly for the part about filtered colimits. (To handle the infinitary case correctly you actually need to do this, though I guess it doesn't matter in the finitary case.)

Scott Morrison (Apr 03 2019 at 19:24):

@Reid Barton could you briefly explain why? I was a bit worried about this, but it seemed to just be adding more cases to the proofs to use quotient.

Reid Barton (Apr 03 2019 at 19:45):

Suppose you have an infinitary operation f and you want to prove x1 ~ y1, x2 ~ y2, ... implies f(x1, x2, ...) ~ f(y1, y2, ...). You cannot conclude this from the fact that f preserves ~ in each argument separately.

Reid Barton (Apr 03 2019 at 19:48):

To put it another way, say you form relation' by adding refl, symm, trans constructors to relation. Then in the infinitary case, relation' is bigger than the equivalence relation generated by relation. relation' is the correct one to use. If you quotient by the equivalence relation generated by relation, then you will not be able to define the operations on the quotient.

Scott Morrison (Apr 03 2019 at 20:47):

Thanks. I will try this out.

Scott Morrison (Apr 03 2019 at 20:48):

How do you feel about the objection that "this colimit is ugly", because it's not the nice one for monoids that a human would produce (words)?

Scott Morrison (Apr 03 2019 at 20:48):

Of course you can use the colimit API, so in some sense you have everything.

Scott Morrison (Apr 03 2019 at 20:48):

But I worry that implementing this generic approach widely is just going to leave us with the desire to build concrete models in many cases anyway.

Scott Morrison (Apr 03 2019 at 20:50):

Does having the "ugly" colimit make it easier to build these concrete models? (Perhaps after setting up the "filtered colimit as disjoint union" machinery?)

Kevin Buzzard (Apr 03 2019 at 20:51):

Kenny defined powers x for x in a ring, as {x^n : n in nat}. This was in the middle of a bunch of monoidy stuff in his localisation work. I asked him recently why he didn't just define it to be the monoid generated by x. He said that this was a pain to work with (the monoid generated by x is some inductive prop-- if a and b are in then a*b is in etc) and that in practice it was much easier to just use the concrete definition rather than having to prove it and rewrite the proof all the time.

Scott Morrison (Apr 03 2019 at 21:02):

My suspicion is that you can have your cake and eat it too. I don't know what "rewrite the proof all the time" could mean --- you prove the monoid generated by a singleton is powers x once, in the file about free monoids. But you should make sure to express the universal properties of powers x using a uniform API for universal properties (i.e. adjunctions, limits, etc), rather than writing them as stray lemmas.

Kevin Buzzard (Apr 03 2019 at 21:22):

He wanted to write <2,rfl> and <1,rfl> and <0,rfl> in term mode rather than having to rewrite the proof that he wrote once, lots of times.

Scott Morrison (Apr 03 2019 at 21:30):

Sorry, not sure what that means. Perhaps we can get him to show the example sometime.

Chris Hughes (Apr 03 2019 at 21:34):

He can write <2,rfl> instead of proof_of_equivalence.2 <2,rfl>

Kevin Buzzard (Apr 03 2019 at 21:34):

He constantly wanted to prove things like "1 in powers x" or "x^2 in powers x" and he could prove them very easily from his definition, the proof that x^2 is in powers x is <2,rfl>. Sometimes he wanted to prove that x^(m+n) was in powers x and his proof was <m+n,rfl>. He found it easier to work with. With powers x = {y : exists n, x^ n = y} he would have to rewrite every time

What Chris said

Kevin Buzzard (Apr 03 2019 at 21:35):

he decided that the benefits outweighed the disadvantages on this particular occasion.

Kevin Buzzard (Apr 03 2019 at 21:35):

It's a subtle business. It's all about your use case, probably.

Chris Hughes (Apr 03 2019 at 21:41):

I don't think it depends on your use case. You still have all the constructors and recursors for powers as you have with the closure definition, as lemmas. But lemma won't give you anonymous constructor notation unfortunately, it needs to be an actual constructor for that.

Last updated: May 06 2021 at 11:23 UTC