Zulip Chat Archive

Stream: Is there code for X?

Topic: Sheaves of category-objects


view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:19):

I see we have algbraic-geometryand a directory topology.sheaves, but am I right in thinking that I still cannot talk about sheaves of objects of a category on a topological space? I want to put a sheaf of rings on a topological space.

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:21):

We built this in a hands-on manner in the schemes repo, without using any categories. But we now have presheaves in this generality (see PresheafedSpace), so the natural thing to do next is sheaves.

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 19:29):

-- locally ringed spaces

import tactic

import topology.basic
import algebraic_geometry.presheafed_space
import algebra.category.CommRing

open algebraic_geometry
structure ringed_space :=
(X : PresheafedSpace CommRing)
-- is a sheaf

The statement I need is that for a bunch of open sets, the canonical map from F(union) to prod_i F(U_i) is the equalizer in the category of sets of the usual two restriction maps from prod_i F(U_i) to prod_{i,j}F(U_i\cap F(U_j).

view this post on Zulip Scott Morrison (Jul 22 2020 at 23:33):

Nope we still don't have a satisfactory version of this, sorry.

view this post on Zulip Scott Morrison (Jul 22 2020 at 23:34):

I've kept intending to go back to this, but keep getting hung up on the decision "try again with the sheaf condition on a topology, or just define sites?"

view this post on Zulip Scott Morrison (Jul 22 2020 at 23:35):

There is an ancient branch called sheaves, but I've no memory of what it contains. :-)

view this post on Zulip Scott Morrison (Jul 23 2020 at 03:47):

haha, you tricked me, @Kevin Buzzard.

I made a new branch (sheaf_condition_in_Type) and started over again, aiming to prove https://stacks.math.columbia.edu/tag/0073.

It's not there yet, but hopefully downhill from here --- I think I've done all of the "maths proof", and the remaining sorries are either easy facts about cones, or about functors preserving limits.

view this post on Zulip Kevin Buzzard (Jul 23 2020 at 06:58):

I have no idea whether we actually use that tag in practice but it would not surprise me if we do

view this post on Zulip Kevin Buzzard (Jul 23 2020 at 06:59):

So the issue is "which definition gives us something we can actually prove theorems about"?

view this post on Zulip Scott Morrison (Jul 23 2020 at 07:38):

Yay, all sorries done. This was much easier than last time I tried.

view this post on Zulip Scott Morrison (Jul 23 2020 at 08:00):

So what are the next things to try out?

  1. write out the element-wise sheaf condition in Type?
  2. show that the presheaves of rings of functions on topological spaces we already have are sheaves?
  3. the gluing exercise?
  4. wonder how to do sheaves over modules (with the ring varying)?

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:12):

@Scott Morrison This is cool

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:12):

Where is the code?

view this post on Zulip Scott Morrison (Jul 23 2020 at 08:12):

sheaf_condition_in_Type

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:12):

Ok, I'll take a look right now

view this post on Zulip Scott Morrison (Jul 23 2020 at 08:13):

in src/topology/sheaves/sheaf/concrete_category.lean

view this post on Zulip Scott Morrison (Jul 23 2020 at 08:13):

it's first cut code, but should be pretty easy to golf

view this post on Zulip Scott Morrison (Jul 23 2020 at 08:13):

and seems worth commenting properly :-)

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:13):

Awww, there are no oleans yet

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:14):

I'll take those for the one-but-last commit

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:18):

@Scott Morrison I would be interested in (1), (2), (3), (4), and also

  1. Sheafification
  2. Pullback and pushforward of sheaves

view this post on Zulip Scott Morrison (Jul 23 2020 at 08:19):

yeah, sheafification would be a good goal

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:19):

  1. Stress-test the code by defining the structure sheaf on the prime spectrum

view this post on Zulip Scott Morrison (Jul 23 2020 at 08:19):

via plus construction?

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:19):

Probably, yes

view this post on Zulip Johan Commelin (Jul 23 2020 at 08:20):

I guess this only works for certain "coefficient" categories

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 13:02):

I've done sheafification for sheaves on a lawvere tierney topology, I'm in the process of doing the specialisation to sites

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 13:04):

This would give sheafification on set-valued sheaves on a site, and since I've got the adjunction to forgetful and preservation of finite limits, ring-valued sheaves and whatever should drop out

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 13:04):

Actually one annoyingly missing thing is that preservation of finite products + equalizers gives preservation of finite limits, strictly speaking I only have the former, though the second is true in Lean (since preserving limits is subsingleton)

view this post on Zulip Scott Morrison (Jul 23 2020 at 13:42):

Johan and I have been working on something very low-brow, and verified that the presheaf of functions (not continuous or anything) really is a sheaf.

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 13:45):

I think the most usable thing to do would be for me to define the equivalence of categories (or topoi?) between my specialised category of sheaves and your concrete category of sheaves, so that you quickly get all the nice categorical properties but don't have to deal with a weird topos api

view this post on Zulip Johan Commelin (Jul 23 2020 at 13:48):

Will things translate nicely along such an equivalence?

view this post on Zulip Johan Commelin (Jul 23 2020 at 13:48):

I would expect that it is better to show that Shv(C) is a topos

view this post on Zulip Johan Commelin (Jul 23 2020 at 13:49):

And maybe have a class [grothendieck_topos] that contains extra API on top of the elementary topos stuff

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 13:52):

I think categorical properties should transfer nicely at least - if you've got that Shv(C) is a category and I can show it's equivalent to my sh(j), then it should drop out that Shv(C) is a topos too

view this post on Zulip Johan Commelin (Jul 23 2020 at 13:53):

Ok... aren't there defs involved that need nice definitions for future hapiness?

view this post on Zulip Johan Commelin (Jul 23 2020 at 13:53):

Or is everything subsingleton?

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 13:54):

There are (non-subsingleton) defs involved, but if the entire structure of a topos is transferred along an equivalence, all the defs should play nicely with each other

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 13:55):

(This is my guess, at least)

view this post on Zulip Johan Commelin (Jul 23 2020 at 14:07):

Sure, but will they play nice with defs outside of topos theory...

view this post on Zulip Johan Commelin (Jul 23 2020 at 14:07):

For example, the exponential object in Shv(C) might want to be the "obvious" definition, instead of something pulled through an equivalence.

view this post on Zulip Johan Commelin (Jul 23 2020 at 14:08):

Because at some point you are going to take sections of that sheaf, and want to treat it as a (un)curried function [I always forget whether it's curry or uncurry]

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 14:29):

Right I see your concern, but my hope is that since we have the universal property, you can transport across the adjunction and treat it as an uncurried function directly

view this post on Zulip Johan Commelin (Jul 23 2020 at 14:31):

Aha... let's hope that works (-;

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 15:42):

I suspect a bigger annoyance might be if you want to work with the product of sheaves - essentially the same problem as if you want to give an element of the cartesian product of types, it's not just the type product because of the has_binary_products Type instance. My way around this for Type has been to use generalised elements - just giving the nat bij between 1 -> X and X, and we have an obvious nat bij between C -> X x Y and pairs C -> X, C -> Y, and putting this together lets you get the element of type X x Y given just an element of type X and element of type Y, which does play well with the other definitions and lemmas; I don't know if something analogous works in geometry though

view this post on Zulip Bhavik Mehta (Jul 23 2020 at 15:43):

I think some lemmas to work with generalised elements might be really useful actually, especially in a well-powered category (like any grot top)

view this post on Zulip Scott Morrison (Jul 24 2020 at 13:33):

@Johan Commelin, I just thoroughly commented our proof from last night. It's on the branch. I propose we do the continuous function version as well, and stage that off as a PR before continuing. I'm happy enough that this setup is viable.

view this post on Zulip Heather Macbeth (Jul 24 2020 at 13:49):

That's a lovely commenting job! You have one interesting TODO:

In fact, I'd like to do it for any "functions satisfying a local condition", for which there's a sketch at https://github.com/leanprover-community/mathlib/issues/1462

If you introduce this class of functions, I think it can be used elsewhere in the library. For example, Sébastien has the definition docs#structure_groupoid.local_invariant_prop for conditions on functions which are local + invariant under a groupoid; maybe that could extend your class.

view this post on Zulip Reid Barton (Jul 26 2020 at 22:54):

Bhavik Mehta said:

I suspect a bigger annoyance might be if you want to work with the product of sheaves - essentially the same problem as if you want to give an element of the cartesian product of types, it's not just the type product because of the has_binary_products Type instance. My way around this for Type has been to use generalised elements - just giving the nat bij between 1 -> X and X, and we have an obvious nat bij between C -> X x Y and pairs C -> X, C -> Y, and putting this together lets you get the element of type X x Y given just an element of type X and element of type Y, which does play well with the other definitions and lemmas; I don't know if something analogous works in geometry though

This is a bigger problem in topology--Top has_limits and therefore has_binary_products but they aren't the ones that we have many nontrivial theorems about, and it's not so easy to connect them. For example, try proving that locally compact spaces are exponentiable and so products by them preserve pushouts. All the nontrivial math is done (I needed it for lean-homotopy-theory), but the pieces don't fit together.

view this post on Zulip Reid Barton (Jul 26 2020 at 23:04):

In lean-homotopy-theory I only needed the functor ×[0,1]- \times [0, 1] and I didn't ever really need the fact that it's a product in the sense of category theory, so I just defined it directly using prod, and then it connected directly to all the relevant facts about product spaces that we already have.

view this post on Zulip Reid Barton (Jul 26 2020 at 23:07):

But that doesn't really seem like the correct approach for mathlib to take.

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 14:48):

@Reid Barton said:

Bhavik Mehta said:

I suspect a bigger annoyance might be if you want to work with the product of sheaves - essentially the same problem as if you want to give an element of the cartesian product of types, it's not just the type product because of the has_binary_products Type instance. My way around this for Type has been to use generalised elements - just giving the nat bij between 1 -> X and X, and we have an obvious nat bij between C -> X x Y and pairs C -> X, C -> Y, and putting this together lets you get the element of type X x Y given just an element of type X and element of type Y, which does play well with the other definitions and lemmas; I don't know if something analogous works in geometry though

This is a bigger problem in topology--Top has_limits and therefore has_binary_products but they aren't the ones that we have many nontrivial theorems about, and it's not so easy to connect them. For example, try proving that locally compact spaces are exponentiable and so products by them preserve pushouts. All the nontrivial math is done (I needed it for lean-homotopy-theory), but the pieces don't fit together.

Alright, I'll give this a go - is the hard part showing that locally compact spaces are exponentiable or that products by them preserve pushouts?

view this post on Zulip Reid Barton (Jul 29 2020 at 16:16):

There's no hard part really. You can consult https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/homotopy_theory/topological_spaces/exponentiable.lean

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:19):

So which pieces don't fit together? I'm confused about what you're proposing the problem here is

view this post on Zulip Reid Barton (Jul 29 2020 at 16:22):

mathlib products

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:38):

I'm not sure if this is what you meant, but I got:

variables {α : Type u} [topological_space α] [locally_compact_space α]
def prod_colimit_iso {β γ δ : Top.{u}} (f : β  γ) (g : β  δ) :
  Top.of α  pushout f g  pushout (limits.prod.map (𝟙 (Top.of α)) f) (limits.prod.map (𝟙 (Top.of α)) g) :=

without any pain

view this post on Zulip Reid Barton (Jul 29 2020 at 16:39):

source?

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:40):

https://gist.github.com/b-mehta/bbdc500ab81bc07b3c31d22878187c19

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:40):

Presumably much of it could be improved since I don't know the topology api at all well

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:40):

but other than that I just tried what was most obvious to me and didn't golf at all, and it happened in 64 lines

view this post on Zulip Reid Barton (Jul 29 2020 at 16:43):

This is using the specific construction of products for Top right?

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:43):

No, just the universal property

view this post on Zulip Reid Barton (Jul 29 2020 at 16:45):

what is https://gist.github.com/b-mehta/bbdc500ab81bc07b3c31d22878187c19#file-reid-lean-L27-L31 then?

view this post on Zulip Reid Barton (Jul 29 2020 at 16:46):

anyways, it's hard to explain the issue with a self-contained example because it is really a global problem

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:46):

Right but I maintain that it's a problem I've never had

view this post on Zulip Reid Barton (Jul 29 2020 at 16:47):

You will have it!

view this post on Zulip Bhavik Mehta (Jul 29 2020 at 16:50):

When? :)

view this post on Zulip Reid Barton (Jul 29 2020 at 16:57):

I don't know but when you do let me know. I've pretty much given up on following the category theory library for now.


Last updated: May 16 2021 at 05:21 UTC