under construction
In the axiomatic of differential cohesion one may synthetically formulate a concept of manifolds locally modeled on a group object $V$. In the interpretation in an differentially cohesive (infinity,1)-topos these are étale infinity-groupoids.
For exposition see at geometry of physics -- manifolds and orbifolds and geometry of physics -- supergeometry.
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. 1, 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. 4, over any point $x \in X$ is the infinitesimal disk $\mathbb{D}^X_x$ in $X$ at that point, def.3. 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. 2 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. 1, 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. 4, i.e. an object $\mathbb{D}^V$ – the typical infinitesimal disk or formal disk, def. 3, – and a (chosen) equivalence
For $V$ a framed object, def. 5, 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. 5) such that the horizontal map in def. 4 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. 4, 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. 5, let $X$ be a $V$-manifold, def. 2. Then the infinitesimal disk bundle, def. 4, 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. 2, for framed $V$, def. 5, then its frame bundle
is the $GL(V)$-principal ∞-bundle given by prop. 2 via remark 3.
As in remark 3, 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. 7 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.
The concept is due to
Igor Khavkine, Urs Schreiber, Synthetic geometry of differential equations Part I -- Jets and comonad structure (arXiv:1701.06238)
Formalization in homotopy type theory is in