colimits in Top

Stream: maths

[Kevin Buzzard]

Do we have coproductscolimits of topological spaces, in either unbundled or bundled form? @Scott Morrison @Mario Carneiro

[Mario Carneiro]

that is disjoint union?

[Kevin Buzzard]

I just want to make a topological space from a union of open sets.

[Kevin Buzzard]

Sorry, I mean colimits

[Scott Morrison]

Yes, we have arbitrarily limits and colimits, see topology/Top/limits.lean

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/src/topology/Top/limits.lean#L51

[Kevin Buzzard]

So this is the bundled form. How about the unbundled form?

[Kevin Buzzard]

Just some explicit lemma about I've got a bunch of topological spaces with no mention of Top

[Johan Commelin]

@Scott Morrison You also had some example file, showing how to work with these, right?

[Kevin Buzzard]

I'd be interested in extracting the unbundled form.

[Scott Morrison]

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

[Kevin Buzzard]

Super, thanks.

[Scott Morrison]

Why not see if you can use the bundled version? You may find you like it. :-)

[Mario Carneiro]

Where is F.sections defined?

[Mario Carneiro]

I want to see the actual type

[Scott Morrison]

category_theory/types.lean

[Scott Morrison]

def sections (F : J ⥤ Type w) : set (Π j, F.obj j) :=
{ u | ∀ {j j'} (f : j ⟶ j'), F.map f (u j) = u j'}

[Kevin Buzzard]

I think bundled v unbundled is a big question. We have to make judgements about what to do here. I have a love-hate relationship with the category theory repo, but every time I fail I come back later a little bit stronger.

[Kevin Buzzard]

I will definitely try the bundled version as well. All we want to do is glue schemes. Kenny has "proved the lemma" that says you can glue locally ringed spaces, unbundled. That's a really useful result. Can you bundle that result? How much of the innards of his argument do you really have to gut in order to bundle it? My feeling is that is an important problem for the expert Bundlers like Reid, Scott and Johan to decide. Kenny is just using an interface really.

[Mario Carneiro]

I prefer for new type definitions to be made free standing, where they can be straightforwardly topologized

[Kevin Buzzard]

We have to try to do really hard things both bundled and unbundled and to see which works best. Kenny is leading the pack with gluing on one top space in the unbundled world, and the bundled world is ahead with gluing topological spaces. Those are the two ingredients needed.

[Mario Carneiro]

I see that F.sections is a subset of a product, does that give it the right topology?

[Johan Commelin]

I prefer for new type definitions to be made free standing, where they can be straightforwardly topologized

What does that mean?

[Mario Carneiro]

sum, the type operator, is defined before category theory

[Scott Morrison]

Just that the type should be defined first, and then the bundled topological space

[Scott Morrison]

exactly as we do in this example: F.sections is the underlying type of lim F.

[Johan Commelin]

The underlying unbundled type of X × Y for X Y : Scheme is horrible, and not what you would think it is.

[Johan Commelin]

It is a completely useless gadget without its topology and sheaf.

[Mario Carneiro]

I think being able to ask what the topology is and what the type definition is of some category construction is a basic question. There are complicated constructions, but doing things via category theory always seems to make it hard to answer these kinds of questions, because everything is buried ten levels deep. It's fine if you never intend to see that stuff again, but I'm sure if Kenny was proving something about one of these concrete types he would just unfold the whole lot of it and work with the underlying representation

[Mario Carneiro]

If you are just doing topology then all that structure just gets in the way

[Kevin Buzzard]

We are not doing products ever here, we are doing colimits of schemes at the minute for some fundamental constructions. We cannot even do scheme-theoretic products until we have colimits.

[Kevin Buzzard]

A scheme is by definition a colimit of basic objects (affine schemes). The basic objects are rings. We do things on rings and then use an extensive transfer theory which we're building by hand to transfer results to colimits

[Johan Commelin]

You mean colimit, I think.

[Kevin Buzzard]

A product of schemes is just a colimit of products of basic objects

[Kevin Buzzard]

gaargh thanks Johan I'll edit.

[Kevin Buzzard]

Thanks. Johan -- do you understand the "basic principle in algebraic geometry" that to prove a certain class of results about schemes, it suffices to prove a related theorem about rings and then to just follow your intuitive algebraic geometer's nose?

[Mario Carneiro]

I think the question of using a predicate vs a construction comes up here btw

[Kevin Buzzard]

Can you formalise that? Is it something to do with commuting with colimits?

[Mario Carneiro]

Are you sure you actually need the colimit construction?

[Mario Carneiro]

It sounds like you just assert such and such is a colimit of some diagram

[Mario Carneiro]

and prove facts from that

[Kevin Buzzard]

If I were lecturing graduate algebraic geometry, I would say "Definition of product of schemes. Step 1 tensor product of rings. Step 2 follow your nose." and I would include a link to the slogan in the stacks project

[Kevin Buzzard]

But there's a subtlety actually because arbitrary colimits don't exist in the category of schemes!

[Kevin Buzzard]

I do not understand what is going on here at all, but I am sure there people who understand it well. Maybe I need to put a topology on the category of rings, and then I can just make schemes magically? Johan do you know this stuff?

[Johan Commelin]

I don't know it well enough to extract a formal statement (-;

[Johan Commelin]

Struggling just as hard as you are.

[Mario Carneiro]

A topology on the category of rings does not typecheck

[Johan Commelin]

Of course there is the "magic" definition that produces algebraic spaces as certain sheaves for the etale topology on AffSch := CommRing^op

[Kevin Buzzard]

I don't need the full strength of bundled colimits in top to be able to make the unbundled colimits I want.

[Kevin Buzzard]

A topology on the category of rings does not typecheck

I guess it would be grothendieck-topology or something

[Johan Commelin]

I think Toen and Vezossi worked out those details.

[Johan Commelin]

But I don't think that definition will make building examples any easier.

[Mario Carneiro]

okay, this is beyond my pay grade, good luck

[Kevin Buzzard]

No but I would really like a tool which says "This result about schemes is local, so it suffices to prove it in the affine case, which is the same as this question about rings, so let's just answer this question about rings instead."

[Kevin Buzzard]

Because I used that tool loads when I was doing alg geom.

[Johan Commelin]

Definitely. And if we can't make it into a theorem, then it might be a meta-theorem (aka tactic).

[Kevin Buzzard]

I want to build products of schemes by saying "look, I made products of rings, so now just give me all the ring-theory results which the machine needs"

[Kevin Buzzard]

The stacks project slogan

The stacks project proof

Not hard to see where de Jong is directing the reader, but good that he writes the abstract stuff!

[Kevin Buzzard]

I think Toen and Vezossi worked out those details.

Do you have a more precise reference? I'm interested

[Johan Commelin]

Note that this works best for algebraic spaces and stacks, not so much for schemes: https://mathoverflow.net/questions/26506/categorical-construction-of-the-category-of-schemes

[Johan Commelin]

And once you want to prove theorems about schemes, you'll still want to know that there is a fully faithful functor to LRS.

[Johan Commelin]

So I don't think this path is directly worth pursuing

[Jan-David Salchow]

Are you guys aware of Vakils "Affine Communication Lemma"? (Lemma 5.3.2 in http://math.stanford.edu/~vakil/216blog/FOAGnov1817public.pdf )

[Johan Commelin]

No, I was not.

[Johan Commelin]

I was aware of the content, but I didn't know a written reference for it.

[Johan Commelin]

I'm not sure if it helps Kevin with his current problems. I feel like Kevin wants a data-variant, instead of only a predicate/property-variant.