Sheaves in Minecraft

I was a little thrown off by the model for a Minecraft world (subset of Z3*N is a bad model because it allows invalid worlds where two blocks occupy the same space. A better model is elements of N^Z3) but whatever.

And for the rest I struggled to motivate the definitions because it seemed something much simpler would do (the simple thing being something like “take the function f: B -> P(E) from the basis to sets of entities plus the injectivity-like condition that f(U) meets f(V) only if U=V, and then extend it to a function from the whole space in the obvious way”). Perhaps the machinery is only necessary when the topology is more interesting (the one in the article being a coarse discrete topology where everything is countable and countable intersections of open sets give open sets) or if the “data” has a more interesting structure than sets with inclusion.

I was also pretty confused about the need for F to be a functor. The article says it is a functor and then that it could be a function but also that it couldn’t. I found it most unclear. I think the article was trying to go on a counterfactual where F is not a functor, then define res_U^V and then reveal that it is just the image of the inclusion U->V under the functor, but it wasn’t clear to me which of its properties are just due to it being a functor and which are separate.

I was also thrown off by some errors (eg getting a subset relation the wrong way round) and I think the choice of variables was not great for subtle reasons:

1. I think it is often not great to have V’ < V (or vice versa) as I think there isn’t a natural order for the two names. Better to have something alphabetical like U < V or hierarchical like U_i < U. But this might just be my personal preference.

2. V was doing double-duty talking sometimes about elements in the domain of F and other times about elements in the image. I think it would be better if e.g. U was always in the domain and V in the image.

I also found the sentence structure confusing in a few cases but it may just be that I am not used to it. For example instead of “if x holds P(x) then Q(x)” I would have preferred “let x. If P(x) then Q(x)” or “given x such that P(x), we have Q(x).”

1. There appears to be a typo in the gluing axiom. The second half of the hypothesis should read

   res^{U_i}_{U_i ∩ U_j}(s_i) = res^{U_j}_{U_i ∩ U_j}(s_j)

2. I'm not confident on this (since I've never successfully understood what a sheaf is before), but I think the sets Γ(V,F) need to be defined as something like an indicator function over the domain of entities (or perhaps a counting function for the number of such entities), so you would actually want to say something like "the support of Γ(V,F)={p}" rather than "Γ(V,F)={p}". Maybe the latter is a standard shorthand for the former when working with this sort of thing, but as a non-expert, it took me a bit of thinking to figure out what the map res^V_V' was actually supposed to concretely be (f.ex. say V' is a chunk that doesn't contain our player. If Γ(V,F)={p}, then what is res^V_V'(p)? More to the point, if V' has no entities and is thus {}, how to we construct functions with it as the co-domain?) Of course, I could be misunderstanding the example or notation completely, but I don't think that's the case.

I wonder if it would be too hopeful to look forward to an illustrative example of sections of sheaves of minecraft chunks in the future.