While reading the chapter on toposes in Spivak and Fong's "Seven Sketches in compositionality", I bumped into the following:
Example 7.61. For a vector bundle $π : E → X$ over a space $X$, the corresponding sheaf is $Sec(π)$ corresponding to its sections: to each open set $i_U : U ⊆ X$, we associate the set of functions $s : U → E$ for which $\pi\circ s=i_U$. For example, in the case of the tangent bundle $π : TM → M$, the corresponding sheaf, call it $VF$, associates to each $U$ the set $VF(U)$ of vector fields on $U$.
The internal logic of the topos can then be used to consider properties of vector fields. For example, one could have a predicate $Grad : VF → Ω$ that asks for the largest subspace $Grad(v)$ on which a given vector field $v$ comes from the gradient of some scalar function. One could also have a predicate that asks for the largest open set on which a vector field is non-zero. Logical operations like $∧$ and $∨$ could then be applied to hone in on precise submanifolds throughout which various desired properties hold,and to reason logically about what other properties are forced to hold there.
I would be particularly interested in knowing something more about the second part of the example I reported here. In particular if such an apporach to study submanifolds of interest (for instance associated to differential equations, as suggested) has indeed been carried out or this is "just" some suggestive intuition.
Any reference would be most appreciated.
Thanks in advance