pushforward/pullback of sheaves

Stream: Is there code for X?

[Kevin Buzzard]

Can we push forward or pull back a sheaf of abelian groups on a topological space, along a morphism of topological spaces?

[Scott Morrison]

https://leanprover-community.github.io/mathlib_docs/topology/sheaves/functors.html

[Scott Morrison]

So only forward, I think.

[Andrew Yang]

We do have docs#category_theory.sites.pushforward, but it is not yet specialized onto topological spaces.

[Andrew Yang]

(it is called pushforward since the direction of X ⟶ Y and opens Y ⥤ opens X are reversed.)

[Kevin Buzzard]

Thanks for these. I'm still finding my way around the library, I don't know whether I should be thinking about sites or topology. Is the philosophy that we should do everything with sites really, and then specialise to topological spaces when necessary?

[Kevin Buzzard]

At the end of the day I'm interested in schemes with the zariski topology, and we have ringed spaces but as far as I know we don't have ringed sites.

[Andrew Yang]

I don't think we are fully committed into sites and I don't think we need to for the time being.

[Kevin Buzzard]

So you're suggesting that we don't worry about eg the etale site and just worry about doing stuff like pushing forward and pulling back sheaves of modules using topological spaces first?

[Junyan Xu]

We have docs#Top.presheaf.pushforward_pullback_adjunction for presheaves on topological spaces which specializes docs#category_theory.Lan.adjunction, but we don't have the adjunction between categories of sheaves (for sites or for spaces). Maybe that exists in LTE? We only have docs#Top.presheaf.sheafify for sheaves in Type* but not in a general category, so we should probably use the sites API for sheafification.

[Andrew Yang]

My take is that it would be great if things are done in the generality of sites, but it is not obligatory. For example, we probably won't replace our current stalk library in favour of stalks on topos points in the near future.

[Andrew Yang]

We do have adjunction between sheaf categories at docs#category.sites.pullback_pushforward_adjunction, and I've just specialized it into spaces in #17561.

[Andrew Yang]

And we probably should specialize the sheafification stuff into sheaves over spaces.
I think it would be a good idea to redefine has_sheafification J K A to mean that is_right_adjoint (Sheaf_to_presheaf J K A) and make the current definition into an instance. Although I don't know any other cases where there exists a sheafification, at least it would be nice if we don't have to remember the magic spell below to do sheafification every time.

  [limits.preserves_limits (forget A)]
  [reflects_isomorphisms (forget A)]
  [Π (X : C), limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (forget A)]
  [∀ (X : C), limits.has_colimits_of_shape (J.cover X)ᵒᵖ A]
  [Π (X : D), limits.preserves_colimits_of_shape (K.cover X)ᵒᵖ (forget A)]
  [∀ (X : D), limits.has_colimits_of_shape (K.cover X)ᵒᵖ A]

[Adam Topaz]

This magic spell will be a non-issue when we switch to Lean4, since it would be very easy to write a macro that expands to this collection of assumptions. If people don't want to wait, then introducing such a has_sheafification would be a good idea IMO. One case which isn't directly covered by this magic spell is when you have a collection of functors which satisfy the (co)limit preservation requirements but which only jointly reflect isomorphisms, but I can't think of an example where this shows up in practice.