Opposite category in TopCat/Presheaf

Stream: new members

[Arnoud van der Leer]

Hi, I mostly work in UniMath (coq) for now, but I keep an eye on some relevant parts of mathlib. This caused me to wonder: Why is a presheaf defined as a functor from the * opposite category * of the "topological space category"?

/-! We define `TopCat.Presheaf C X` simply as `(TopologicalSpace.Opens X)ᵒᵖ ⥤ C`, -/

and

/-! Since `Opens X` has a partial order, it automatically receives a `Category` instance. -/

I guess that is the reason why we need to take the opposite category. But I would assume that

• The partial order is a somewhat arbitrary choice. One can also define A < B to mean that A contains B (although, I admit, that this does look a bit weird).
• The additional .op everywhere might cause some trouble in the long run.
• One could also always work with (TopologicalSpace.Opens X) ⥤ Cᵒᵖ instead of (TopologicalSpace.Opens X)ᵒᵖ ⥤ C, right?

What is the reasoning behind this choice? Is this maybe deliberately done this way to make sure that a presheaf is also a presheaf in the category theoretical sense? Wouldn't it be easier to define another category here, with A -> B to mean that A contains B, and then use that to define the presheaf?

[Joël Riou]

Firstly, a choice had to be made! Secondly, in the mathematical literature, most authors consider "contravariants functors from C to D" as functorsCᵒᵖ ⥤ D rather than C ⥤ Dᵒᵖ. Another argument is that (pre)sheaves on topological spaces are only a special of a more general construction. Then, the objects in the source category C usually have a geometric meaning, and the morphisms also have a geometric interpretation: indeed, if U and V are open subsets of X, and U is contained in V, there is a continuous map from U to V (and not from V to U).

[Arnoud van der Leer]

Fair. These seem like decent considerations. Thanks.