open_set

Stream: maths

[Reid Barton]

@Scott Morrison I'm curious why you reversed the direction of the arrows of open_set. I would rather put the contravariant-ness in the notion of (pre)sheaf.

[Scott Morrison]

Ah, I hadn't seen this, and asked your opinion elsewhere. I'll reverse it again when I get there.

[Kevin Buzzard]

Yes Scott mentioned this before I think. Maybe he said something like he had ops everywhere at all times with no obvious purpose?

[Kevin Buzzard]

I guess the point is that we never use the unopped category

[Johan Commelin]

Right, but once we start doing sheaves over sites we will want contravariant (pre)sheaves. And we also want those to specialise to "plain old" (pre)sheaves on open sets. So I vote for keeping the op.

[Kevin Buzzard]

Another question of course is where you want the op -- source or target. It's funny this is coming up now. I distinctly remember Scott saying "eew there are ops everywhere, but I've had a brilliant idea -- if we just redefine the open set category then they all go away and it's much easier to use" and it was one of those moments where I just thought "yeah, it's not ideal but I can completely see his point. It removes all of them at once."