Redefining Sheaves

Stream: maths

[Adam Topaz]

I have found it fairly annoying working with Sheaf J A as it's currently defined docs#category_theory.Sheaf and I'm fairly certain the source of the issues come from the fact that Sheaf J A is defined as the subtype {P : Cᵒᵖ ⥤ A // presheaf.is_sheaf J P}. Lean is happy to dsimplify P.val to ↑P, and that makes it difficult for automation to work.

So, I would like to redefine Sheaf J A as

structure Sheaf :=
(to_presheaf : Cᵒᵖ ⥤ A)
(condition : presheaf.is_sheaf J to_presheaf)

with no additional coercions, so that we can have more precise control for when a sheaf is considered as a presheaf.

Another question is whether we want morphisms of sheaves to be defined as natural transformations or as something like this:

structure hom (X Y : Sheaf J A) :=
mk :: (presheaf_hom : X.to_presheaf ⟶ Y.to_presheaf)

Again, I think it could be useful to have more precise control for deciding when a morphism of sheaves should be seen as "just" another natural transformation.

What do people think about this?

[Adam Topaz]

Ping @Johan Commelin @Andrew Yang @Bhavik Mehta @Scott Morrison

[Johan Commelin]

I agree. The only downside is that to_presheaf is pretty long.

[Johan Commelin]

Maybe reusing val as the field name isn't too evil?

[Adam Topaz]

Sure, val is fine. What do you think about redefining the morphisms as well? I'm less convinced about that

[Bhavik Mehta]

I'm not opposed to either of these changes, but I wonder if what you want can be achieved in a simpler way. For instance, we had the change of fin being defined as a structure to a subtype, and this is essentially the reverse direction. I'm actually slightly more convinced about the morphisms change (it might even be a good idea for subcategories in general?)

[Justus Springer]

This has been discussed shortly in my PR #9607, where I changed the definition of a sheaf on a topological space into a subtype. I have also found the distinction between morphisms of presheaves vs morphisms of sheaves a bit annoying in the past. Maybe having more precise control over the coercions will make it better.

[Justus Springer]

If you redefine sheaves on sites in that way, sheaves on spaces should probably be changed as well. Better still, sheaves on spaces should finally be defined as a special case of sheaves on sites. But this might be a slightly bigger project, I'm not sure. Note that I connected the sheaf conditions on either side to each other back in #9609.

[Adam Topaz]

As far as I can tell, the coercion from Sheaf J A to C\op \func A in this case only causes pain with essentially no gain. And since we have a dsimp lemma which will always trigger to change S.val to ↑S, we would not be able to, for example, use S.val in statements of theorems if we then want to freely use dsimpin the proof. This is an issue if we want to write, e.g., S.val.map f or something like that. As far as I can tell, this means that we cannot use subtypes to define Sheaf J A if we want to avoid such problems.

[Bhavik Mehta]

Isn't this the same thing which happens with any subtype? Lemmas shouldn't be written in terms of S.val, but instead in terms of the coercion, and then dsimp doing that conversion won't be an issue

[Adam Topaz]

I don't think ↑S.map f works.

[Bhavik Mehta]

(S : C\op \func A).map f does - and this is the usual pattern across mathlib for subtypes

[Johan Commelin]

Yeah, that means we would have to duplicate a bunch of presheaf-API for sheaves.

[Johan Commelin]

That might be the cleanest option. But it's also a lot of repetition. Pretty non-DRY

[Bhavik Mehta]

It might also mean we'd duplicate a bunch of subtype-API for sheaves (again comparing to the fin change)

[Adam Topaz]

Johan Commelin said:

Yeah, that means we would have to duplicate a bunch of presheaf-API for sheaves.

No it doesn't. If you want to use the presheaf API, you would write F.val.

[Johan Commelin]

I meant that if we want to keep using subtypes, then it might make sense to do

def sheaf.map (F : sheaf J D) := F.val.map

etc...

[Adam Topaz]

Let's take a vote...

[Adam Topaz]

(how do you make polls again?)

[Adam Topaz]

/poll
Redefine Sheaf as a structure, leave morphisms of sheaves as is
Leave Sheaf as a subtype, redefine morphisms as a structure
Redefine Sheaves and morphisms of sheaves as structures
Leave everything alone

[Adam Topaz]

I messed up

[Alex J. Best]

It definitely seems to me that making automation work better / finding workarounds is better long-term than defining bespoke subtypes every time we hit an issue with them. But as I haven't tried using sheaves I don't actually feel qualified to vote lol

[Adam Topaz]

Alex I think this is a pretty special case, because we already have a lot of automation built up for functors.

[Adam Topaz]

/poll Redefining Sheaves
Redefine Sheaf as a structure, leave morphisms of sheaves as is
Leave Sheaf as a subtype, redefine morphisms as a structure
Redefine Sheaves and morphisms of sheaves as structures
Leave everything alone

[Johan Commelin]

I vote for "all or nothing"

[Alex J. Best]

If there is only one simp lemma that is annoying does adding local attribute [-simp] subtype.val_eq_coe whenever the automation fails help? Or is there more to the Sheaf as subtype issue?

[Adam Topaz]

So you propose to add that local attribute to every file that involves sheaves?

[Alex J. Best]

Well only those where automation fails I suppose. But I don't know the explicit examples you do, so I have no idea how widespread the issue is

[Adam Topaz]

(deleted)

[Adam Topaz]

Sorry, that was my mistake

[Adam Topaz]

Option 5: Redefine full subcategories in general:

import category_theory.full_subcategory

open category_theory

variables {C : Type*} [category C]

structure full_subcategory (P : C → Prop) :=
(val : C)
(prop : P val)

namespace full_subcategory

@[ext]
structure hom {P : C → Prop} (X Y : full_subcategory P) :=
mk :: (val : X.val ⟶ Y.val)

@[simps]
instance category {P : C → Prop} : category (full_subcategory P) :=
{ hom := hom,
  id := λ X, ⟨𝟙 _⟩,
  comp := λ X Y Z f g, ⟨f.val ≫ g.val⟩ }

#check @full_subcategory.category_id_val
/-
category_id_val :
  ∀ {C : Type u_3} [_inst_1 : category_theory.category C] {P : C → Prop} (X : full_subcategory P),
    (𝟙 X).val = 𝟙 X.val
-/

#check @full_subcategory.category_comp_val
/-
category_comp_val :
  ∀ {C : Type u_3} [_inst_1 : category_theory.category C] {P : C → Prop} (X Y Z : full_subcategory P) (f : X ⟶ Y)
  (g : Y ⟶ Z), (f ≫ g).val = f.val ≫ g.val
-/

@[simps]
def inclusion {P : C → Prop} : full_subcategory P ⥤ C :=
{ obj := λ X, X.val,
  map := λ X Y f, f.val }

#check @inclusion_obj
/-
inclusion_obj :
  ∀ {C : Type u_3} [_inst_1 : category_theory.category C] {P : C → Prop} (X : full_subcategory P),
    inclusion.obj X = X.val
-/

#check @inclusion_map
/-
inclusion_map :
  ∀ {C : Type u_3} [_inst_1 : category_theory.category C] {P : C → Prop} (X Y : full_subcategory P) (f : X ⟶ Y),
    inclusion.map f = f.val
-/

end full_subcategory

[Adam Topaz]

I've opened a PR that cleans up some of the simps involved with sheaves here #10574
Note that I had to add

@[simp] lemma id_app (X : Sheaf J A) (B : Cᵒᵖ) : (𝟙 X : X ⟶ X).app B = 𝟙 _ := rfl
@[simp] lemma comp_app {X Y Z : Sheaf J A} (f : X ⟶ Y) (g : Y ⟶ Z) (B : Cᵒᵖ) :
  (f ≫ g).app B = f.app B ≫ g.app B := rfl

which dsimp, simp was not able to close. I think this is a first example of what @Johan Commelin was mentioning above regarding needing to copy some of the API for functors, which I don't think is very ideal.

[Adam Topaz]

I ran into yet another annoying issue in LTE regarding the current deffinition of the category of sheaves. I added a comment here:
https://github.com/leanprover-community/lean-liquid/blob/890de421fb657301057d418f6a19085b7e2494cb/src/condensed/adjunctions.lean#L58

And this prompted me to actually write a PR redefining sheaves per the discussion above -- #10678

I tagged this as RFC for now. Please let me know what you think!

[Adam Topaz]

Just a remark: The simp_nf linter failed on this commit
https://github.com/leanprover-community/mathlib/pull/10678/commits/a236c2c04eb3522f45d8265eb9b1b5308033d668
I think this is a good sign, because it means that simp is able to now do more work with this change.

[Adam Topaz]

:ping_pong: Any further thoughts about this?

[Johan Commelin]

Looks fine to me. But I'll ping @Andrew Yang @Bhavik Mehta and @Justus Springer for their thoughts.

[Adam Topaz]

Since the linkifier is broken, here is the link to the PR:
https://github.com/leanprover-community/mathlib/pull/10678

[Bhavik Mehta]

Bhavik Mehta said:

I'm not opposed to either of these changes, but I wonder if what you want can be achieved in a simpler way. For instance, we had the change of fin being defined as a structure to a subtype, and this is essentially the reverse direction. I'm actually slightly more convinced about the morphisms change (it might even be a good idea for subcategories in general?)

I still have this concern; this PR does the exact opposite of the fin refactor. I don't see a way this new approach avoids re-duplication of subtype API and presheaf API

[Adam Topaz]

But what part of the subtype API do you actually want in this case?

[Adam Topaz]

Remember that you shouldnt be evil and talk about equality of sheaves

[Adam Topaz]

And if you want to view a sheaf as a presheaf, just write F.val, just like you had to before, except now lean wouldn't get confused if you apply dsimp which currently applies lemmas from the subtype API that cause various annoyances in proofs.

[Adam Topaz]

I guess one of the main points of this PR is that I think the subtype API only causes pain in this case. I can't think of anything that I want from the subtype API in this context.

[Johan Commelin]

I think we should move forward with this PR. I agree with @Adam Topaz that the subtype API seems less useful in this specific case (put mildly). @Bhavik Mehta do you have further concerns? Otherwise I would like to merge the PR

[Bhavik Mehta]

Let's go with it and see what happens!

[Markus Himmel]

I will need to be able to work with several subcategories of the category of functors and how they relate, and for that I think it is still useful to have a unified development of full subcategories instead of a hand-rolled structure approach like the one introduced in #10678. For this reason, I will attempt to refactor the definition of full_subcategory as suggested by Adam above. If you have any objections, please let me know.

[Antoine Chambert-Loir]

A remark from an outsider. Some mathematicians claim that categories/functors are all over the place and that it is the right (and only right) way to proceed, but most of them do it appropriately lazily enough (forgetting about forgetful functors all over the place, for example). For a large scale formalization process, thinking categorically has advantages since it makes a lot of the constructions systematic. I guess it would be fruitful to gather pros and cons, and regarding cons, it would probably be fruitful to think about how to circumvent them systematically. Maybe, for particular categories, one would realize that they were not properly defined (such as filters, as Johann, Kevin and Patrick did) and this would lead to a (essentially equivalent but slightly) better definition, at least to a better understanding.

[Patrick Massot]

For the record: Johan, Kevin and I have nothing to do with the definition of filters in mathlib. Filters were defined in mathlib by Johannes Hölzl in the very first months, ported from Isabelle/HOL (see https://link.springer.com/chapter/10.1007/978-3-642-39634-2_21)

[Markus Himmel]

Markus Himmel said:

I will need to be able to work with several subcategories of the category of functors and how they relate, and for that I think it is still useful to have a unified development of full subcategories instead of a hand-rolled structure approach like the one introduced in #10678. For this reason, I will attempt to refactor the definition of full_subcategory as suggested by Adam above. If you have any objections, please let me know.

I finally got around to this and opened #14767. For now, I only put the objects in a custom structure and left morphisms. I tried also putting the morphisms in a separate structure (already on the level of induced_category) as is currently done for sheaves, but I ran into two issues:

1. Apparently some uses of the bundled framework can lead to some concrete categories being created through multiple levels of induced_category, which means you have to write things like f.val.val to get hold of the actual map.
2. If x is a point of a topological space X, then the preorder category open_nhds x is a full_subcategory of the preorder category opens X. If we create a structure for the morphisms in a full subcategory, then open_nhds x has two non-defeq category structures, which causes issues.