Refactoring sheaves

Stream: general

[Andrew Yang]

Now that sheaves over sites has a rich and useful API, I think it is increasingly favorable that we switch the "official definition" of sheaves over topological spaces to be the one in terms of grothendieck topologies. This switch was also briefly discussed in this topic. The main pros are

1. The X.Sheaf C category is now defeq to (opens.grothendieck_topology X).Sheaf C, so that functors between categories of sheaves over sites (and other categorical results) could be specialized onto topological spaces without the abundant equivalences.
2. It allows sheaves over spaces to value in arbitrary categories that doesn't have all products.

Some changes / cons are

1. (I saw someone mention this elsewhere) People would need to know what sites are before using it. But this could be solved by sufficient documentation.
2. For F : X.sheaf C, F.1 now has the type of a functor, and we need F.presheaf to access the dot notation, but I think writing out the explicit projection is favored in mathlib nonetheless.
3. X.sheaf C is no longer a subtype of X.presheaf C, but following the arguments of making Sheaf not a subtype, I think this is a conscious and appreciated change.

There is also a draft PR #15384 which builds but still fails lint (mainly because [has_products C] is no longer nessecary) and lacks documentation if one would like to see how the switch went.

[Sam van G]

From my experience with @Jake Levinson formalizing some things this past week, I think it is really important, if such a refactoring is made, that there is a very good API that allows someone who doesn't know what a site is to pretend they are working with a topological space, with the "backend" doing the work of creating the relevant site, canonical Grothendieck topology on that site, showing that a sheaf in the topology sense is the same as a sheaf in the Grothendieck sense, etc.

[Sam van G]

On a related, but different topic, also regarding the appropriate level of generality in the definition of sheaf: we ran into quite some trouble with forgetful functors and the category C. I am worried that con (3) in Andrew's comment above might lead to similar problems but I may be wrong, I can't truly assess that.
In our PR #15398 we tried to address this by introducing some notation, but with limited success. If anyone who knows the category theory part of the library better than we do can show how to make the transition from object of C to underlying set here and here less painful, that would be great.

[Sam van G]

Tagging @Johan Commelin @Scott Morrison @Nikolas Kuhn in case they want to weigh in (my point of view may very well be too naive or I may be misunderstanding how to use the category part of the library correctly)

[Adam Topaz]

@Sam van G can you explain what troubles you are referring to with forgetful functors?

[Sam van G]

It is explained in detail in Jake's two comments on our PR: https://github.com/leanprover-community/mathlib/pull/15398/files

[Adam Topaz]

Hmmm.... it seems that you're not really using the whiskering api we have set up for sheaves.

[Adam Topaz]

We still don't have the general notion of stalks for sheaves on sites (e.g. w.r.t. topos-theoretic points, or something similar)

[Adam Topaz]

That's one important point that's missing from the sheaves-on-sites part of the library

[Jake Levinson]

I could definitely believe that we overlooked or misunderstood part of the API. (I remember seeing the word whiskering but not knowing what it meant.)

[Jake Levinson]

That said, everything seemed to work fine until those last two lines of the proof, when we weren’t able to easily deal with the (forget C).map applications.

[Adam Topaz]

We have a good API for filtered colimits of concrete categories. presumably that would help here.

[Adam Topaz]

That's pretty cool notation!

[Adam Topaz]

Okay, your last 4 lines

change (((forget C).map _) ≫ ((forget C).map _)) s =
(((forget C).map _) ≫ ((forget C).map _)) s,

rw ← (forget C).map_comp,
rw ← (forget C).map_comp,
rw T.naturality,

can be changed to

dsimp [map_on_sections, restrict_along],
simp only [← comp_apply, nat_trans.naturality],

[Adam Topaz]

And your last few lines in the other direction can be proved using

dsimp only [map_on_sections, forget_map_eq_coe] at h_eq,
rw h_eq,
dsimp only [Top.presheaf.germ],
let ι' : (⟨V,hxV⟩ : open_nhds x) ⟶ ⟨U,hxU⟩ := ι,
erw [← limits.colimit.w _ ι'.op, comp_apply], refl,

[Adam Topaz]

It seems that there is some API missing here. The API around germ is done for any category C essentially by using the colimit api, but now you're using it on elements when you have a concrete category, so there is some back-and-forth that needs to happen when you apply a composition of moprhisms.

[Jake Levinson]

Awesome! We’ll make those edits. If you can think of any API additions you think we should add in this same PR, we’d be happy to extend it.

[Jake Levinson]

@Sam van G

[Adam Topaz]

One sec I think I can clean up the second block

[Adam Topaz]

Okay here's the complete proof with the new finishing lines

/-- Being locally surjective is equivalent to being surjective on stalks. -/
lemma locally_surjective_iff_surjective_on_stalks (T : ℱ ⟶ 𝒢) :
  is_locally_surjective T ↔ is_surjective_on_stalks T :=
begin
  split; intro hT,
  { /- human proof:
    Let g ∈ Γₛₜ 𝒢 x be a germ. Represent it on an open set U ⊆ X
    as ⟨t, U⟩. By local surjectivity, pass to a smaller open set V
    on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
    Then the germ of s maps to g -/

    -- Let g ∈ Γₛₜ 𝒢 x be a germ.
    intros x g,
    -- Represent it on an open set U ⊆ X as ⟨t, U⟩.
    rcases 𝒢.germ_exist x g with ⟨U, hxU, t, rfl⟩,
    -- By local surjectivity, pass to a smaller open set V
    -- on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
    rcases hT U t x hxU with ⟨V, ι, hxV, s, h_eq⟩,

    -- Then the germ of s maps to g.
    use (forget C).map (ℱ.germ ⟨x, hxV⟩) s,
    convert Top.presheaf.stalk_functor_map_germ_apply V ⟨x, hxV⟩ T s,

    -- New finish
    dsimp only [map_on_sections, forget_map_eq_coe] at h_eq,
    erw [h_eq, ← comp_apply, 𝒢.germ_res], refl },

  { /- human proof:
    Let U be an open set, t ∈ Γ ℱ U a section, x ∈ U a point.
    By surjectivity on stalks, the germ of t is the image of
    some germ f ∈ Γₛₜ ℱ x. Represent f on some open set V ⊆ X as ⟨s, V⟩.
    Then there is some possibly smaller open set x ∈ W ⊆ V ∩ U on which
    we have T(s) |_ W = t |_ W. -/
    intros U t x hxU,

    set t_x := (forget C).map (𝒢.germ ⟨x, hxU⟩) t with ht_x,
    obtain ⟨s_x, hs_x : (T _ₛₜ x) s_x = t_x⟩ := hT x t_x,
    obtain ⟨V, hxV, s, rfl⟩ := ℱ.germ_exist x s_x,
    -- rfl : ℱ.germ x s = s_x
    have key_W := 𝒢.germ_eq x hxV hxU (T _* s) t
      (by { convert hs_x,
            symmetry,
            convert Top.presheaf.stalk_functor_map_germ_apply _ _ _ s, }),
    obtain ⟨W, hxW, hWV, hWU, h_eq⟩ := key_W,
    refine ⟨W, hWU, hxW, ⟨s |_ hWV, _⟩⟩,
    convert h_eq,

    -- New finish
    dsimp [map_on_sections, restrict_along],
    simp only [← comp_apply, nat_trans.naturality],
    },
end

Using erw is not ideal -- that usually means that there is some missing dsimp lemma.

[Adam Topaz]

Hmm... on second thought it looks like all these defs/notations are just preventing the appropriate simp lemmas from firing.

[Sam van G]

Thanks Adam!! This is already a huge improvement.

[Sam van G]

Re your last comment, I may remember wrong and am not on computer right now but I think at one point yesterday @Jake Levinson and I had the same thought and tried to just copy in the definitions for the notations and it did not help. Will check this later.

[Jake Levinson]

Should we mark those definitions reducible or something?

[Adam Topaz]

I think the best approach would be to make the notation directly using the existing API without making any new defs

[Adam Topaz]

I'm no expert in making notation, so hopefully someone else can help with that

[Jake Levinson]

Oh I see. We can experiment a bit, defining the notation directly. The notation definitely made parts of the proof easier to think through, so it would be nice to keep it in some form.

[Adam Topaz]

I agree the notation is very nice, but I think having working simp lemmas would be nicer ;)

[Adam Topaz]

it would be great if we can have both!

[Adam Topaz]

Here's a version of the file with all the notation and defs removed (plus some tricks using instances for concrete categories):
https://gist.github.com/adamtopaz/802c0ad2491ef63e37b0d040d85e9eef

[Andrew Yang]

@Sam van G Regarding your first comment, Is an iff rewriting the new sheaf condition with the old sheaf condition enough?
If one really doesn't want to go near sites, one could rewrite it whenever they really want to use the sheaf condition.

[Adam Topaz]

I think the bigger issue would be with sheafification.

[Andrew Yang]

By this, do you mean that people working on sheaves over spaces would want sheafifications with a better underlying implementation?

[Adam Topaz]

I just mean that the current def of the non-sites shrafification uses this disjoint union of stalks. So if someone wants to rely on this precise construction, they would have to deal with isomorphisms to go back and forth with the site-theoretic definition

[Adam Topaz]

It's not that bad though. I don't think we have any defeq abuse in this part of the library.

[Adam Topaz]

In any case, I'm 100% in favor of the refactor that you suggested (obviously ;-) )

[Sam van G]

It is fundamental for algebraic geometry to be able to switch seamlessly between sheaf-as-functor-on-opens and sheaf-as-bundle-of-stalks. If this requires passing through an isomorphism every time you do it, I am worried it would add a layer of complication to the already pretty complicated API. So for being able to do some algebraic geometry, I personally would be more interested in making the existing sheaf on space more easily usable before trying to generalize.
As an alternative option, couldn’t one begin by making a separate notion called sheaf_on_site, leaving the current notion of sheaf on space untouched, and then prove that the current notion is a special case of the newly defined sheaf_on_site? (This may be a somewhat non trivial exercise in itself.)

[Andrew Yang]

The non-sites sheafification only applies to Types, and it has little API, so I don't think people should be encouraged to use that.
In most cases people only only want a left adjoint to the forgetful functor, and in cases where people need the description on elements, knowing that the to sheafification map is_locally_surjective should be enough.

[Andrew Yang]

The alternative approach is probably the current approach?
The current approach is that A presheaf is a functor on opens, and is_sheaf is a predicate on it.
A sheaf is just a bundled functor with the is_sheaf predicate.
We have a definition of sheaves on sites and sheaf on spaces, the difference is that the is_sheaf is different, but the presheaf is the same thing.

What I am proposing is replacing the is_sheaf of spaces with the equivalent is_sheaf of sites. The functor should remain unchanged.

[Sam van G]

I’m not so sure about that, it seems to me that there are several other local properties of sheaves beyond just local surjectivity that will require speaking about the description on stalks on the Set/Type level.
But I will now leave it to others with more experience in (formalizations of) algebraic geometry to comment on that.

[Adam Topaz]

Sam van G said:

As an alternative option, couldn’t one begin by making a separate notion called sheaf_on_site, leaving the current notion of sheaf on space untouched, and then prove that the current notion is a special case of the newly defined sheaf_on_site? (This may be a somewhat non trivial exercise in itself.)

See docs#Top.presheaf.Sheaf_spaces_equiv_sheaf_sites

[Andrew Yang]

We already have a substantial API around stalks of sheaves independent of the sheafification stuff, and I believe that is enough?

[Adam Topaz]

Do we have the sheafification adjunction for the topological sheafification? I don''t see it in topology/sheaves/sheafify

[Adam Topaz]

If we have that, then we would get the isomorphism with the site-theoretic sheafification (compatibly with the adjunction) for free

[Andrew Yang]

No we don't. That file is all we have got for topological sheafifications, and no other file imports it.

[Jake Levinson]

Maybe that could be another short-term goal.

[Andrew Yang]

My stance is that we wouldn't need two versions of sheafification, but others may very well disagree.
IMHO an isomorphism as sheaves between them as a sanity check suffices.
I think the isomorphism would be more easily shown by

1. the descent of an injective presheaf morphism onto its sheafification is injective.
2. If f >> g is surjective, then so is g.
3. An injective and surjective morphism between sheaves is bijective.
4. The topological sheafification map is both injective and surjective.
   Also, the first three results are all useful and important on its own.

[Jake Levinson]

@Adam Topaz , thanks so much for those nice proofs. I'm still fiddling with the file to get the hang of what you did. When I make a new commit, how do I acknowledge you? In the commit message I guess?

Regarding notation: those two lines

local attribute [instance] concrete_category.has_coe_to_fun
local attribute [instance] concrete_category.has_coe_to_sort

definitely make things easier to read and write. Is there a way to also coerce opens X into (opens X).op? or coerce the sheaf-related functions to take objects and morphisms from opens X? I imagine this is some broader question about contravariant functors, so maybe there's some reason why this isn't doable. But, it is confusing to have to write .op everywhere.

On another note, I think it can be easy to forget how illegible these extra layers of abstraction and notation are, after you've gotten used to them. Actually, the reason @Sam van G and I introduced those other notations in the first place is because, after reading topology/presheaf.lean and stalks.lean and so on, we still couldn't figure out how to write down the relevant variables for is_locally_surjective (which after all involved all the main sheaf-related objects: sections, germs, restriction maps, induced maps). We definitely found s : (forget C).map (ℱ.obj (op U)) harder to read than s : Γ_ ℱ U, never mind a statement involving several of these objects. I think it would have been harder still if we had also had to unpack from sheaves on sites to sections on open sets.

Generalizing to Grothendieck topologies might well make it easier to prove more categorical facts about sheaves. But will it make it harder to (e.g.) describe the structure sheaves and modules of varieties and schemes? What about proving local properties by passing to a local ring and using Nakayama's lemma? Or doing some kind of local calculation involving actual polynomials?

I can recognize that presumably all of this stuff would be recoverable by specializing back to the ordinary Zariski topology, and I don't want to get in your way in developing this part of the library. Still, I am probably not the only algebraic geometer who barely knows what a Grothendieck topology is, so it would at least make it harder for me to use this library.

[Andrew Yang]

No matter the sheaf condition is stated in terms of sieves or open covers, a presheaf will always be a (opens X)ᵒᵖ ⥤ C, and this refactor won't any difference in manipulating the elements on the presheaf. By checking the diff of the draft PR #15384, I think it should be evident that this PR is not as intrusive as you seem to imagine.

[Adam Topaz]

Jake Levinson said:

When I make a new commit, how do I acknowledge you? In the commit message I guess?

Oh, don't worry about it. I was happy to help!

The issue with op is indeed annoying, but there is really no good way around it (as far as I know). You may just need to learn to live with op and unop.

We have the sheaf condition in terms of multiequalizers which should reduce directly to the usual sheaf condition on topological spaces. Maybe I'll try to write down a PR doing this later today.

[Andrew Yang]

On the other hand, the I agree that the type signatures are not that illegible. I think an idea worth exploring is to make a has_sections type class that enables a notation like Γ(_, _) so that we could write Γ(ℱ, U) for sheaves and presheaves, as well as Γ(X, U) for ringed spaces and schemes etc In place of foo.presheaf.obj (op bar)

[Jake Levinson]

I have tried to write a bit on functoriality of sheafification. I managed to show that sheafification is functorial, but my proof isn't very nice. Here's what I added in topology/sheafify.lean (https://github.com/leanprover-community/mathlib/blob/d8974a346b09e05ad7f36c8200037521b7e076f6/src/topology/sheaves/sheafify.lean#L129):

variables {F} {G : presheaf (Type v) X}

def sheafify_map (T : F ⟶ G) : F.sheafify ⟶ G.sheafify :=
{ app := λ U f,
    ⟨λ x, (stalk_functor _ x.1).map T (f.1 x),
     λ x, begin
      obtain ⟨V, hxV, ι, ⟨f', hf'⟩⟩ := f.2 x,
        -- notice that ι : V ⟶ unop U, I'm not sure why the API is mixing
        -- (opens X) and (opens X)ᵒᵖ here...
      refine ⟨V, hxV, ι, _⟩,
      exact ⟨T.app _ f', λ x',
      begin
        simp only [subtype.val_eq_coe] at ⊢ hf', rw hf',
        exact stalk_functor_map_germ_apply V x' T f',
      end⟩,
    end⟩,
  naturality' := λ U V res, begin
    ext f x,
    simp only [category_theory.types_comp_apply, subtype.coe_mk],
    change _ = (stalk_functor (Type v) x.val).map T _,
    congr,
  end, }

lemma sheafify_id (F : X.presheaf (Type v)) :
  sheafify_map (𝟙 F) = 𝟙 F.sheafify :=
begin
  ext U f x,
  unfold sheafify_map, simp,
end

lemma sheafify_comp {F G H : X.presheaf (Type v)} (T1 : F ⟶ G) (T2 : G ⟶ H) :
  sheafify_map (T1 ≫ T2) = sheafify_map T1 ≫ sheafify_map T2 :=
begin
  ext U f x,
  unfold sheafify_map, simp,
end

def sheafification : presheaf (Type v) X ⥤ sheaf (Type v) X :=
{ obj := λ F : presheaf (Type v) X, F.sheafify,
  map := λ F G T, sheafify_map T,
  map_id' := sheafify_id,
  map_comp' := λ _ _ _ T1 T2, sheafify_comp T1 T2, }

It took me a while to figure out how to formulate the objects in question, and at some point I also found myself with a mix of opens X and (opens X)ᵒᵖobjects, which is a sign that I am using the API wrong. I guess I am still trying to write with sets and functions rather than the categorical language.

With this the adjunction shouldn't be too bad either, since the lemma sheafify_stalk_iso should make it easy to show that when G is a sheaf, the natural map G ⟶ G.1.sheafifyis an isomorphism.

[Jake Levinson]

I'm imagining that the adjunction would be formulated as T : F ⟶ G.1 becomes something like (sheafify_map T) ≫ (G.sheafify_equiv.to_inv_fun) : F.sheafify ⟶ G and conversely T : F.sheafify ⟶ G just goes to F.to_sheafify ≫ T : F ⟶ G.1.

[Andrew Yang]

The refactor #15384 is now ready for review.