@DamienC: Flabby means the restriction morphism F(V)→F(U) is surjective for any inclusion of opens U⊂V. If F is the sheaf of sections of the trivial vector bundle, it is easy to construct examples where the restriction map is not surjective, e.g., the smooth section x↦1/x over (-∞,0)∪(0,∞) does not extend to the real line.

The site of fibered smooth manifolds was first considered (implicitly) by Nijenhuis in 1958. Natural operations in differential geometry are defined as morphisms of sheaves on this site, see the book by Kolář–Michor–Slovák. For more references, see also Section 4.1 in arxiv.org/abs/2011.01208v4 and also Section 3.3 in arxiv.org/abs/2111.01095v3.

It may be best to give a definition of a vertical / nonvertical map, it is not clear from the context.

@PinakBanerjee: The case of (∞,n)-categories is a special case of sheaves valued in (∞,1)-categories: simply take the (∞,1)-category of (∞,n))-categories as a target.

Since $N$ is not required to be connected in the statement, there is a much easier answer: pick any atlas N→M, where N is a disjoint union of charts in M, which we can take to be diffeomorphic to open balls. Now N is homotopy equivalent to a discrete space (with H^k=0 for k>0) and any closed form on N is exact.

References for most items can be found by following the hyperlinks in ncatlab.org/nlab/show/duality+between+algebra+and+geometry. For the last three items, see also arxiv.org/abs/2005.05284. I am not aware of a single unifying source.

@PedroLauridsenRibeiro: The negative dimension is captured in the structure sheaf, not in the underlying topological space, so there is no connection to the topological or Hausdorff dimensions, since the latter do not depend on the structure sheaf.

@Emily: Thanks a lot, now available on the nLab here: ncatlab.org/nlab/show/list+of+theses+in+category+theory

To answer the question as it is stated in the title: a von Neumann algebra coincides with its double commutant, and the double commutant always contains the identity operator.

@SebastianGoette: I am not aware of any written accounts. Here is my guess how it could work. Working in the setting of presheaves of simplicial groups on the site of smooth manifolds, we can construct String(H) as an extension of Spin by the smooth ∞-group U(H)//U(1), where // denotes the stacky quotient (i.e., homotopy colimit). Then we can take π_0 of the resulting fiber sequence of presheaves of simplicial groups, which produces an exact sequence PU(H)→π_0(String(H))→Spin of sheaves of groups on the site of smooth manifolds.

The nLab has a fairly detailed article on pointfree uniformities: ncatlab.org/nlab/show/uniform+locale