Grothendieck topologies from morphism properties

Stream: maths

[Ben Eltschig]

On any category $C$ with a terminal object $*$, you can define a Grothendieck topology by equipping each $X\in C$ with all sieves that contain all arrows $*\to X$. I'm interested in this topology because it is closely related to local sites and concrete sheaves, and would like to formalise it soon.

I've been thinking a bit about what the correct level of generality for this is - for example, you could replace $*$ in this definition with any other object, or even a collection of objects of $C$ - and it seems that the most general construction is actually one in terms of morphism properties: for any morphism property $A$ such that 1) $A$ is stable under composition with arbitrary morphisms from the right and 2) every morphism in $A$ can be written as the composition of two morphisms in $A$, the collection of all sieves that contain all possible morphisms in $A$ forms a Grothendieck topology on $C$. The Grothendieck topologies that arise in this way are precisely those for which each object has a minimal covering sieve, and it is possible to go the other way by taking the morphism property "is contained in all possible covering sieves" (recovering the original morphism property iff it was also stable under composition with arbitrary morphisms from the left).

How much of this do we want in mathlib? I only need the special case of morphisms from the terminal object, but we already have one construction of (pre)topologies from morphism properties in Mathlib.CategoryTheory.Sites.MorphismProperty, so it might also make sense to also add the general case of this construction there. I'm also curious if anyone has a reference for any of these topologies, or an idea for what they should be called; the only mention I've found is slide 9 here, which does not give a name.

[Matt Diamond]

I'm not familiar with this area but is this different from docs#CategoryTheory.GrothendieckTopology ?

[Ben Eltschig]

It is one specific construction of a docs#CategoryTheory.GrothendieckTopology :slight_smile: just like the cofinite topology would be one particular construction of a docs#TopologicalSpace

[Matt Diamond]

oh, gotcha

[Andrew Yang]

cc @Christian Merten

[Adam Topaz]

I think @Qi Ge has thought about such things before

[Filippo A. E. Nuccio]

And perhaps also @Dagur Asgeirsson and @Joël Riou .

[Christian Merten]

I am not familiar with this construction. Do you have any other applications of this topology in mind beyond your special case? And could you elaborate a bit on what your original use case is?

[Joël Riou]

If this is not too painful, I think it would make sense to have the general results in mathlib.

[Ben Eltschig]

Christian Merten said:

I am not familiar with this construction. Do you have any other applications of this topology in mind beyond your special case? And could you elaborate a bit on what your original use case is?

My original use case is that I want to define concrete sheaves (roughly "sheaves with an underlying set"); diffeological spaces are the main example I'm interested in, but simplicial complexes and quasi-topological spaces are also examples of concrete sheaves, so I think it's worth formulating this general notion. The correct setting for this seems to be local sites, sites with a terminal object on which the global sections functor to sets/types has a right adjoint, on which nlab defines sheaves to be concrete iff the unit of that adjunction is a monomorphism on them. The topology $J_*$ consisting of all sieves that contain all morphisms from the terminal object comes into play with the following two observations:

1. A site $(C,J)$ with a terminal object is local iff $J\subseteq J_*$,
2. A sheaf on a local site is concrete iff it is separated with respect to $J_*$.

That second point in particular means that concrete sheaves are a special case of biseparated presheaves. Quite a few things that are true of concrete sheaves are also true of biseparated sheaves - for example, that they form a quasitopos - so I think to do things in the correct generality, that's the better out of the two definitions of concrete sheaves to use.

Aside from this use of $J_*$ though, I don't know of any application of the more general construction of Grothendieck topologies in question.

[Ben Eltschig]

Joël Riou said:

If this is not too painful, I think it would make sense to have the general results in mathlib.

That's what I was thinking - it probably isn't much more effort than just defining the special case I care about, so I might as well do it. In some sense, the hardest part might be coming up with a good name - do you have any ideas? MorphismProperty.grothendieckTopology is already taken, and I imagine we want something more specific than MorphismProperty.grothendieckTopology' :sweat_smile:

[Christian Merten]

Ben Eltschig said:

In some sense, the hardest part might be coming up with a good name - do you have any ideas? MorphismProperty.grothendieckTopology is already taken, and I imagine we want something more specific than MorphismProperty.grothendieckTopology' :sweat_smile:

MorphismProperty.minimalTopology perhaps? Because among the topologies coarser than docs#CategoryTheory.MorphismProperty.grothendieckTopology, it is the one where every covering sieve is minimal.