this entry contains one chapter of geometry of physics.
previous chapters: smooth sets, smooth homotopy types
next chapters: G-structure and Cartan geometry, supergeometry, BPS charges
In the discussion at geometry of physics -- smooth sets we have started with very simple model spaces for differential geometry, namely just the Cartesian spaces, and have obtained from these, by passing to the sheaf topos over the site that they form, very general smooth spaces. We remarked that smooth manifolds form a full subcategory for these general smooth sets and hence sit in between the very simple model spaces and the very general smooth sets.
In making this statement, we assumed that we already know what smooth manifolds are. Here now we consider the question of characterizing smooth manifolds as special smooth sets, hence (re-)defining them, but in a way that is slightly (though not much) different from the traditional textbook description, a way that is true to the spirit of regarding smooth sets as the good ambient context for doing differential geometry.
Or rather, as throughout these notes, by characterizing smooth manifolds among smooth sets in a neat general abstract way, we may carry this characterization verbatim from smooth sets to the more general context of smooth homotopy types, where its interpretation becomes something that goes beyond what traditional textbook methods allow to cover: the concept of smooth manifold thus embedded into smooth groupoids comes out as the concept of étale groupoid (differentiable étale stack). A traditionally fairly familiar special class of these are orbifolds the direct analog in differential geometry of what in algebraic geometry is famous as Deligne-Mumford stacks.
Fully generally, the interpretation of the abstract concept of manifold in smooth homotopy types is a concept of smooth étale ∞-groupoids.
In fact more is true. The terminology smooth étale groupoid without further qualification refers to smooth groupoids that are locally diffeomorphic to a Cartesian space $\mathbb{R}^n$, in a suitable way. But more generall one may replace $\mathbb{R}^n$ here with any other group object $V$ in smooth sets, hence with any smooth group, and in fact with any ∞-group object in smooth homotopy types, hence with any smooth ∞-group: given any such, then a V-manifold is a smooth homotopy type $X$ which is locally diffeomorphic to $V$ in a suitable sense. One may say that $X$ is étalé (spread out), but over $V$.
For instance in higher super Cartan geometry $V$ is typically an extended super Minkowski spacetime (some super n-group) and $X$ is a superspacetime locally diffeomorphic to that.
A key aspect featured by $V$-manifolds, in this general sense, but not necessarily by more general smooth homotopy types, is that they carry a frame bundle, a principal bundle for the general linear group $GL(V)$ – which in the generality of higher differential geometry we define to be the automorphism ∞-group of the infinitesimal neighbourhood of the neutral element in $V$. The class of this frame bundle characterizes how the local diffeomorphic identifications of $X$ with $V$ are twisted with respect to each other as one moves around on $X$.
This is the key to formulating genuine geometric structure on smooth spaces: following an insight that goes back to Élie Cartan, most every sort of geometric structure on a smooth space $X$ is a (infinitesimally integrable) G-structure, hence a reduction of the structure group of the frame bundle of $X$, subject to some local rigidity constraint. This subsumes notably (pseudo-)Riemannian geometric structure, complex structure, symplectic structure, conformal structure and much more. These geometric structures on higher manifolds are the topic of the chapter geometry of physics -- G-structure and Cartan geometry.
We give first an account of the traditional definition of smooth manifolds, but (re-)phrasing it equivalently in category-theoretic terms that lend themselves to generalization.
In order to speak about tangent vectors and local diffeomorphisms in a way that generalizes to higher differential geometry, it is useful to introduce structure that allows to co-represent tangent vectors: where a smooth path in a Cartesian space $X$ is a smooth function out of the real line $\mathbb{R}$ into $X$, a tangent vector as traditionally defined is intuitively the restriction of such a map to the first order infinitesimal neighbourhood of the origin in $\mathbb{R}$: an “infinitesimal path”.
The idea now (which is the idea of synthetic differential geometry) is to make that intuition into a mathematical fact by passing to a context of slightly generalized Cartesian spaces where that infinitesimal neighbourhood exists literally as a subobject $\mathbb{D} \hookrightarrow \mathbb{R}$, such that the a tangent vector is literally a morphism $\mathbb{D} \to X$.
In order to see what these generalized Cartesian spaces might be, recall a basic fact about smooth functions:
Write $CAlg_{\mathbb{R}}$ for the category of commutative algebras over the field of real numbers. Write SmoothCartSp for the category of Cartesian spaces and smooth functions between them.
The functor
which sends a Cartesian space to (the formal dual of) its $\mathbb{R}$-algebra of smooth functions is a full and faithful functor.
In other words, for two Cartesian spaces $X,Y$ there is a natural bijection between the smooth functions $X \to Y$ and the algebra homomorphisms $C^\infty(X)\leftarrow C^\infty(Y)$.
See at embedding of smooth manifolds into formal duals of R-algebras for more on this.
One has to be careful that prop. 1 might seem to imply more than it does. In order that all constructions on all commutative algebras have the desired dual effect on formally dual smooth spaces (e.g. construction of products/coproducts, or construction of Kähler differentials) one needs to refine plain commutative algebras over $\mathbb{R}$ to smooth algebras. See there for more on this point, which however for our purposes here is not of further concern.
With Cartesian spaces embedded into the larger context of formal duals of commutative algebras by prop. 1, we may pass to a larger subcategory of the latter to obtain a notion of generalized smooth spaces. Since we are after infinitesimal spaces of sorts, and since, via the embedding of prop. 1, a space is equivalently encoded in the algebra of functions it carries, we need to specify those commutative algebras that behave like algebras of functions on infinitesimal Cartesian spaces. The intuition is that these spaces are so small, that the canonical coordinate functions $x^i$ on them take values which are so very small $\llt 1$ that when taken to some power they vanish not only approximately, but identically. But this intuition is easily formalized:
Write
for the full subcategory of the opposite category of commutative algebras over $\mathbb{R}$ on formal duals of commutative algebras over the real numbers of the form $\mathbb{R}\oplus V$ with $V$ a finite-dimensional nilpotent ideal (local Artin algebras over the real numbers). We call this the category of infinitesimally thickened points.
Write moreover
for the full subcategory on formal duals of those algebras which are tensor products of commutative $\mathbb{R}$-algebras of the form
of algebras $C^\infty(\mathbb{R}^p)$ of smooth functions $\mathbb{R}^n$ as in def. 1 with algebras corresponding to infinitesimally thickened points $D$ as above.
The basic idea of prop. 1 is familiar in algebraic geometry, going back to Alexander Grothendieck’s work in the 1950s, related to crystalline cohomology. Traditionally the idea is often embodied in the concept of formal schemes, which is however considerably more involved (locally ringed spaces, ind-objects) than necessary for capturing the basic phenomenon. The point that the simple idea of modelling infinitesimals by nilpotent element in functions rings is not at all restricted to algebraic geometry but also works in differential geometry has been highlighted by William Lawvere in the 1960s, who phrased it in terms of what is now known as the Kock-Lawvere axioms of synthetic differential geometry. In this context textbooks tend to amplify the usefulness of smooth algebras with infinitesimals, but as long as one does not insist on all geometric operations to have algebraic duals, see remark 1 above, then using just plain real algebras with nilpotent elements as done here is sufficient.
The evident full subcategory inclusion of smooth Cartesian spaces into formal smooth Cartesian spaces, def. 1 is coreflective, hence has a right adjoint $p$
On formal dual algebras, $p$ is given by quotienting out the nilpotent ideal.
We need to check that for all $n_1, n_2 \in \mathbb{N}$ and for all $D \in InfPoint$, there is a natural bijection between the set of morphisms
in $FormalSmoothCartSp$, and the set of morphisms
in $SmoothCartSp$. By definition, the former set is equivalently that of $\mathbb{R}$-algebra homomorphisms $\phi$ of the form
where $V$ is the nilpotent ideal of the formal dual algebra of functions on $D$.
Now for $v$ an element in the algebra on the right which is nilpotent, hence for which there is $p \in \mathbb{N}$ such that $v^p = 0$, then any algebra homomorphism $\phi$ needs to preserve this condition, hence also $\phi(v)^p = 0$ and hence also $\phi(v)$ is nilpotent. But the only nilpotent element in $C^\infty(\mathbb{R}^{n_1})$ is zero. Therefore every algebra homomorphism $\phi$ as above has to have $V$ in its kernel, hence it has to factor through the quotient projection $C^\infty(\mathbb{R}^{n_2})\otimes_{\mathbb{R}} V \to C^\infty(\mathbb{R}^{n_2})$.
With this the statement follows by prop. 1.
(A similar argument gives that $p$ is a functor in the first place.)
Following closely the theory at geometry of physics -- smooth sets, we are now to pass to the generalized smooth spaces which are locally probe-able by the formal smooth Cartesian spaces of def. 1, and these are the sheaves on the site $FormalSmoothCartSp$ that the latter form.
Regard the category $FormalSmoothCartSp$ of def. 1 as a site by equipping it with the coverage whose covering families are of the form
for $U, U_i \in SmoothCartSp \hookrightarrow FormalSmoothCartSp$, $D \in InfPoint \hookrightarrow FormalSmoothCartSp$, and $\{U_i \stackrel{\phi_i}{\to} U\}$ a covering family in $SmoothCartSp$, hence a traditional open cover.
A formal smooth set is a sheaf on the site $FormalSmoothCartSp$ of def. 2. Write
for the category of sheaves on that site.
The category of def. 3 is traditionally known as the Cahiers topos.
The co-reflective inclusion of sites of prop. 2
extends via Kan extension to an adjoint quadruple of functors
between smooth sets and formal smooth sets.
We agree that when in the following we write an unlabeled inclusion
then we always mean inclusion by $i_!$ in the above, not by $i_\ast$. On representables this is the inclusion $i$ of smooth Cartesian spaces into Cartesian spaces.
We write
for the adjoint triple of (co-)monads induced from the functors in prop. 3. At times we call these, respectively
$\Re$ – reduction modality;
$\Im$ – infinitesimal shape modality;
$\&$ – infinitesimal flat modality.
The single key fact to understand the operations in def. 4 is the left Kan extension of presheaves along a functor between sites restricts to that functor on representables. (See at Kan extension – Left Kan extension on representables).
This means that for $U \in SmoothCartSp \hookrightarrow FormalSmoothCartSp$ and $D \in InfPoint \hookrightarrow FormalSmoothCartSp$ then
$\Re( U \times D) \simeq D$;
$Hom(U \times D, \Im(X)) \simeq Hom(U, X)$.
The following is the key observation regarding generally the role of nilpotent elements in function algebras and specifically as to the nature of formal Cartesian spaces.
Write $\mathbb{D}$ for the formal dual of the algebra of dual numbers $(\mathbb{R}[\epsilon])/(\epsilon^2)$. Then morphisms
which are the identity after restriction along $\mathbb{R}^n \to \mathbb{R}^n \times \mathbb{D}$, are equivalently algebra homomorphisms of the form
which are the identity modulo $\epsilon$. Such a morphism has to take any function $f \in C^\infty(\mathbb{R}^n)$ to
for some smooth function $(\partial f) \in C^\infty(\mathbb{R}^n)$. The condition that this assignment makes an algebra homomorphism is equivalent to the statement that for all $f_1,f_2 \in C^\infty(\mathbb{R}^n)$
Multiplying this out and using that $\epsilon^2 = 0$ this in turn is equivalent to
This in turn means equivalently that $\partial\colon C^\infty(\mathbb{R}^n)\to C^\infty(\mathbb{R}^n)$ is a derivation. But derivations of algebras of smooth functions are equivalent to vector fields. (See at derivations of smooth functions are vector fields).
In particular one finds that maps
are equivalently single tangent vectors.
Based on this, the following is a classical fact of synthetic differential geometry.
For $X \in SmoothMfd \hookrightarrow Smooth0Type \hookrightarrow FormalSmooth0Type$ a smooth manifold, then the internal hom $[\mathbb{D},X]$ out of the infinitesimal interval is equivalent to the total space manifold of the tangent bundle of $X$:
By definition of internal hom, for every object $U$ then morphisms
are in natural bijection with morphisms
By example 2 these are smoothly $U$-parameterized tangent vectors in $X$, hence are naturally isomorphism to morphisms
Hence $[\mathbb{D},X]$ and $T X$ represent isomorphic representable functors. Then the Yoneda lemma implies that they are themselves isomorphic.
The traditional definition of local diffeomorphisms says
A smooth function $f \colon X \longrightarrow Y$ between smooth manifolds is a local diffeomorphism if for all points $x\in X$ its derivatives at that point induce an isomorphism of tangent vector spaces
A more category theoretic way to say this, which may still be found in some traditional textbooks, is this
A smooth function $f \colon X \longrightarrow Y$ between smooth manifolds is a local diffeomorphism, def. 5, equivalently if the diagram of tangent bundles that it induces
is a pullback diagram.
Now this in turn we may further reformulate as follows:
A smooth function $f \colon X \longrightarrow Y$ between smooth manifolds is a local diffeomorphism, def. 5, equivalently if after regarding in under the embedding $Smooth0Type \hookrightarrow FormalSmooth0Type$, the unit naturality square of the infinitesimal shape modality, def. 4,
is a pullback
Pullbacks of sheaves are detected by giving pullbacks of sets after evaluating on all possible objects of the site.
Consider first those objects of the form $U \in SmoothCartSp \hookrightarrow FormalSmoothCartSp \hookrightarrow FormalSmooth0Type$. By example 1 for these the diagram in question becomes
which is trivially a pullback. Consider then objects of the form $U \times \mathbb{D}$ for $\mathbb{D}$ the infinitesimal interval. By example 1 and by prop. 4 they all giving pullbacks is equivalent to the diagram
being a pullback. By prop. 5 this is already equivalent to $f$ being a local diffeomorphism.
But local diffeomorphisms of smooth manifolds (as opposed to formally étale morphisms of schemes!) are already necessarily étale morphisms, i.e. they diffeomorphically identify not just an infinitesimal neighbourhood around each point, but the whole germ. This implies that for $D \in InfPoint \hookrightarrow FormalSmoothCartSp \hookrightarrow FormalSmooth0Type$ any object, also the image of the diagram under $Hom(U \times D,-)$ gives a pullback.
Given prop. 6 it makes sense to say
A morphism $f \colon X\to Y$ in $FormalSmooth0Type$ is a local diffeomorphism (or formally étale morphism) if the naturality sqare of the unit of its infinitesimal shape modality
is a pullback diagram.
With the (re-)formulation of local diffeomorphisms between smooth manifolds and their generalization to maps of smooth sets by prop. 6, we now have the following neat way to characterize smooth manifolds among smooth sets.
For $n\in \mathbb{N}$, a smooth manifold of dimension $n$ is an object $X \in FormalSmooth0Type$ such that there exists a morphisms of the form
which is
an epimorphism,
a local diffeomorphism, def. 6;
A quick abstract way to prove this, for which however at this point we have not provided all the ingredients yet, is to observe that the map being an 1-epimorphism makes it equivalent to its Cech nerve groupoid object, and it being a local diffeomorphism makes that an étale groupoid. This being 0-truncated, its underlying object (stack) is equivalent to a smooth manifold, in fact as a groupoid object it is the Cech groupoid of that smooth manifold
with respect to the cover that we started with above.
the following is some semi-traditional basic discussion. Need to see what to do with this here.
On each overlap $U_i \cap U_j$ of two charts, the partial derivatives of the corresponding coordinate transformations
form the Jacobian matrix of smooth functions
with values in invertible matrices, hence in the general linear group $GL(n)$. By construction (by the chain rule), these functions satisfy on triple overlaps of coordinate charts the matrix product equations
(here and in the following sums over an index appearing upstairs and downstairs are explicit)
hence the equation
in the group $C^\infty(U_i \cap U_j \cap U_k, GL(n))$ of smooth $GL(n)$-valued functions on the chart overlaps.
This is the cocycle condition for a smooth Cech cocycle in degree 1 with coefficients in $GL(n)$ (precisely: with coefficients in the sheaf of smooth functions with values in $GL(n)$ ). We write
Formulated as smooth groupoids
$X$ itself is a Lie groupoid $(X \stackrel{\longrightarrow}{\longrightarrow} X)$ with trivial morphism structure;
from the atlas $\{U_i \to X\}$ we get the corresponding Cech groupoid
whose objects are the points in the atlas, with morphisms identifying lifts of a point in $X$ to different charts of the atlas;
The above situation is neatly encoded in the existence of a diagram of Lie groupoids of the form
where
the left morphism is stalk-wise (around small enough neighbourhoods of each point) an equivalence of groupoids (we make this more precise in a moment);
the horizontal functor $\tau_X$ has as components the functions $\lambda_{i j}$ and its functoriality is the cocycle condition $\lambda_{i j} \cdot \lambda_{j k} = \lambda_{i k}$.
A transformation of smooth functors $\lambda_1 \Rightarrow \lambda_2 : C(\{U_i\}) \to \mathbf{B} GL(n)$ is precisely a coboundary between two such cocycles.
This defines a morphism of smooth groupoids
The homotopy fiber of this map is a $GL(n)$-principal bundle called the frame bundle of $X$, while the canonically associated bundle via the canonical representation of $GL(n)$ on $\mathbb{R}^n$ is the tangent bundle
We now lift the above discussion of smooth manifolds inside smooth sets. phrased via an infinitesimal shape modality from the context of smooth sets to that of smooth groupoids. For background on smooth groupoids see the relevant discussions at geometry of physics -- smooth homotopy types.
In view of the refinement of smooth sets on the one hand to formal smooth sets and on the other hand to smooth groupoid, we now consider the joint refinement to formal smooth groupoids.
This proceeds essentially verbatim to the previous definitions
A pre-formal smooth groupoid is a presheaf of groupoids on $FormalSmoothCartSp$.
Write
for the (2,1)-category which is the simplicial localization at the local weak equivalences.
(…)
We may now directy adapt the definition of local diffeos as in def. 6 simply by generalizing 0-types to 1-types and pullbacks to homotopy pullbacks:
A morphism $f \colon X\to Y$ in $FormalSmooth1Type$, def. 8, is a local diffeomorphism (or formally étale morphism) if the naturality sqare of the unit of its infinitesimal shape modality
is a homotopy pullback diagram.
The traditional definition of smooth étale groupoids is the following:
A Lie groupoid $\mathcal{G}_\bullet$ is étale if its target map
is a local diffeomorphism.
The condition in def. 10 implies that all the other structure maps are local diffeomorphisms, too:
Inversion $(-)^{-1}\colon \mathcal{G}_1\stackrel{\simeq}{\to} \mathcal{G}_1$ is even a global diffeomorphism. Hence if the target map is a local diffeomorphism then the source map $s = t \circ (-)^{-1}$ is the composite of two local diffeos and as such itself a local diffeo.
The identity-assigning map $i \colon \mathcal{G}_0 \to \mathcal{G}_1$ is a section of a local diffeo (either $s$ or $t$) and hence itself a local diffeo.
The two projections out of $\mathcal{G}_1 \underset{\mathcal{G}_0}{\times} \mathcal{G}_1$ are pullbacks of local diffeos, and hence themselves local diffeos.
We now rephrase this more intrinsically.
Given a Lie groupoid we write $\mathcal{G}_0 \longrightarrow \mathcal{G}$ for the corresponding differentiable stack with atlas.
A Lie groupoid $\mathcal{G}_\bullet$ is an étale groupoid, def. 10, precisely if $\mathbb{G}_0 \to \mathcal{G}$ is a local diffeomorphism of smooth groupoids, def. 9 in that
is a homotopy pullback diagram of formal smooth groupoids
We compute the homotopy pulback by fibrant presentation of the morphism on the right, via the factorization lemma.
Inspection shows that in degree 0 this diagram is just the naturality square of the $\Im$-unit on the target map $t\colon \mathcal{G}_1 \to \mathcal{G}_0$. Hence by prop. 6 this is a pullback in degree-0 precisely already if $\mathcal{G}_\bullet$ is étale. By remark 4 this implies that the projection $p_2 \colon \mathcal{G}_1\underset{\mathcal{G}_0}{\times}\mathcal{G}_1 \to \mathcal{G}_1$ is a local diffeo, and that is equivalent to the above diagram being a pullback in degree 1.
In view of def./prop. 7, prop. 7 gives that étale groupoids are precisely the “1-higher manifolds”. For historical reasons this kind of statement is more prominent in the context of algebraic geometry, where it essentially corresponds to regarding Artin stacks (in particular Deligne-Mumford stacks) as higher or derived schemes.
Another point that prop. 7 makes maybe more manifest is that the traditional definition 10 makes a silent assumption that one may want to make explicit: it characterizes a Lie groupoid as étale relative to a manifold. A priori it may seem that the characterization is relative specifically to its maniold of objects. However, if $\mathcal{G}_0 \to \mathcal{G}$ is an étale atlas of a differentiable stack, and if \{\mathbb{R^n}\simeq U_i \to \mathcal{G}_0\}
is an open cover of the smooth manifold $\{\mathbb{R^\mathcal{G}_0$, then also the composite
is an étale atlas. This means that the étale nature of $\mathcal{G}_\bullet$ is really with respect to the chosen model space
One way to make this explicit in the more intrinsic diagrammatic formulation that we are discussing here is to say that we have a correspondence
where
both morphisms are local diffeomorphisms of smooth groupoids, def. 9;
the right morphism in addition is an effective epimorphism (1-epimorphism).
Jointly this says that $U \to X$ is an atlas which is étale relative to the model space $V$.
This perspective leads to the general abstract definition of V-manifolds in higher differential geometry, hence of étale ∞-groupoids, below.
In the above discussion we found an adjoint quadruple, prop. 3, on the category of formal smooth sets, and ended up expressing the theory of smooth manifolds entirely in terms of the induced monad which we called the infinitesimal shape modality $\Im$.
One may hence turn this around and regard any cohesive (∞,1)-topos that is equipped with an adjoint quadruple inclusion in this way as a formal context for manifold theory (“elasticity”).
Given a cohesive (∞,1)-topos $\mathbf{H}$ then the structure of differential cohesion on it is a choice of sub-topos $i_! \colon \mathbf{H}_{\Re} \hookrightarrow \mathbf{H}$ such that the inclusion extends to an adjoint quadruple
and such that $i_!$ preserves finite products. Given this then we write
for the induced adjoint triple of (co-)(∞,1)-monads induced from the four (∞,1)-functors. At times we call these, respectively
$\Re$ – reduction modality;
$\Im$ – infinitesimal shape modality;
$\&$ – infinitesimal flat modality.
Given $X,Y\in \mathbf{H}$ then a morphism $f \;\colon\; X\longrightarrow Y$ is a local diffeomorphism if its naturality square of the infinitesimal shape modality
is a homotopy pullback square.
Let now $V \in \mathbf{H}$ be given, equipped with the structure of a group (∞-group).
A V-manifold is an $X \in \mathbf{H}$ such that there exists a $V$-atlas, namely a correspondence of the form
with both morphisms being local diffeomorphisms, def. 12, and the right one in addition being an epimorphism, hence an atlas.
For $X \in \mathbf{H}$ an object and $x \colon \ast \to X$ a point, then we say that the infinitesimal neighbourhood of, or the infinitesimal disk at $x$ in $X$ is the homotopy fiber $\mathbb{D}^X_x$ of the unit of the infinitesimal shape modality at $x$:
For $X$ any object in differential cohesion, its infinitesimal disk bundle $T_{inf} X \to X$ is the homotopy pullback
of the unit of its infinitesimal shape modality along itself.
By the pasting law, the homotopy fiber of the infinitesimal disk bundle, def. 15, over any point $x \in X$ is the infinitesimal disk $\mathbb{D}^X_x$ in $X$ at that point, def.14. Nevertheless, for general $X$ the infinitesimal disk bundle need not be an fiber ∞-bundle with typical fiber (the infinitesimal disks at different points need not be equivalent, and even if they are, the bundle need not be locally trivial). Below in prop. 9 we see that for $X$ a $V$-manifold modeled on a group object $V$, then its infinitesimal disk bundle is indeed an fiber ∞-bundle, and hence is the associated ∞-bundle to some principal ∞-bundle. That principal bundle is the frame bundle of $X$.
The Atiyah groupoid of $T_{inf} X$ is the jet groupoid of $X$.
If $\iota \colon U \to X$ is a local diffeomorphism, def. 12, then
By the definition of local diffeos and using the pasting law we have an equivalence of pasting diagrams of homotopy pullbacks of the following form:
For $V$ an object, a framing on $V$ is a trivialization of its infinitesimal disk bundle, def. 15, i.e. an object $\mathbb{D}^V$ – the typical infinitesimal disk or formal disk, def. 14, – and a (chosen) equivalence
For $V$ a framed object, def. 16, we write
for the automorphism ∞-group of its typical infinitesimal disk/formal disk.
When the infinitesimal shape modality exhibits first-order infinitesimals, such that $\mathbb{D}(V)$ is the first order infinitesimal neighbourhood of a point, then $\mathbf{Aut}(\mathbb{D}(V))$ indeed plays the role of the general linear group. When $\mathbb{D}^n$ is instead a higher order or even the whole formal neighbourhood, then $GL(n)$ is rather a jet group. For order $k$-jets this is sometimes written $GL^k(V)$ We nevertheless stick with the notation “$GL(V)$” here, consistent with the fact that we have no index on the infinitesimal shape modality. More generally one may wish to keep track of a whole tower of infinitesimal shape modalities and their induced towers of concepts discussed here.
This class of examples of framings is important:
Every differentially cohesive ∞-group $G$ is canonically framed (def. 16) such that the horizontal map in def. 15 is given by the left action of $G$ on its infinitesimal disk at the neutral element:
By the discussion at Mayer-Vietoris sequence in the section Over an ∞-group and using that the infinitesimal shape modality preserves group structure, the defining homotopy pullback of $T_{inf} G$, def. 15, is equivalent to the pasting of pullback diagrams
where the right square is the defining pullback for the infinitesimal disk $\mathbb{D}^G$. Finally for the left square we find by this proposition that $T_{inf} G \simeq G\times \mathbb{D}^G$ and that the top horizontal morphism is as claimed.
By lemma 1 it follows that:
For $V$ a framed object, def. 16, let $X$ be a $V$-manifold, def. 13. Then the infinitesimal disk bundle, def. 15, of $X$ canonically trivializes over any $V$-cover $V \leftarrow U \rightarrow X$ , i.e. there is a homotopy pullback of the form
This exhibits $T_{inf} X\to X$ as a $\mathbb{D}^V$-fiber ∞-bundle.
By this discussion this fiber fiber ∞-bundle is the associated ∞-bundle of an essentially uniquely determined $\mathbf{Aut}(\mathbb{D}^V)$-principal ∞-bundle $Fr(X)$, i.e. there exists a homotopy pullback diagram of the form
Given a $V$-manifold $X$, def. 13, for framed $V$, def. 16, then its frame bundle
is the $GL(V)$-principal ∞-bundle given by prop. 9 via remark 10.
As in remark 9, this really axiomatizes in general higher order frame bundles with the order implicit in the nature of the infinitesimal shape modality.
By prop. 1 the construction of frame bundles in def. 18 is functorial in formally étale maps between $V$-manifolds.
This provides all the necessary structure to now set up an axiomatic theory of G-structure and higher Cartan geometry. This is discussed further at geometry of physics -- G-structure and Cartan geometry.
(…) formulation of the above in homotopy type theory in Wellen 17 (…)
The above formulation of V-manifolds in differential cohesion is due to dcct and
and the formalization in homotopy type theory is in