Sheaves of sets on a space are somehow "parametrized sets". This is the philosophy by which one can do mathematics internal to a sheaf topos (of which theory I admit I know essentially nothing), with the possibility of defining all the usual mathematical concepts, except that in this case -if I understand correctly- the underlying logic will not be classical, e.g. the excluded middle may not hold.



> 
> What about linear algebra inside a sheaf topos? Which is the relationship between the category of (say finite dimensional) vector spaces as seen within a sheaf topos, and the category of vector bundles?
> 
> 
> 


I imagine that "internal" vector spaces will not be *exactly* the same thing as "external" vector bundles; rather, they will be something like sheaves of vector spaces. Is it correct? To which "internal" notion -if any- does the category of vector bundles correspond?



Is the theory of vector bundles just linear algebra done in a suitable topos?
I'll gather all the snippets from the various comments here (and mark this post as community wiki).


The answer to the question "Is the theory of vector bundles just linear algebra done in a suitable topos?" is a resounding **yes**.


One needs to fix a ring object $\mathcal{O}\_X$ in the topos $\mathrm{Sh}(X)$ of set-valued sheaves on the underlying topological space. Then vector bundles over $X$ are, from the internal point of view of $\mathrm{Sh}(X)$, simply finite free $\mathcal{O}\_X$-modules, and any intuitionistic theorem about modules applies to them. This holds for arbitrary ringed spaces (or even ringed locales or ringed toposes).


* If $\mathcal{O}\_X$ is the sheaf of continuous real-valued functions, then this notion will yield topological vector bundles. This example is slightly unique in that the sheaf of continuous real-valued functions can be described internally, as the set of Dedekind real numbers, and doesn't have to be put in as an external ingredient.
* If $X$ is a smooth manifold and $\mathcal{O}\_X$ is the sheaf of smooth real-valued functions, then this notion will yield smooth vector bundles.
* If $X$ is a complex manifold and $\mathcal{O}\_X$ is the sheaf of holomorphic functions, then this notion will yield holomorphic vector bundles.
* If $X$ is a scheme and $\mathcal{O}\_X$ is the structure sheaf of $X$, then this notion will yield scheme-theoretical vector bundles. (In this case, one often relaxes the condition "finite free" to "coherent".)


In all these cases, the ring object $\mathcal{O}\_X$ will look like a local ring from the internal point of view. Therefore all intuitionistic theorems about modules over local rings apply, for instance that the kernel of a surjection between finite free modules is finite free. In particular, this justifies Qiaochu's comment: A module over any ring is dualizable if and only if it is finitely generated and projective; a module over a local ring is finitely generated and projective if and only if it is finite free.


Additionally, in all the cases above except the case of unreduced schemes, the ring object $\mathcal{O}\_X$ will satisfy the following field condition from the internal point of view: Any element which is not invertible is zero. This field condition is strong enough to imply that any finitely generated module is *not not* finite free; this translates to the following external statement: Any sheaf of finite type is finite locally free on a dense open subset.


(This field condition is intuitionistically not equivalent to the related condition that any nonzero element is invertible. If one wants a ring object with this property, one has to look at the structure sheaf of an appropriate "big topos".)


To conclude, I want to mention just two of many applications of this school of thought.


* Many constructions which work for vector spaces generalize to vector bundles: for instance tensor products, exterior powers, symmetric powers, and so on. These generalizations "behave like their counterparts for vector spaces". One way to make this observation precise, and at the same time to prove it in full generality, is to employ the internal language: Any intuitionistic theorem about modules carries over to the internal setting.
* It's easy to show that finite free $R$-modules of rank $n$ are the same thing as $\mathrm{GL}\_n(R)$-torsors: map a finite free module $V$ to the torsor of bases of $V$. Conversely, map a $\mathrm{GL}\_n$-torsor $T$ to $T \otimes\_R R^n$. By the internal language, this automatically implies that vector bundles of rank $n$ are the same thing as sheaves of $\mathrm{GL}\_n(\mathcal{O}\_X)$-torsors. These are classified by the first Čech cohomology group of $\mathrm{GL}\_n(\mathcal{O}\_X)$. In this way we painlessly rederive the result that vector bundles of rank $n$ are classified by $\check H^1(X, \mathrm{GL}\_n(\mathcal{O}\_X))$.


More details and examples are in [these notes of mine](https://rawgit.com/iblech/internal-methods/master/notes.pdf).


