colimits

Stream: PR reviews

[Scott Morrison]

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

[Scott Morrison]

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

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]

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

[Scott Morrison]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

(as Kevin said in the meantime)

[Scott Morrison]

Now, I think one can make this really smooth.

[Scott Morrison]

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]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Kevin Buzzard]

OK

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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]

This goal we can finally discharge directly with mul_assoc.

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Reid Barton]

I think you just do it?

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Reid Barton]

Why?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Or am I dreaming?

[Johan Commelin]

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]

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]

Yeah, that's true.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Johan Commelin]

This is cool.

[Johan Commelin]

Is the next step to build the python script?

[Johan Commelin]

Or are you going for tactics directly?

[Johan Commelin]

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]

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]

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

[Reid Barton]

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]

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

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]

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]

Thanks. I will try this out.

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

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]

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]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

What Chris said

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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.