Hello! I've come across a lot of questions (and nice answers) on MO, concerning infinite-dimensional manifolds and differential calculus over them, but nothing suiting the simpler and special case I have in mind.
Namely, I'm not putting my hand on "wild" spaces as the spaces of maps between (finite-dimensional) manifolds, but I'm rather interested in objects obtained as inverse limits of (finite-dimensional, finite-rank) smooth bundles. More precisely, let $$ M=M_0\leftarrow M_1\leftarrow M_2\leftarrow\cdots $$ a sequence of smooth bundles, and $$ F=F_0=C^\infty(M_0)\subseteq F_1=C^\infty(M_1)\subseteq F_2\subseteq F_3\subseteq\cdots $$ the corresponding sequence of smooth function algebras. Now, the "algebraic sequence" contains all information about the "geometric sequence" (in the spirit of Gelfand-Kolmogorov duality between manifolds and algebra of functions), so we can forget about the latter, and focus on the former. Direct limits of sequences of algebras embeddings are objects of the category of filtered algebras - so I can call the corresponding inverse limits of sequences of smooth bundles co-filtered manifolds.
When it comes to morphisms, it gets somehow harder to agree on the right definition. Indeed, for obvious geometrical reasons, we can consider only morphisms of filtered algebras having finite shift, i.e., algebras homomorphisms $\phi:F\to G$ sending each subalgebra $F_i$ into $G_{i+d}$, where the shift $d$ does not depend on $i$. However, there is plenty of nontrivial morphisms, which, on the corresponding co-filtered manifold, act as the identity. I have in mind the powers $\epsilon^r$, where $\epsilon:F\to F$ is the shift-1 morphism sendind each $F_i$ into $F_{i+1}$, i.e., the canonical embedding. Accordingly, it looks obvious to me to factor out such morphisms, hence declaring that two morphisms of filtered algebras are equivalent if their difference is $\epsilon^r$. This suggests to define the category of pro-finite manifolds, whose objects are co-filtered manifolds, and whose morphisms are equivalence classes w.r.t. the above equivalence.
Now, it looks easy and natural to develop differential calculus over pro-finite manifolds, by studying derivations, differential operators, differential forms, jet modules, etc., associated with filtered algebras, with only one additional care w.r.t. the finite-dimensional case: keeping track of the shift of the involved homomorphisms. This means that all objects which formalize a notion of differential calculus have to be filtered, accordingly to their shift: we have, e.g., vector fields of shit 0, of shift 1, etc. So, it is convenient to introduce the category of filtered modules over a filtered algebra, since it will contain all relevant modules needed for describing differential calculus in algebraic terms.
QUESTION: is the category of pro-finite manifolds, whose object are spectra of filtered algebras, and whose morphisms are equivalence classes (in the above sense) of filtered morphisms of finite shift, already known (most likely under another name)? if yes, has the differential calculus over them been described in terms of the filtered modules of derivations, differential operators, differential forms, etc., in the spirit of the duality between manifolds and function algebras?
PS. Of course, not all filtered algebras give rise to a sequence of smooth bundles... I tacitly assumed we were considering only the "good ones", just to not divert attention from the main question.

