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).”
If you have trouble reading the article. The article assumes the reader has some knowledge of set notation. Look into it and you will find it easily readable.
>But now, minecraft also has a functor F:(openM)→E, where E is the category of entities, which has as objects just sets of entities and as morphisms the surjective maps
I too learned about categories, functors, and morphisms in my set theory class ..
Don't get me wrong I do know what all of those things are but I didn't learn about them in set theory.
i.e. the unions should be swapped for intersections. This is somewhat obvious if you've been paying attention to the definition of the restriction map and think about what the axiom is trying to accomplish, but tripped me up enough that I needed to check on Wikipedia to make sure I was following along correctly.
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 believe you would be correct on the first point, but have the second backwards. If V' was instead a chunk without the player, then res^V_V' Γ(V,F) = ∅, and the sections of sheaves are supported on {p} (as well as on any other entity with a valid chunk assignment). These sections would basically be functions providing the chunk containing a given entity, supported on the collection of all entities that actually exist on the map. Any other would give you 0 in the constructed top. space (no chunks if you don't exist).
What a fantastic choice of analogy to convey how sheaves attach data to a base space. With so many "Category Theory for Programmers" tutorials floating around, it's refreshing to see such a precise and easily comprehensible explanation of such topics while maintaining their geometric nature.
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.
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).”