Zulip Chat Archive

Stream: Is there code for X?

Topic: Calculations with presheaves


view this post on Zulip Jens Hemelaer (May 29 2020 at 13:20):

Hi! I asked this in the Category Theory zulip before. I'm not very familiar with Lean.
Is there a way to calculate the Hom-sets of presheaves in Lean?
In other words, can Lean generate a list of all morphisms from F to G, where F and G are two presheaves?
Or equivalently, can Lean generate a list of natural transformations between two functors?

I'm thinking of presheaves with only a few sections, over a category that has only a few objects and morphisms (so that the set of natural transformations doesn't become too big).

view this post on Zulip Kenny Lau (May 29 2020 at 13:21):

The usage of "calculate" in mathematics and in Lean (i.e. CS) are very different. In mathematics the process does not need to be automated

view this post on Zulip Kenny Lau (May 29 2020 at 13:21):

and I suspect there is any automatic algorithm to do what you ask

view this post on Zulip Kenny Lau (May 29 2020 at 13:22):

how "calculate the morphisms from F to G" might translate into Lean is "establish an equiv between the type of morphisms from F to G and some nicer type"

view this post on Zulip Jens Hemelaer (May 29 2020 at 13:30):

Ok, thanks! I'll try to find another way.

view this post on Zulip Johan Commelin (May 29 2020 at 13:36):

@Jens Hemelaer If everything in sight is finite, then it might work

view this post on Zulip Johan Commelin (May 29 2020 at 13:36):

But otherwise, I think you have to be more precise about what you really mean

view this post on Zulip Johan Commelin (May 29 2020 at 13:37):

E.g.: can you compute all function from N\mathbb{N} to N\mathbb{N}?
(That's a baby example of sections of a presheaf.)

view this post on Zulip Jens Hemelaer (May 29 2020 at 13:47):

Yes, everything in sight is finite. For example a directed graph is a presheaf on a category with two objects and two morphisms, and in this case I would be interested in the set of graph morphisms from one graph to another. In order to make this realistic computationally, both graphs should have only very few vertices and edges (say 5 or 6).

view this post on Zulip Johan Commelin (May 29 2020 at 13:55):

Yup, such things would be possible in lean.

view this post on Zulip Kenny Lau (May 29 2020 at 13:55):

but fast it would not be

view this post on Zulip Johan Commelin (May 29 2020 at 13:56):

Yup, being fast would probably require you to consider graphs with 1 or 2 vertices (-; :oops:

view this post on Zulip Johan Commelin (May 29 2020 at 13:56):

On the other hand, if you are willing to write some tactics, you can make it fast.

view this post on Zulip Johan Commelin (May 29 2020 at 13:57):

After all, lean can also prove that 5 digit numbers are prime, and can compute the first 10 digits of pi.

view this post on Zulip Johan Commelin (May 29 2020 at 13:57):

Both require a fair amount of computation. But the computation is not done by definitional reductions.

view this post on Zulip Kenny Lau (May 29 2020 at 13:58):

compute the first 10 digits of pi

with certificates

view this post on Zulip Jens Hemelaer (May 29 2020 at 13:59):

By "slow" do you mean that it would take a lot of computation time, or that it would take a lot of time to implement?

view this post on Zulip Kenny Lau (May 29 2020 at 13:59):

the former

view this post on Zulip Kevin Buzzard (May 29 2020 at 14:48):

The kind of thing that Lean can do is to understand the definition of a morphism of presheaves, and prove theorems about Hom(F,G) even if it's uncountably infinite.

view this post on Zulip Jens Hemelaer (May 29 2020 at 16:53):

So I guess that, while it might be possible in theory, Lean is not the right tool for what I want to do.

view this post on Zulip Johan Commelin (May 29 2020 at 17:09):

To decide that, you would have to be more explicit about what you want to do

view this post on Zulip Johan Commelin (May 29 2020 at 17:10):

If you want to compute with explicit graphs, maybe not. If you want to compute with explicit presheaves, maybe yes.

view this post on Zulip Chris Hughes (May 29 2020 at 17:11):

Why is Lean bad for computing explicit graphs?

view this post on Zulip Johan Commelin (May 29 2020 at 17:19):

Because we have nothing about graphs at all, whereas other languages have huge libraries

view this post on Zulip Bhavik Mehta (May 29 2020 at 17:21):

My instinct is that presheaves might compute quite nicely in lean but I can't be sure - things with fintype seem to compute reasonably well in my experience

view this post on Zulip Jens Hemelaer (May 29 2020 at 19:31):

I'm sorry for being vague, I only know the absolute basics of theorem proving in Lean.
What I want to do is not theorem proving. I just thought I could take advantage of existing "definitions" in Lean, instead of implementing presheaves and natural transformations from scratch in e.g. Python.

To be more explicit, what I want to do is the following:

  • define a specific category C, as a list of <10 objects and <10 morphisms
  • define two presheaves F and G on them, i.e. for each presheaf and each object a short list of sections, and a function defining restriction
  • get as output of the program a list of presheaf morphisms from F to G.

I could do this by hand, but then it's easy to make mistakes.

view this post on Zulip Kevin Buzzard (May 29 2020 at 19:39):

Right. So what we have in Lean is all the machinery to make the definition, but very few algorithms to compute the answer explicitly. Instead we can prove theorems about the answer, e.g. one could prove there are infinitely many presheaves on the real numbers with its usual topology. Now one could write code to do what you want to do, and it would be an interesting exercise, but it would be harder to do than in python because for each algorithm you write, you would also have to write a formal proof that the algorithm always terminated under some specific finiteness conditions which you'd have to make precise and which would cover your use case, and furthermore that it always gave the right answer -- or at least you'd have to do this if you wanted the algorithm to output something which you wanted to know for sure was the set of morphisms. If you did this, then it would be essentially impossible to make mistakes, however it would also be some work. And there would be no guarantee that it would run quickly in Lean 3.

view this post on Zulip Johan Commelin (May 29 2020 at 19:42):

Well... you could use the existing definitions, and just write meta algorithms afterwards.

view this post on Zulip Johan Commelin (May 29 2020 at 19:42):

That way you can skip all the proofy bits

view this post on Zulip Kevin Buzzard (May 29 2020 at 19:43):

I guess here is an algorithm: assuming each set of sections is finite (of size 10, say), one could literally just define the presheaf morphisms to be the subset of the product over all UU of Hom(F(U),G(U))Hom(F(U),G(U)) consisting of those things which obeyed the presheaf axiom. Now you get an algorithm for free, but the moment you try to apply it Lean will make a set possibly of size (1010)10(10^{10})^{10} and then start going through it and printing out the elements which satisfy the axiom. But in practice Lean will never even make the set of course.

view this post on Zulip Reid Barton (May 29 2020 at 19:45):

Right, I think if you went through and added a bunch of fintype instances, you could get #eval to do the calculation in principle, but it would be slow even by "who needs algorithm design?" standards.

view this post on Zulip Reid Barton (May 29 2020 at 19:46):

What would be a lot more effective (and fun) would be to have some tactic which can spit out a SAT encoding of what it means to be a morphism of presheaves from the definitions, and then hand that to a SAT solver. However, we don't have anything like that yet.

view this post on Zulip Kevin Buzzard (May 29 2020 at 19:47):

Say XX is a top space with 1 element, and we consider two presheaves taking values in sets of size at most 5. In practice this is just two sets of size at most 5, and a morphism between them. Enumerating all morphisms between two such sets involves looking at a set of size (55)2(5^5)^2 and then picking out the elements for which the diagram commutes. Already this is presumably completely unfeasible for Lean.

view this post on Zulip Kevin Buzzard (May 29 2020 at 19:48):

These numbers like 10 in the original question will just exponentially blow up the size of the answer.

view this post on Zulip Jens Hemelaer (May 29 2020 at 20:05):

I will take a look at #eval. Yes, the presheaves should have very small size, 10 sections might already be too much.

view this post on Zulip Adam Topaz (Jun 01 2020 at 15:31):

(deleted)


Last updated: May 16 2021 at 05:21 UTC