Zulip Chat Archive

Stream: maths

Topic: presheaves


view this post on Zulip Scott Morrison (Apr 08 2019 at 12:18):

I know that mathlib doesn't like examples, but I'm happy that the definition

noncomputable def presheaf_of_complex_functions (Y : Top) : presheaf_on_space CommRing Y :=
presheaf_of_functions_to_TopCommRing Y TopCommRing.complex

works. :-)

view this post on Zulip Kevin Buzzard (Apr 09 2019 at 09:17):

This message is just sitting in a separate browser tab waiting to be read. What is happening here? Is this the presheaf of rings corresponding to complex-valued functions on Y?

view this post on Zulip Scott Morrison (Apr 09 2019 at 10:32):

Yes.

view this post on Zulip Scott Morrison (Apr 09 2019 at 10:32):

It works for functions to any topological commutative ring.

view this post on Zulip Kevin Buzzard (Apr 09 2019 at 10:36):

OK you get my emoji :-) Are they continuous functions or all functions? Proving that it is a sheaf of rings should be straightforward I guess, once the definitions are there; the necessary topology lemmas ("continuity is local") are almost certainly in mathib (and might well be trivialities if you can drive the filter machine)

view this post on Zulip Scott Morrison (Apr 09 2019 at 10:37):

Continuous functions

view this post on Zulip Kevin Buzzard (Apr 09 2019 at 10:37):

you always have to check this sort of thing in this place ;-)

view this post on Zulip Scott Morrison (Apr 09 2019 at 10:38):

I still don't have a good version of the sheaf condition handy. I've tried several times and each time ended up with gross definitions.

view this post on Zulip Kevin Buzzard (Apr 09 2019 at 10:38):

Part of me wants to start going on about axiomatising Grothendieck topologies and doing it that way

view this post on Zulip Kevin Buzzard (Apr 09 2019 at 10:39):

and part of me knows that sometimes the most general way of thinking about things might not be the most sensible (although it can be!)

view this post on Zulip Johan Commelin (Apr 09 2019 at 10:56):

Part of me wants to start going on about axiomatising Grothendieck topologies and doing it that way

Yay, let's go for it! (After the perfectoid project)


Last updated: May 14 2021 at 18:28 UTC