## Stream: Is there code for X?

### Topic: Calculations with presheaves

#### 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).

#### 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

#### Kenny Lau (May 29 2020 at 13:21):

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

#### 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"

#### Jens Hemelaer (May 29 2020 at 13:30):

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

#### Johan Commelin (May 29 2020 at 13:36):

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

#### Johan Commelin (May 29 2020 at 13:36):

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

#### Johan Commelin (May 29 2020 at 13:37):

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

#### 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).

#### Johan Commelin (May 29 2020 at 13:55):

Yup, such things would be possible in lean.

#### Kenny Lau (May 29 2020 at 13:55):

but fast it would not be

#### Johan Commelin (May 29 2020 at 13:56):

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

#### 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.

#### 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.

#### Johan Commelin (May 29 2020 at 13:57):

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

#### Kenny Lau (May 29 2020 at 13:58):

compute the first 10 digits of pi

with certificates

#### 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?

the former

#### 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.

#### 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.

#### Johan Commelin (May 29 2020 at 17:09):

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

#### 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.

#### Chris Hughes (May 29 2020 at 17:11):

Why is Lean bad for computing explicit graphs?

#### Johan Commelin (May 29 2020 at 17:19):

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

#### 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

#### 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.

#### 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.

#### Johan Commelin (May 29 2020 at 19:42):

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

#### Johan Commelin (May 29 2020 at 19:42):

That way you can skip all the proofy bits

#### 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 $U$ of $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 $(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.

#### 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.

#### 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.

#### Kevin Buzzard (May 29 2020 at 19:47):

Say $X$ 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 $(5^5)^2$ and then picking out the elements for which the diagram commutes. Already this is presumably completely unfeasible for Lean.

#### 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.

#### 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.

#### Adam Topaz (Jun 01 2020 at 15:31):

(deleted)

Last updated: May 16 2021 at 05:21 UTC