Zulip Chat Archive

Stream: general

Topic: bundled presheaves with preorders on the stalks


Scott Morrison (Apr 06 2019 at 05:56):

Hi @Kevin Buzzard, I think I've got it --- the category of bundled presheaves with preordered stalks.

Kevin Buzzard (Apr 06 2019 at 06:21):

Topological rings?

Kevin Buzzard (Apr 06 2019 at 06:22):

With the stalks being computed on the underlying presheaf of rings?

Kevin Buzzard (Apr 06 2019 at 06:23):

We need two things from this category -- the notion of isomorphism (which comes for free) and the ability to pull back to an open subspace

Kevin Buzzard (Apr 06 2019 at 06:24):

Many thanks!

Scott Morrison (Apr 06 2019 at 06:37):

okay, I think my TODO list for this stuff is:
1) put the ops back in the open sets
2) PR everything about presheafs, unbundled and bundled, to mathlib
3) dump the stuff about stalks, and structured stalks, into perfectoid? (it's not mathlib ready)
4) do pullbacks to open subspaces
5) generalise "stalks with preorders" to "stalks with structure"
6) once we have a has_colimits CommRing instance, everything is already set up to compute stalks in CommRing (or for that matter in TopCommRing)

Kevin Buzzard (Apr 06 2019 at 08:16):

Presumably the has_colimits CommRing instance will give us the universal property as well?

Kevin Buzzard (Apr 06 2019 at 08:18):

I know that @Ramon Fernandez Mir made the construction of a general colimit of comm rings (as a quotient of the poly ring over Z in variables corresponding to the disjoint union of the rings) late last year but I can't find it in his schemes repo :-/

Scott Morrison (Apr 06 2019 at 08:37):

Yes, has_colimits packages the universal property.

Kevin Buzzard (Apr 06 2019 at 08:49):

Actually here's a potential problem. I need to define a preorder on the colimit. In this case (the stalk of a sheaf on a top space) the colimit is actually a direct limit. I would imagine that the universal property is a statement about defining ring homs from the colimit to other rings. But this is not what we have; I want to define a morphism of types from the stalk to some other type (I want to define a valuation on the stalk, and I'll get the preorder from the valuation). The underlying type of a direct limit of commutative rings is equal to the direct limit of the underlying types, so I can use the universal property of direct limits of types to get my function. However it is not true that the underlying type of an arbitrary colimit of commutative rings is equal to the colimit of the underlying types (consider a coproduct of two rings; the underlying type of the coproduct isn't the disjoint union of the two underlying types).

Scott Morrison (Apr 06 2019 at 08:53):

Yes. :-)

Johan Commelin (Apr 06 2019 at 08:53):

Luckily Reid pushed some stuff about filtered limits to a branch...

Johan Commelin (Apr 06 2019 at 08:54):

Once that code is accessible (either in mathlib, or in the perfectoid project) we only need to show that the forgetful functor from CommRing to Type preserves filtered colimits

Kevin Buzzard (Apr 06 2019 at 09:57):

is "filtered colimits" the same as direct limits?

Scott Morrison (Apr 06 2019 at 10:53):

yes, a very slight generalisation

Scott Morrison (Apr 06 2019 at 10:53):

having either implies the other

Scott Morrison (Apr 06 2019 at 10:54):

a category is filtered if every finite diagram admits a cone

Scott Morrison (Apr 06 2019 at 10:54):

in particular, for every two objects X and Y, you can find an object Z with maps X -> Z and Y -> Z

Scott Morrison (Apr 06 2019 at 10:55):

and for every parallel pair of morphisms f g : X \hom Y, there is a h : Y \hom Z so f h = g h.

Scott Morrison (Apr 06 2019 at 10:55):

and there is an object!

Scott Morrison (Apr 06 2019 at 10:56):

Putting the op back in the definition of presheaves is really awful. I have spent hours on it.

Scott Morrison (Apr 06 2019 at 10:57):

@Johan Commelin, @Reid Barton, if either of you want to explain why it is so dire to bake it into the source category, that would be great.

Scott Morrison (Apr 06 2019 at 10:57):

also, if you want to look at my code/screen share, etc, we can try to fix it!

Scott Morrison (Apr 06 2019 at 11:07):

Just in case anyone wants to have a look:

  • deb92bf7c3340e47652206ed64e0933fcfd1cc36 is presheaves (with opens defined with reverse inclusion)
  • 4cb659a3dace959dd9e2ef2ea476066a79d40e57 is stalks (with opens defined with reverse inclusion)
  • 5793683020650371848828bacbbeea8310625c34 is def presheaf (X) := (opens X)ᵒᵖ ⥤ C, pretty much working, but with some proof made grosser
  • faffe160b9c281e46b6086f0a49da4eaae4ee3ea is stalks based on that, with everything borked and apparently unfixable.

Johan Commelin (Apr 06 2019 at 11:20):

Sorry, to which url should we append these hashes to see the code?

Kevin Buzzard (Apr 06 2019 at 11:44):

It sounds to me like "you haven't quite got op working yet". So can you just define a new category opens_op?

I am about to embark on a journey to Austria via Germany and will try to get a bunch of work done. I am acutely aware that whilst all the pieces seem to be there for defining adic spaces, it will take some time to glue them together.

matt rice (Apr 06 2019 at 12:20):

Sorry, to which url should we append these hashes to see the code?

they are all linked from here it seems,
https://github.com/leanprover-community/mathlib/compare/stalks-op
https://github.com/leanprover-community/mathlib/compare/presheaf

Reid Barton (Apr 06 2019 at 17:52):

if either of you want to explain why it is so dire to bake it into the source category, that would be great.

I guess the core reason is that the morphisms in opens X are not just some bookkeeping device to keep track of the subset relation, they have actual geometric content. A morphism UVU \to V should really be thought of as a (continuous) map from UU to VV which is compatible with the inclusions UXU \to X and VXV \to X. Geometrically, it doesn't make sense to think of it as a morphism from VV to UU.

Kevin Buzzard (Apr 06 2019 at 17:55):

I think it's a great idea to make the category that Scott can work with.

Reid Barton (Apr 06 2019 at 17:55):

Also, it might not really matter for what Kevin wants to do for perfectoid spaces, but if you want to define sheaves even in the most classical way, then you're going to talk about covering families which are supposed to be families of maps {UαU}\{U_\alpha \to U\}, not {UUα}\{U \to U_\alpha\}.

Kevin Buzzard (Apr 06 2019 at 17:55):

I also think it's a great idea to think about why he can't yet work with opposite categories. The opposite category is really closely related to the bake-in-the-maps-the-wrong-way category; I hesitate to say they're isomorphic but they look isomorphic to me.

Kevin Buzzard (Apr 06 2019 at 17:56):

As we all know, just because two things are isomorphic and you can prove stuff for one, it doesn't mean that you can deduce stuff for the other, and it certainly doesn't mean that the same techniques that prove stuff for one will prove the same stuff for the other

Kevin Buzzard (Apr 06 2019 at 17:58):

This is where Scott seems to be. So ideally at some point someone should figure out why using opposite categories makes stuff so much more like hard work, and of course and ideal candidate would be someone who is moaning about Scott not using opposites ;-) They will either become convinced Scott is right, or they'll show him how to get it working :D

Reid Barton (Apr 06 2019 at 17:58):

More generally, the setup is that we have some category of geometric objects which came from somewhere, and we want to formally extend to presheaves. The original category is supposed to embed in the category of presheaves, by the Yoneda embedding. It doesn't work if you don't put op in the definition of presheaves.

Kevin Buzzard (Apr 06 2019 at 17:58):

How about functors from usual opens to ring^op? ;-)

Reid Barton (Apr 06 2019 at 17:59):

I agree, it seems like something is just missing about the way opposites are set up, maybe some missing simp lemmas.

Reid Barton (Apr 06 2019 at 17:59):

I mean Scott can't really be using anything about opens X that changes when we reverse the arrows, right?

Kevin Buzzard (Apr 06 2019 at 17:59):

exactly. If Scott has got things working with the arrows baked the wrong way round, it provides a natural starting point for trying to figure out what the hell is going on.

Kevin Buzzard (Apr 06 2019 at 18:00):

It could just be a case of Lean not unfolding something.

Reid Barton (Apr 06 2019 at 18:00):

somehow it works with opens_op X but not with (opens X)\op

Reid Barton (Apr 06 2019 at 18:01):

I'm guessing it's an instance of a recurring annoyance for category theory, where we have simp lemmas like f >> 1 X = f which simp is fond of not applying

Reid Barton (Apr 06 2019 at 18:02):

because under the hood the simp lemma says comp Y X X f (1 X) = f, but maybe the implicit object arguments in an occurrence of f >> 1 X are not syntactically X, but only something defeq to X

Reid Barton (Apr 06 2019 at 18:06):

For example, one of the implicit Xs might be (functor.id C).obj X

Johan Commelin (Apr 06 2019 at 18:07):

But that ought to be simped away as well, right?

Reid Barton (Apr 06 2019 at 18:08):

Well it can't be simped because it is in a position where the type of something else depends on it. It can be dsimped though. That's why we end up with simp, dsimp, simp stuff

Reid Barton (Apr 06 2019 at 18:09):

but if we didn't have the simp lemma for (functor.id C).obj X, we'd be stuck. So hopefully we are just missing some similar simp lemma for opposite stuff.

Reid Barton (Apr 06 2019 at 18:09):

It seems like a difficult problem to solve in general though because you are relying on dsimp to be able to put objects into a consistent normal form, but, in general, the objects of your category could be anything

Johan Commelin (Apr 06 2019 at 18:12):

Which means we need something that is smarter than "try to normalise LHS and RHS and hope that we win". I guess this is where rw_search might become a real hero (-;

Reid Barton (Apr 06 2019 at 18:17):

Well, I think all we really need here is for simp to match repeated variables in the lemma it is trying to apply using definitional equality, rather than syntactic equality

Reid Barton (Apr 06 2019 at 18:17):

maybe there's even an option to do that already?

Scott Morrison (Apr 07 2019 at 03:50):

I had another read over the simp configuration, and I don't think there's anything that does this.

Reid Barton (Apr 07 2019 at 03:51):

Are the fields of the options record documented somewhere?

Scott Morrison (Apr 07 2019 at 03:52):

I've got everything working again on the stalks-op branch. There are some ugly proofs, but they are ugly in controlled ways:
1) I need to call erw category_theory.functor.map_id and erw category.id_comp frequently, when you'd hope that simp works.
2) In one or two places I have a j : (nbhds X)ᵒᵖ, and I have to run an unpleasant little sequence dsimp [opposite] at j, cases j, cases j_val, dsimp before being able to proceed, so that some things become definitionally true.

Scott Morrison (Apr 07 2019 at 03:53):

No, I've never found documentation for the simp configuration object.


Last updated: Dec 20 2023 at 11:08 UTC