## Stream: Is there code for X?

### Topic: Sheaves of category-objects

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

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

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

#### Scott Morrison (Jul 22 2020 at 23:33):

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

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

#### Scott Morrison (Jul 22 2020 at 23:35):

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

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

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

#### Kevin Buzzard (Jul 23 2020 at 06:59):

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

#### Scott Morrison (Jul 23 2020 at 07:38):

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

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

#### Johan Commelin (Jul 23 2020 at 08:12):

@Scott Morrison This is cool

#### Johan Commelin (Jul 23 2020 at 08:12):

Where is the code?

#### Scott Morrison (Jul 23 2020 at 08:12):

sheaf_condition_in_Type

#### Johan Commelin (Jul 23 2020 at 08:12):

Ok, I'll take a look right now

#### Scott Morrison (Jul 23 2020 at 08:13):

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

#### Scott Morrison (Jul 23 2020 at 08:13):

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

#### Scott Morrison (Jul 23 2020 at 08:13):

and seems worth commenting properly :-)

#### Johan Commelin (Jul 23 2020 at 08:13):

Awww, there are no oleans yet

#### Johan Commelin (Jul 23 2020 at 08:14):

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

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

#### Scott Morrison (Jul 23 2020 at 08:19):

yeah, sheafification would be a good goal

#### Johan Commelin (Jul 23 2020 at 08:19):

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

#### Scott Morrison (Jul 23 2020 at 08:19):

via plus construction?

Probably, yes

#### Johan Commelin (Jul 23 2020 at 08:20):

I guess this only works for certain "coefficient" categories

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

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

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

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

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

#### Johan Commelin (Jul 23 2020 at 13:48):

Will things translate nicely along such an equivalence?

#### Johan Commelin (Jul 23 2020 at 13:48):

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

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

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

#### Johan Commelin (Jul 23 2020 at 13:53):

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

#### Johan Commelin (Jul 23 2020 at 13:53):

Or is everything subsingleton?

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

#### Bhavik Mehta (Jul 23 2020 at 13:55):

(This is my guess, at least)

#### Johan Commelin (Jul 23 2020 at 14:07):

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

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

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

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

#### Johan Commelin (Jul 23 2020 at 14:31):

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

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

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

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

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

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

#### Reid Barton (Jul 26 2020 at 23:04):

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 (Jul 26 2020 at 23:07):

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

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

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

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

mathlib products

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

source?

#### Bhavik Mehta (Jul 29 2020 at 16:40):

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

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

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

#### Reid Barton (Jul 29 2020 at 16:43):

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

#### Bhavik Mehta (Jul 29 2020 at 16:43):

No, just the universal property

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

#### Bhavik Mehta (Jul 29 2020 at 16:46):

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

#### Reid Barton (Jul 29 2020 at 16:47):

You will have it!

When? :)

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