## Stream: maths

### Topic: colimits in Top

#### Kevin Buzzard (Jul 23 2019 at 09:40):

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

#### Mario Carneiro (Jul 23 2019 at 09:40):

that is disjoint union?

#### Kevin Buzzard (Jul 23 2019 at 09:40):

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

#### Kevin Buzzard (Jul 23 2019 at 09:41):

Sorry, I mean colimits

#### Scott Morrison (Jul 23 2019 at 09:41):

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

#### Johan Commelin (Jul 23 2019 at 09:41):

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

#### Kevin Buzzard (Jul 23 2019 at 09:42):

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

#### Kevin Buzzard (Jul 23 2019 at 09:42):

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

#### Johan Commelin (Jul 23 2019 at 09:42):

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

#### Kevin Buzzard (Jul 23 2019 at 09:42):

I'd be interested in extracting the unbundled form.

#### Scott Morrison (Jul 23 2019 at 09:43):

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

Super, thanks.

#### Scott Morrison (Jul 23 2019 at 09:43):

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

#### Mario Carneiro (Jul 23 2019 at 09:44):

Where is F.sections defined?

#### Mario Carneiro (Jul 23 2019 at 09:45):

I want to see the actual type

#### Scott Morrison (Jul 23 2019 at 09:46):

category_theory/types.lean

#### Scott Morrison (Jul 23 2019 at 09:46):

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 (Jul 23 2019 at 09:47):

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 (Jul 23 2019 at 09:47):

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 (Jul 23 2019 at 09:48):

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

#### Kevin Buzzard (Jul 23 2019 at 09:48):

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 (Jul 23 2019 at 09:48):

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

#### Johan Commelin (Jul 23 2019 at 09:49):

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

What does that mean?

#### Mario Carneiro (Jul 23 2019 at 09:49):

sum, the type operator, is defined before category theory

#### Scott Morrison (Jul 23 2019 at 09:50):

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

#### Scott Morrison (Jul 23 2019 at 09:50):

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

#### Johan Commelin (Jul 23 2019 at 09:50):

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

#### Johan Commelin (Jul 23 2019 at 09:51):

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

#### Mario Carneiro (Jul 23 2019 at 09:56):

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 (Jul 23 2019 at 09:56):

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

#### Kevin Buzzard (Jul 23 2019 at 09:58):

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 (Jul 23 2019 at 09:59):

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 (Jul 23 2019 at 10:00):

You mean colimit, I think.

#### Kevin Buzzard (Jul 23 2019 at 10:00):

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

#### Kevin Buzzard (Jul 23 2019 at 10:00):

gaargh thanks Johan I'll edit.

#### Kevin Buzzard (Jul 23 2019 at 10:02):

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 (Jul 23 2019 at 10:02):

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

#### Kevin Buzzard (Jul 23 2019 at 10:02):

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

#### Mario Carneiro (Jul 23 2019 at 10:03):

Are you sure you actually need the colimit construction?

#### Mario Carneiro (Jul 23 2019 at 10:03):

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

#### Mario Carneiro (Jul 23 2019 at 10:04):

and prove facts from that

#### Kevin Buzzard (Jul 23 2019 at 10:04):

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 (Jul 23 2019 at 10:04):

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

#### Kevin Buzzard (Jul 23 2019 at 10:05):

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 (Jul 23 2019 at 10:05):

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

#### Johan Commelin (Jul 23 2019 at 10:05):

Struggling just as hard as you are.

#### Mario Carneiro (Jul 23 2019 at 10:06):

A topology on the category of rings does not typecheck

#### Johan Commelin (Jul 23 2019 at 10:06):

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

#### Kevin Buzzard (Jul 23 2019 at 10:06):

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

#### Kevin Buzzard (Jul 23 2019 at 10:06):

A topology on the category of rings does not typecheck

I guess it would be grothendieck-topology or something

#### Johan Commelin (Jul 23 2019 at 10:06):

I think Toen and Vezossi worked out those details.

#### Johan Commelin (Jul 23 2019 at 10:07):

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

#### Mario Carneiro (Jul 23 2019 at 10:07):

okay, this is beyond my pay grade, good luck

#### Kevin Buzzard (Jul 23 2019 at 10:08):

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 (Jul 23 2019 at 10:08):

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

#### Johan Commelin (Jul 23 2019 at 10:08):

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

#### Kevin Buzzard (Jul 23 2019 at 10:09):

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 (Jul 23 2019 at 10:18):

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 (Jul 23 2019 at 11:50):

I think Toen and Vezossi worked out those details.

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

#### Johan Commelin (Jul 23 2019 at 12:19):

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 (Jul 23 2019 at 12:19):

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 (Jul 23 2019 at 12:20):

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

#### Jan-David Salchow (Jul 23 2019 at 13:55):

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

No, I was not.

#### Johan Commelin (Jul 23 2019 at 14:02):

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

#### Johan Commelin (Jul 23 2019 at 14:03):

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.

Last updated: May 06 2021 at 17:38 UTC