Zulip Chat Archive

Stream: maths

Topic: colimits in Top


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 23 2019 at 09:40):

that is disjoint union?

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 09:40):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 09:41):

Sorry, I mean colimits

view this post on Zulip Scott Morrison (Jul 23 2019 at 09:41):

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

view this post on Zulip Johan Commelin (Jul 23 2019 at 09:41):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 09:42):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 23 2019 at 09:42):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 09:42):

I'd be interested in extracting the unbundled form.

view this post on Zulip Scott Morrison (Jul 23 2019 at 09:43):

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 09:43):

Super, thanks.

view this post on Zulip Scott Morrison (Jul 23 2019 at 09:43):

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

view this post on Zulip Mario Carneiro (Jul 23 2019 at 09:44):

Where is F.sections defined?

view this post on Zulip Mario Carneiro (Jul 23 2019 at 09:45):

I want to see the actual type

view this post on Zulip Scott Morrison (Jul 23 2019 at 09:46):

category_theory/types.lean

view this post on Zulip 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'}

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 23 2019 at 09:49):

sum, the type operator, is defined before category theory

view this post on Zulip Scott Morrison (Jul 23 2019 at 09:50):

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

view this post on Zulip Scott Morrison (Jul 23 2019 at 09:50):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 23 2019 at 09:51):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 23 2019 at 09:56):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 23 2019 at 10:00):

You mean colimit, I think.

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 10:00):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 10:00):

gaargh thanks Johan I'll edit.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 23 2019 at 10:02):

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

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 10:02):

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

view this post on Zulip Mario Carneiro (Jul 23 2019 at 10:03):

Are you sure you actually need the colimit construction?

view this post on Zulip Mario Carneiro (Jul 23 2019 at 10:03):

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

view this post on Zulip Mario Carneiro (Jul 23 2019 at 10:04):

and prove facts from that

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 23 2019 at 10:05):

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

view this post on Zulip Johan Commelin (Jul 23 2019 at 10:05):

Struggling just as hard as you are.

view this post on Zulip Mario Carneiro (Jul 23 2019 at 10:06):

A topology on the category of rings does not typecheck

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 23 2019 at 10:06):

I think Toen and Vezossi worked out those details.

view this post on Zulip Johan Commelin (Jul 23 2019 at 10:07):

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

view this post on Zulip Mario Carneiro (Jul 23 2019 at 10:07):

okay, this is beyond my pay grade, good luck

view this post on Zulip 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."

view this post on Zulip Kevin Buzzard (Jul 23 2019 at 10:08):

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

view this post on Zulip 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).

view this post on Zulip 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"

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 23 2019 at 12:20):

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

view this post on Zulip 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 )

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:01):

No, I was not.

view this post on Zulip Johan Commelin (Jul 23 2019 at 14:02):

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

view this post on Zulip 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