A sheaf is a combinatorial, high-dimensional data structure on a topological space. You can use it to stitch together images, spatio-temporal target tracking, inference, data fusion, IoT time-series, continuous functions -- all kinds of things. Crazy cool stuff!
Applied sheaf theory is pretty new, and not yet widely known. This DARPA sheaf tutorial is a full two-day video series by Prof Michael Robinson (great teacher), and it's about the equivalent of a semester CS course compressed into two days. If you want to see an intro/big-picture overview video on what the sheaf data structure is, and how it's related to graph databases, topology, category theory, and data analysis, see:
What kind of math background do you need to understand Sheaf theory? Are these lectures truly accessible for someone with a non-background?
I tried watching bits of the youtube video OP linked but never saw where he actually defined what a Sheaf was as oppose to building motivation of learning it for applications.
I am excited for any truly accessibly beginner resources. Want to get your opinion if you links are for the true beginner?
Sheaf models are one of the most useful tools in logic and I'll definitely read this paper once I have more time again. One thing that seems strange to me based on the overview video is the focus on sheafs on a topological space. In mathematics it's typically easier and more flexible to consider sheafs on categories equipped with a Grothendieck coverage. Is there a reason why topological spaces are sufficient to model sensor integration?
Fascinating stuff. I've now done maths for some years now and this is the first time I even hear about sheafs.
Makes one wonder what else you may have missed just because it's not something profs at your programme are interested in.
edit. Follow-up. I wonder if there's a list of curious and possibly useful math stuff you might easily miss because it's not as ubiquitous and 'canonical' as (e.g.) analysis, linear algebra or functional analysis?
I had sheaf theory at an advanced algebraic geometry course, essentially you need them to define schemes. They are on the "you won't need this unless you go for a PhD" area, usually, although they are not that weird (I found schemes weirder than sheaves for some reason)
So, I can probably try to provide the beginnings of an ELI5 from a math point of view, since the heading really caught my eye: a sheaf is a way of assigning some data to subsets of a space which satisfied some commonsense axioms.
For instance, suppose you have a sheaf F that assigns to every open interval I on the real line the set[1] F(I) of real-valued functions defined on it. If I write F(a,b) for F((a,b)):
* f(x) = x is in all the F(a,b), since it's defined everywhere on the real line
* f(x) = 1/(x-3) isn't in F(2.9, 3.1) or even F(1,5), but it is in F(4,5)
And so on. There's an axiom that says that if you have
* f in F(I)
* g in F(J)
such that f = g everywhere on the intersection of I and J, then there is in fact some function h defined all over I ∪ J (i.e. h ∈ F(I ∪ J)) which you can restrict to I and J to get f and g respectively. So "compatible functions can be stitched together", where "compatible" means "agree on overlaps".
Sheaves give you a language to coherently[0] talk about "partially-defined" functions such as 1/(x-3) above, to stitch them together, and go from the "local" to the "global" picture and back comfortably. This last point is actually a hallmark of mathematics in the last one or two centuries: for instance, consider some equation which you want to find integer solutions for. If you want to show it has no solutions, you can reduce both sides modulo some number and show that there are no solutions mod n, which means it is impossible to find any solutions to begin with. It is a much more deep fact (the Hasse principle) that if you can find solutions mod all n (and a real one), you can always solve the original equation! (I'm fudging a bit here: see [2] for details.)
(Quick plug: I have a short post that talks about these things here[3], as well as another on the "p-adic" numbers that appear in the Hasse principle.)
Sheaves are general enough ("data" can mean[4] almost anything!) that Paul Cohen used them to prove the independence of the axiom of choice[5] from the Zermelo-Fränkel axioms (which is hard set theory) even though they were created for geometry, broadly speaking: in particular, they were one of the tools with which Grothendieck and his collaborators powerfully recast algebraic geometry in the 20th century, giving birth to "scheme theory"[6], which is e.g. vital in modern number theory. (I should probably mention the standard example of Wiles' proof of the Taniyama-Shimura conjecture that settled FLT.)
The "sheaf axioms" define what it means for a "rule" associating "data" to open subsets to be a sheaf, and I was just trying to illustrate them with the example of "F". (Perhaps calling them "properties" or "laws" -- or even an interface or typeclass! -- might help?)
In general, proving that something that looks like a sheaf really is one may be nontrivial. :)
In the special case that I outlined above, it certainly is easy to show that F satisfies those axioms, as you point out. And it is a sheaf (the sheaf of continuous real-valued functions on R) precisely because it does.
Sorry, I meant the claim about f and g. Assuming you meant that F(I) should be continuous functions, you can construct an h from f,g to be cont on I and J, no? So it's not an axiom. Just making sure I understand correctly...
Again, that was just an example. F is just one possible sheaf on the real line, and in the case of F, yes, continuous functions can be stitched together.
You could define A(I) = { } for a trivial example of a different sheaf A where the "data" (always an empty set, regardless of I) is very different from what it was in the case of F (the set of continuous functions on I).
Applied sheaf theory is pretty new, and not yet widely known. This DARPA sheaf tutorial is a full two-day video series by Prof Michael Robinson (great teacher), and it's about the equivalent of a semester CS course compressed into two days. If you want to see an intro/big-picture overview video on what the sheaf data structure is, and how it's related to graph databases, topology, category theory, and data analysis, see:
"Sheaves for engineering problems" https://www.youtube.com/watch?v=223-0x2KNOg
And for a deep dive into a paper, see:
"Sheaves are the canonical data structure for sensor integration" https://arxiv.org/abs/1603.01446
Python Cellular Sheaf Library:
https://github.com/kb1dds/pysheaf