## Stream: maths

### Topic: presheaves

#### 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. :-)

#### 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?

Yes.

#### Scott Morrison (Apr 09 2019 at 10:32):

It works for functions to any topological commutative ring.

#### 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)

#### Scott Morrison (Apr 09 2019 at 10:37):

Continuous functions

#### Kevin Buzzard (Apr 09 2019 at 10:37):

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

#### 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.

#### 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

#### 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!)

#### 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