presheaves

Stream: maths

[Scott Morrison]

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]

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?

[Scott Morrison]

Yes.

[Scott Morrison]

It works for functions to any topological commutative ring.

[Kevin Buzzard]

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]

Continuous functions

[Kevin Buzzard]

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

[Scott Morrison]

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]

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

[Kevin Buzzard]

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]

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)