Calculations with presheaves

Stream: Is there code for X?

[Jens Hemelaer]

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]

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]

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

[Kenny Lau]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

Yup, such things would be possible in lean.

[Kenny Lau]

but fast it would not be

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

compute the first 10 digits of pi

with certificates

[Jens Hemelaer]

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?

[Kenny Lau]

the former

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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

[Chris Hughes]

Why is Lean bad for computing explicit graphs?

[Johan Commelin]

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

[Bhavik Mehta]

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]

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]

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]

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

[Johan Commelin]

That way you can skip all the proofy bits

[Kevin Buzzard]

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]

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]

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]

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]

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

[Jens Hemelaer]

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

[Adam Topaz]

(deleted)

[Wojciech Nawrocki]

I hope it's okay to revive this thread with a related (?) question. Is there a lemma saying that limits of presheaves are computed pointwise? More specifically the product (and apologies about the less-than-minimal imports):

import Mathlib.CategoryTheory.Limits.FunctorCategory
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.Sites.Limits
import Mathlib.CategoryTheory.Closed.Cartesian

open CategoryTheory

def prod_obj {𝒞 : Type u} [Category 𝒞] (F G : 𝒞 ⥤ Type u) (C : 𝒞) :
    (F ⨯ G).obj C = (F.obj C ⨯ G.obj C) := by -- Note these are different: \X and \x
  apply?

[Adam Topaz]

It’s not equal, but canonically isomorphic

[Adam Topaz]

Use the fact that evaluation preserves limits

[Adam Topaz]

I can write up some code when I get home if needed

[Adam Topaz]

If you want something actually equal, you will have to use a bespoke limit cone

[Wojciech Nawrocki]

Ah, I was worried they might not be. I am assuming you mean docs#CategoryTheory.evaluation. Thanks!

[Wojciech Nawrocki]

For posterity,

noncomputable def prod_obj {𝒞 : Type u} [Category 𝒞] (F G : 𝒞 ⥤ Type u) (C : 𝒞) :
    (F ⨯ G).obj C ≅ (F.obj C × G.obj C) :=
  let evalC := evaluation 𝒞 (Type u) |>.obj C
  Iso.trans
    (Limits.PreservesLimitPair.iso evalC F G)
    (Limits.Types.binaryProductIso _ _)

[Adam Topaz]

Bah that’s too complicated! It should just be docs#CategoryTheory.preservesLimitIso

[Adam Topaz]

Maybe we have docs#CategoryTheory.PreservesProducts and some api?

[Adam Topaz]

Aha ok so it’s docs#CategoryTheory.Limits.PreservesProduct.iso

[Adam Topaz]

docs#CategoryTheory.Limits.PreservesBinaryProduct.iso

[Adam Topaz]

I don’t know. It’s hard doing this on mobile ;)