bundled presheaves with preorders on the stalks

Stream: general

[Scott Morrison]

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

[Kevin Buzzard]

Topological rings?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Many thanks!

[Scott Morrison]

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]

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

[Kevin Buzzard]

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]

Yes, has_colimits packages the universal property.

[Kevin Buzzard]

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]

Yes. :-)

[Johan Commelin]

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

[Johan Commelin]

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]

is "filtered colimits" the same as direct limits?

[Scott Morrison]

yes, a very slight generalisation

[Scott Morrison]

having either implies the other

[Scott Morrison]

a category is filtered if every finite diagram admits a cone

[Scott Morrison]

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

[Scott Morrison]

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]

and there is an object!

[Scott Morrison]

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

[Scott Morrison]

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

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

[Scott Morrison]

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]

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

[Kevin Buzzard]

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]

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]

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 $U \to V$ should really be thought of as a (continuous) map from $U$ to $V$ which is compatible with the inclusions $U \to X$ and $V \to X$. Geometrically, it doesn't make sense to think of it as a morphism from $V$ to $U$.

[Kevin Buzzard]

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

[Reid Barton]

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_\alpha \to U\}$, not $\{U \to U_\alpha\}$.

[Kevin Buzzard]

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]

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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Johan Commelin]

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

[Reid Barton]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Reid Barton]

Are the fields of the options record documented somewhere?

[Scott Morrison]

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]

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