Sheaves of category-objects

Stream: Is there code for X?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

@Scott Morrison This is cool

[Johan Commelin]

Where is the code?

[Scott Morrison]

sheaf_condition_in_Type

[Johan Commelin]

Ok, I'll take a look right now

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

and seems worth commenting properly :-)

[Johan Commelin]

Awww, there are no oleans yet

[Johan Commelin]

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

[Johan Commelin]

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

5. Sheafification
6. Pullback and pushforward of sheaves

[Scott Morrison]

yeah, sheafification would be a good goal

[Johan Commelin]

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

[Scott Morrison]

via plus construction?

[Johan Commelin]

Probably, yes

[Johan Commelin]

I guess this only works for certain "coefficient" categories

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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)

[Scott Morrison]

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.

[Bhavik Mehta]

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

[Johan Commelin]

Will things translate nicely along such an equivalence?

[Johan Commelin]

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

[Johan Commelin]

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

[Bhavik Mehta]

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

[Johan Commelin]

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

[Johan Commelin]

Or is everything subsingleton?

[Bhavik Mehta]

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

[Bhavik Mehta]

(This is my guess, at least)

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

[Bhavik Mehta]

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

[Johan Commelin]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Scott Morrison]

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

[Heather Macbeth]

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.

[Reid Barton]

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.

[Reid Barton]

In lean-homotopy-theory I only needed the functor $- \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.

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

mathlib products

[Bhavik Mehta]

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

[Reid Barton]

source?

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Reid Barton]

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

[Bhavik Mehta]

No, just the universal property

[Reid Barton]

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Reid Barton]

You will have it!

[Bhavik Mehta]

When? :)

[Reid Barton]

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.