\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{geometry of physics -- manifolds and orbifolds}

\begin{quote}%
this entry contains one chapter of \emph{[[geometry of physics]]}.

previous chapters: \emph{[[geometry of physics -- smooth sets|smooth sets]]}, \emph{[[geometry of physics -- smooth homotopy types|smooth homotopy types]]}

next chapters: \emph{[[geometry of physics -- G-structure and Cartan geometry|G-structure and Cartan geometry]]}, \emph{[[geometry of physics -- supergeometry|supergeometry]]}, \emph{[[geometry of physics -- BPS charges|BPS charges]]}


\end{quote}
\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{ManifoldsAndOrdbifolds}{\textbf{Manifolds and orbifolds}}\dotfill \pageref*{ManifoldsAndOrdbifolds} \linebreak
\noindent\hyperlink{ModelLayer}{Model Layer}\dotfill \pageref*{ModelLayer} \linebreak
\noindent\hyperlink{ModelLayerManifolds}{Manifolds}\dotfill \pageref*{ModelLayerManifolds} \linebreak
\noindent\hyperlink{FormalSmoothCartesianSpaces}{Formal smooth Cartesian spaces}\dotfill \pageref*{FormalSmoothCartesianSpaces} \linebreak
\noindent\hyperlink{FormalSmoothSets}{Formal smooth sets}\dotfill \pageref*{FormalSmoothSets} \linebreak
\noindent\hyperlink{TangentVectors}{Tangent vectors}\dotfill \pageref*{TangentVectors} \linebreak
\noindent\hyperlink{local_diffeomorphisms}{Local diffeomorphisms}\dotfill \pageref*{local_diffeomorphisms} \linebreak
\noindent\hyperlink{SmoothManifold}{Smooth manifolds}\dotfill \pageref*{SmoothManifold} \linebreak
\noindent\hyperlink{FrameBundleTraditional}{Frame bundles}\dotfill \pageref*{FrameBundleTraditional} \linebreak
\noindent\hyperlink{tale_groupoids}{\'E{}tale groupoids}\dotfill \pageref*{tale_groupoids} \linebreak
\noindent\hyperlink{formal_smooth_groupoids}{Formal smooth groupoids}\dotfill \pageref*{formal_smooth_groupoids} \linebreak
\noindent\hyperlink{EtaleLieGroupoids}{\'E{}tale Lie groupoids}\dotfill \pageref*{EtaleLieGroupoids} \linebreak
\noindent\hyperlink{semantics_layer}{Semantics Layer}\dotfill \pageref*{semantics_layer} \linebreak
\noindent\hyperlink{differential_cohesion}{Differential cohesion}\dotfill \pageref*{differential_cohesion} \linebreak
\noindent\hyperlink{VManifolds}{$V$-Manifolds}\dotfill \pageref*{VManifolds} \linebreak
\noindent\hyperlink{FrameBundles}{Frame bundles}\dotfill \pageref*{FrameBundles} \linebreak
\noindent\hyperlink{syntax_layer}{Syntax Layer}\dotfill \pageref*{syntax_layer} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{ManifoldsAndOrdbifolds}{}\subsection*{{\textbf{Manifolds and orbifolds}}}\label{ManifoldsAndOrdbifolds}

In the discussion at \emph{[[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 \emph{[[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.

\begin{displaymath}
CartSp \hookrightarrow SmoothMfd \hookrightarrow Smooth0Type
\end{displaymath}
In making this statement, we assumed that we already know what smooth manifolds are. Here now we consider the question of \emph{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 \emph{[[étale groupoid]]} ([[differentiable stack|differentiable]] [[étale stack]]). A traditionally fairly familiar special class of these are \emph{[[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 \emph{smooth [[étale ∞-groupoids]]}.

In fact more is true. The terminology \emph{smooth [[étale groupoid]]} without further qualification refers to [[smooth groupoids]] that are \emph{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 \emph{[[V-manifold]]} is a smooth homotopy type $X$ which is locally diffeomorphic to $V$ in a suitable sense. One may say that $X$ is \emph{\'e{}tal\'e{}} (spread out), but over $V$.

For instance in [[higher Cartan geometry|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 \emph{[[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 ([[integrable G-structure|infinitesimally integrable]]) \emph{[[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 geometry|pseudo]]-)[[Riemannian geometry|Riemannian geometric structure]], [[complex structure]], [[symplectic structure]], [[conformal structure]] and much more. These geometric structures on higher manifolds are the topic of the chapter \emph{[[geometry of physics -- G-structure and Cartan geometry]]}.

\hypertarget{ModelLayer}{}\subsubsection*{{Model Layer}}\label{ModelLayer}

\hypertarget{ModelLayerManifolds}{}\paragraph*{{Manifolds}}\label{ModelLayerManifolds}

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.

\hypertarget{FormalSmoothCartesianSpaces}{}\paragraph*{{Formal smooth Cartesian spaces}}\label{FormalSmoothCartesianSpaces}

\begin{enumerate}%
\item 

\end{enumerate}
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 \emph{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 \emph{literally} as a [[subobject]] $\mathbb{D} \hookrightarrow \mathbb{R}$, such that the a tangent vector is \emph{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.

\begin{prop}
\label{EmbeddingOfSmoothManifoldsIntoFormalDualsOfRAlgebras}\hypertarget{EmbeddingOfSmoothManifoldsIntoFormalDualsOfRAlgebras}{}
The [[functor]]

\begin{displaymath}
C^\infty(-) \colon SmoothCartSp \longrightarrow CAlg_{\mathbb{R}}^{op}
\end{displaymath}
which sends a [[Cartesian space]] to (the [[formal dual]] of) its $\mathbb{R}$-[[commutative algebra|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)$.

\end{prop}
See at \emph{[[embedding of smooth manifolds into formal duals of R-algebras]]} for more on this.

\begin{remark}
\label{CarefulWithSmoothAlgebras}\hypertarget{CarefulWithSmoothAlgebras}{}
One has to be careful that prop. \ref{EmbeddingOfSmoothManifoldsIntoFormalDualsOfRAlgebras} 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 \emph{[[smooth algebras]]}. See there for more on this point, which however for our purposes here is not of further concern.

\end{remark}
With Cartesian spaces embedded into the larger context of formal duals of commutative algebras by prop. \ref{EmbeddingOfSmoothManifoldsIntoFormalDualsOfRAlgebras}, 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. \ref{EmbeddingOfSmoothManifoldsIntoFormalDualsOfRAlgebras}, 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:

\begin{defn}
\label{FormalSmoothCartesianSpaces}\hypertarget{FormalSmoothCartesianSpaces}{}
Write

\begin{displaymath}
InfPoint \hookrightarrow CAlg_{\mathbb{R}}^{op}
\end{displaymath}
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 \emph{[[infinitesimally thickened points]]}.

Write moreover

\begin{displaymath}
FormalSmoothCartSp
  \coloneqq
  CartSp \rtimes InfPoint \hookrightarrow CAlg_{\mathbb{R}}^{op}
\end{displaymath}
for the [[full subcategory]] on [[formal duals]] of those algebras which are [[tensor products]] of commutative $\mathbb{R}$-algebras of the form

\begin{displaymath}
C^\infty(\mathbb{R}^n) \otimes C^\infty(D)
\end{displaymath}
of algebras $C^\infty(\mathbb{R}^p)$ of [[smooth functions]] $\mathbb{R}^n$ as in def. \ref{EmbeddingOfSmoothManifoldsIntoFormalDualsOfRAlgebras} with algebras corresponding to infinitesimally thickened points $D$ as above.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
The basic idea of prop. \ref{FormalSmoothCartesianSpaces} 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 \ref{CarefulWithSmoothAlgebras} above, then using just plain real algebras with nilpotent elements as done here is sufficient.

\end{remark}
\begin{prop}
\label{SmoothCartSpCoreflectiveInFormalSmoothCartSp}\hypertarget{SmoothCartSpCoreflectiveInFormalSmoothCartSp}{}
The evident [[full subcategory]] inclusion of [[smooth Cartesian spaces]] into [[formal smooth manifold|formal smooth Cartesian spaces]], def. \ref{FormalSmoothCartesianSpaces} is [[coreflective subcategory|coreflective]], hence has a [[right adjoint]] $p$

\begin{displaymath}
(i \dashv p)
  \;\colon\;
  SmoothCartSp 
   \stackrel{\overset{i}{\hookrightarrow}}{\underset{p}{\longleftarrow}}
  FormalSmoothCartSp
  \,.
\end{displaymath}
On formal dual algebras, $p$ is given by quotienting out the [[nilpotent ideal]].

\end{prop}
\begin{proof}
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

\begin{displaymath}
\mathbb{R}^{n_1} \longrightarrow \mathbb{R}^{n_2}\times D
\end{displaymath}
in $FormalSmoothCartSp$, and the set of morphisms

\begin{displaymath}
\mathbb{R}^{n_1} \longrightarrow \mathbb{R}^{n_2}
\end{displaymath}
in $SmoothCartSp$. By definition, the former set is equivalently that of $\mathbb{R}$-algebra homomorphisms $\phi$ of the form

\begin{displaymath}
C^\infty(\mathbb{R}^{n_1})
   \longleftarrow
  C^\infty(\mathbb{R}^{n_2})\otimes_{\mathbb{R}} V
  \,,
\end{displaymath}
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. \ref{EmbeddingOfSmoothManifoldsIntoFormalDualsOfRAlgebras}.

(A similar argument gives that $p$ is a functor in the first place.)

\end{proof}
\hypertarget{FormalSmoothSets}{}\paragraph*{{Formal smooth sets}}\label{FormalSmoothSets}

Following closely the theory at \emph{[[geometry of physics -- smooth sets]]}, we are now to pass to the [[generalized smooth spaces]] which are \emph{locally probe-able} by the formal smooth Cartesian spaces of def. \ref{FormalSmoothCartesianSpaces}, and these are the [[sheaves]] on the [[site]] $FormalSmoothCartSp$ that the latter form.

\begin{defn}
\label{FormalSmoothCartesianSpacesSite}\hypertarget{FormalSmoothCartesianSpacesSite}{}
Regard the category $FormalSmoothCartSp$ of def. \ref{FormalSmoothCartesianSpaces} as a [[site]] by equipping it with the [[coverage]] whose covering families are of the form

\begin{displaymath}
\left\{
    U_i \times D \stackrel{(\phi_i,id_D)}{\longrightarrow} U \times D
  \right\}
\end{displaymath}
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]].

\end{defn}
\begin{defn}
\label{ToposOfFormalSmoothSets}\hypertarget{ToposOfFormalSmoothSets}{}
A \emph{formal smooth set} is a [[sheaf]] on the site $FormalSmoothCartSp$ of def. \ref{FormalSmoothCartesianSpacesSite}. Write

\begin{displaymath}
FormalSmooth0Type \coloneqq Sh(FormalSmoothCartSp)
\end{displaymath}
for the [[category of sheaves]] on that site.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
The category of def. \ref{ToposOfFormalSmoothSets} is traditionally known as the \emph{[[Cahiers topos]]}.

\end{remark}
\begin{prop}
\label{AdjointQuadrupleOnFormalSmoothSets}\hypertarget{AdjointQuadrupleOnFormalSmoothSets}{}
The co-reflective inclusion of sites of prop. \ref{SmoothCartSpCoreflectiveInFormalSmoothCartSp}

\begin{displaymath}
SmoothCartSp \stackrel{\overset{i}{\hookrightarrow}}{\underset{p}{\longleftarrow}} FormalSmoothCartSp
\end{displaymath}
extends via [[Kan extension]] to an [[adjoint quadruple]] of functors

\begin{displaymath}
Smooth0Type
   \stackrel{\overset{i_!}{\hookrightarrow}}{\stackrel{\overset{i^\ast}{\longleftarrow}}{\stackrel{\overset{i_\ast}{\hookrightarrow}}{\underset{i^!}{\longrightarrow}}}}
  FormalSmooth0Type
\end{displaymath}
between [[smooth sets]] and [[formal smooth sets]].

\end{prop}
We agree that when in the following we write an unlabeled inclusion

\begin{displaymath}
Smooth0Type \hookrightarrow FormalSmooth0Type
\end{displaymath}
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.

\begin{defn}
\label{AdjointTripleOnFormalSmoothSets}\hypertarget{AdjointTripleOnFormalSmoothSets}{}
We write

\begin{displaymath}
(\Re \dashv \Im \dashv \&)
  \;\colon\;
  FormalSmooth0Type
   \stackrel{\overset{i^\ast}{\longrightarrow}}{\stackrel{\overset{i_\ast}{\longleftarrow}}{\underset{i^!}{\longrightarrow}}}
   Smooth0Type
   \stackrel{\overset{i_!}{\longrightarrow}}{\stackrel{\overset{i^\ast}{\longleftarrow}}{\underset{i_\ast}{\longrightarrow}}}
  FormalSmooth0Type
\end{displaymath}
for the [[adjoint triple]] of ([[comonad|co]]-)[[monads]] induced from the functors in prop. \ref{AdjointQuadrupleOnFormalSmoothSets}. At times we call these, respectively

\begin{itemize}%
\item $\Re$ -- [[reduction modality]];


\item $\Im$ -- [[infinitesimal shape modality]];


\item $\&$ -- [[infinitesimal flat modality]].



\end{itemize}
\end{defn}
\begin{example}
\label{NatureOfTheModalitiesOnCahiersTopos}\hypertarget{NatureOfTheModalitiesOnCahiersTopos}{}
The single key fact to understand the operations in def. \ref{AdjointTripleOnFormalSmoothSets} is the [[left Kan extension]] of presheaves along a functor between sites restricts to that functor on representables. (See at \emph{\href{Kan+extension#LeftKanOnRepresentables}{Kan extension -- Left Kan extension on representables}}).

This means that for $U \in SmoothCartSp \hookrightarrow FormalSmoothCartSp$ and $D \in InfPoint \hookrightarrow FormalSmoothCartSp$ then

\begin{itemize}%
\item $\Re( U \times D) \simeq D$;


\item $Hom(U \times D, \Im(X)) \simeq Hom(U, X)$.



\end{itemize}
\end{example}
\hypertarget{TangentVectors}{}\paragraph*{{Tangent vectors}}\label{TangentVectors}

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.

\begin{example}
\label{TangentVectorsByAlgebra}\hypertarget{TangentVectorsByAlgebra}{}
Write $\mathbb{D}$ for the [[formal dual]] of the [[algebra of dual numbers]] $(\mathbb{R}[\epsilon])/(\epsilon^2)$. Then morphisms

\begin{displaymath}
\mathbb{R}^n \times \mathbb{D}\longrightarrow \mathbb{R}^n
\end{displaymath}
which are the identity after restriction along $\mathbb{R}^n \to \mathbb{R}^n \times \mathbb{D}$, are equivalently algebra homomorphisms of the form

\begin{displaymath}
(C^\infty(\mathbb{R}^n) \oplus \epsilon C^\infty(\mathbb{R}^n))
  \longleftarrow
  C^\infty(\mathbb{R}^n)
\end{displaymath}
which are the identity modulo $\epsilon$. Such a morphism has to take any function $f \in C^\infty(\mathbb{R}^n)$ to

\begin{displaymath}
f + (\partial f) \epsilon
\end{displaymath}
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)$

\begin{displaymath}
(f_1 f_2 + (\partial (f_1 f_2))\epsilon )
  =
  (f_1 + (\partial f_1) \epsilon)
  (f_2 + (\partial f_2) \epsilon)
  \,.
\end{displaymath}
Multiplying this out and using that $\epsilon^2 = 0$ this in turn is equivalent to

\begin{displaymath}
\partial(f_1 f_2) = (\partial f_1) f_2 + f_1 (\partial f_2)
  \,.
\end{displaymath}
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 \emph{[[derivations of smooth functions are vector fields]]}).

In particular one finds that maps

\begin{displaymath}
\mathbb{D} \longrightarrow \mathbb{R}^n
\end{displaymath}
are equivalently single [[tangent vectors]].

\end{example}
Based on this, the following is a classical fact of [[synthetic differential geometry]].

\begin{prop}
\label{TangentBundlesAsInternalHoms}\hypertarget{TangentBundlesAsInternalHoms}{}
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$:

\begin{displaymath}
T X \simeq [\mathbb{D},X]
  \,.
\end{displaymath}
\end{prop}
\begin{proof}
By definition of [[internal hom]], for every object $U$ then morphisms

\begin{displaymath}
U \longrightarrow [\mathbb{D},X]
\end{displaymath}
are in [[natural bijection]] with morphisms

\begin{displaymath}
U \times \mathbb{D}\longrightarrow X
  \,.
\end{displaymath}
By example \ref{TangentVectorsByAlgebra} these are smoothly $U$-parameterized tangent vectors in $X$, hence are naturally isomorphism to morphisms

\begin{displaymath}
U \longrightarrow T X
  \,.
\end{displaymath}
Hence $[\mathbb{D},X]$ and $T X$ represent isomorphic [[representable functors]]. Then the [[Yoneda lemma]] implies that they are themselves [[isomorphism|isomorphic]].

\end{proof}
\hypertarget{local_diffeomorphisms}{}\paragraph*{{Local diffeomorphisms}}\label{local_diffeomorphisms}

The traditional definition of [[local diffeomorphisms]] says

\begin{defn}
\label{LocalDiffeomorphismTraditional}\hypertarget{LocalDiffeomorphismTraditional}{}
A [[smooth function]] $f \colon X \longrightarrow Y$ between [[smooth manifolds]] is a \emph{local diffeomorphism} if for all points $x\in X$ its [[derivatives]] at that point induce an [[isomorphism]] of [[tangent bundle|tangent]] [[vector spaces]]

\begin{displaymath}
\underset{x \in X}{\forall} \;\; d f \;\colon\; T_x X \stackrel{\simeq}{\longrightarrow} T_{f(x)}Y
  \,.
\end{displaymath}
\end{defn}
A more [[category theory|category theoretic]] way to say this, which may still be found in some traditional textbooks, is this

\begin{prop}
\label{LocalDiffeosDetectedByPullbackOfTangentBundle}\hypertarget{LocalDiffeosDetectedByPullbackOfTangentBundle}{}
A [[smooth function]] $f \colon X \longrightarrow Y$ between [[smooth manifolds]] is a \emph{local diffeomorphism}, def. \ref{LocalDiffeomorphismTraditional}, equivalently if the [[diagram]] of [[tangent bundles]] that it induces

\begin{displaymath}
\itexarray{
    T X &\stackrel{}{\longrightarrow}& X
    \\
    \downarrow^{\mathrlap{d f}} && \downarrow
    \\
    T Y &\stackrel{}{\longrightarrow}& Y
  }
\end{displaymath}
is a [[pullback]] diagram.

\end{prop}
Now this in turn we may further reformulate as follows:

\begin{prop}
\label{TraditionalLocalDiffeosByModality}\hypertarget{TraditionalLocalDiffeosByModality}{}
A [[smooth function]] $f \colon X \longrightarrow Y$ between [[smooth manifolds]] is a \emph{local diffeomorphism}, def. \ref{LocalDiffeomorphismTraditional}, equivalently if after regarding in under the embedding $Smooth0Type \hookrightarrow FormalSmooth0Type$, the [[unit of a monad|unit]] [[natural transformation|naturality square]] of the [[infinitesimal shape modality]], def. \ref{AdjointTripleOnFormalSmoothSets},

\begin{displaymath}
\itexarray{
    X &\stackrel{}{\longrightarrow}& \Im X
    \\
    \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}}
    \\
    Y &\stackrel{}{\longrightarrow}& \Im Y
  }
\end{displaymath}
is a [[pullback]]

\end{prop}
\begin{proof}
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 \ref{NatureOfTheModalitiesOnCahiersTopos} for these the diagram in question becomes

\begin{displaymath}
\itexarray{
    Hom(U,X) &\stackrel{id}{\longrightarrow}& Hom(U,X)
    \\
    \downarrow^{\mathrlap{Hom(U,f)}} && \downarrow^{\mathrlap{Hom(U,f)}}
    \\
    Hom(U,Y) &\stackrel{id}{\longrightarrow}& Hom(U,Y)
  }
  \,,
\end{displaymath}
which is trivially a pullback. Consider then objects of the form $U \times \mathbb{D}$ for $\mathbb{D}$ the [[infinitesimal interval]]. By example \ref{NatureOfTheModalitiesOnCahiersTopos} and by prop. \ref{TangentBundlesAsInternalHoms} they all giving pullbacks is equivalent to the diagram

\begin{displaymath}
\itexarray{
    T X &\stackrel{}{\longrightarrow}& X
    \\
    \downarrow^{\mathrlap{d f}} && \downarrow
    \\
    T Y &\stackrel{}{\longrightarrow}& Y
  }
\end{displaymath}
being a pullback. By prop. \ref{LocalDiffeosDetectedByPullbackOfTangentBundle} 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.

\end{proof}
Given prop. \ref{TraditionalLocalDiffeosByModality} it makes sense to say

\begin{defn}
\label{LocalDiffeosGenerallyInCahiersTopos}\hypertarget{LocalDiffeosGenerallyInCahiersTopos}{}
A morphism $f \colon X\to Y$ in $FormalSmooth0Type$ is a \emph{[[local diffeomorphism]]} (or [[formally étale morphism]]) if the [[natural transformation|naturality sqare]] of the [[unit of a monad|unit]] of its [[infinitesimal shape modality]]

\begin{displaymath}
\itexarray{
    X &\stackrel{}{\longrightarrow}& \Im X
    \\
    \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}}
    \\
    Y &\stackrel{}{\longrightarrow}& \Im Y
  }
\end{displaymath}
is a [[pullback]] diagram.

\end{defn}
\hypertarget{SmoothManifold}{}\paragraph*{{Smooth manifolds}}\label{SmoothManifold}

With the (re-)formulation of local diffeomorphisms between smooth manifolds and their generalization to maps of smooth sets by prop. \ref{LocalDiffeosGenerallyInCahiersTopos}, we now have the following neat way to characterize smooth manifolds among [[smooth sets]].

\begin{defn}
\label{ManifoldsAsEtaleGroupoids}\hypertarget{ManifoldsAsEtaleGroupoids}{}
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

\begin{displaymath}
\underset{i }{\coprod} U_i
  \stackrel{=}{\to}
  \underset{i }{\coprod} \mathbb{R}^n 
  \longrightarrow
  X
\end{displaymath}
which is

\begin{enumerate}%
\item an [[epimorphism]],


\item a [[local diffeomorphism]], def. \ref{LocalDiffeosGenerallyInCahiersTopos};



\end{enumerate}
\end{defn}
\begin{proof}
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 in an (infinity,1)-category|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

\begin{displaymath}
\underset{i,j}{\coprod}  U_i \underset{X}{\times} U_j
  \stackrel{\longrightarrow}{\longrightarrow}
  \underset{i}{\coprod} U_i
\end{displaymath}
with respect to the cover that we started with above.

\end{proof}
\hypertarget{FrameBundleTraditional}{}\paragraph*{{Frame bundles}}\label{FrameBundleTraditional}

\begin{quote}%
the following is some semi-traditional basic discussion. Need to see what to do with this here.


\end{quote}
On each overlap $U_i \cap U_j$ of two charts, the [[partial derivatives]] of the corresponding [[coordinate transformations]]

\begin{displaymath}
\phi_j\circ \phi_i^{-1}
  : 
  U_i \cap U_j \subset \mathbb{R}^n \to \mathbb{R}^n
\end{displaymath}
form the [[Jacobian matrix]] of [[smooth functions]]

\begin{displaymath}
((\lambda_{i j})^{\mu}{}_{\mu})
  \coloneqq
  \left[\frac{d}{d x^\nu} \phi_j \circ \phi_i^{-1} (x^\mu)
  \right]
  :
  U_i \cap U_j 
  \to 
  GL_n
\end{displaymath}
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

\begin{displaymath}
(\lambda_{i j})^\mu{}_\lambda (\lambda_{j k})^\lambda{}_{\nu} 
  = 
  (\lambda_{i k})^\mu{}_{\nu}
  \,,
\end{displaymath}
(here and in the following sums over an index appearing upstairs and downstairs are explicit)

hence the equation

\begin{displaymath}
\lambda_{i j} \cdot \lambda_{j k} = \lambda_{i k}
\end{displaymath}
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 \emph{[[cocycle]] condition} for a smooth [[Cech cohomology|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

\begin{displaymath}
[(\lambda_{i j})] \in H^1_{smooth}(X, GL_n)
  \,.
\end{displaymath}
Formulated as [[smooth groupoids]]

\begin{itemize}%
\item $X$ itself is a [[Lie groupoid]] $(X \stackrel{\longrightarrow}{\longrightarrow} X)$ with trivial morphism structure;


\item from the atlas $\{U_i \to X\}$ we get the corresponding [[Cech groupoid]]

\begin{displaymath}
C(\{U_i\}) = 
  (\coprod_{i, j} U_i \cap U_j \stackrel{\longrightarrow}{\longrightarrow} \coprod_i U_i)
  = 
  \left\{
    \itexarray{
    && (x,j)
    \\
    & \nearrow &=& \searrow
    \\
      (x,i) &&\to&& (x,k)
    }
    \;\;\;
    for\, x \in U_i \cap U_j \cap U_k
  \right\}
  \,,
\end{displaymath}
whose objects are the points in the atlas, with morphisms identifying lifts of a point in $X$ to different charts of the atlas;



\end{itemize}
The above situation is neatly encoded in the existence of a [[diagram]] of Lie groupoids of the form

\begin{displaymath}
\itexarray{
     C(\{U_i\}) &\stackrel{\tau_X}{\longrightarrow}& \mathbf{B} GL(n).
     \\
     {}^{\mathllap{\simeq}}\downarrow
     \\
     X
  }
  \,,
\end{displaymath}
where

\begin{itemize}%
\item 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);


\item 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}$.



\end{itemize}
A [[natural transformation|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]]

\begin{displaymath}
\tau_X \;\colon\; X \to \mathbf{B}GL(n)
  \,.
\end{displaymath}
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]]

\begin{displaymath}
T X \to X
  \,.
\end{displaymath}
\hypertarget{tale_groupoids}{}\paragraph*{{\'E{}tale groupoids}}\label{tale_groupoids}

We now lift the \hyperlink{ModelLayerManifolds}{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 \emph{[[geometry of physics -- smooth homotopy types]]}.

\hypertarget{formal_smooth_groupoids}{}\paragraph*{{Formal smooth groupoids}}\label{formal_smooth_groupoids}

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

\begin{defn}
\label{FormalSmoothGroupoids}\hypertarget{FormalSmoothGroupoids}{}
A \emph{pre-formal smooth groupoid} is a [[presheaf]] of [[groupoids]] on $FormalSmoothCartSp$.

Write

\begin{displaymath}
FormalSmooth1Type \coloneqq L_{lwhe} PreFormalSmooth1Type
\end{displaymath}
for the [[(2,1)-category]] which is the [[simplicial localization]] at the local weak equivalences.

\end{defn}
(\ldots{})

\begin{displaymath}
\itexarray{
    Smooth1Type &
      \stackrel{\hookrightarrow}{\stackrel{\longleftarrow}{\stackrel{\hookrightarrow}{\longleftarrow}}}
    & FormalSmooth1Type
    \\
    \downarrow && \downarrow
    \\
    Smooth0Type
    &
      \stackrel{\hookrightarrow}{\stackrel{\longleftarrow}{\stackrel{\hookrightarrow}{\longleftarrow}}}
    &
    FormalSmooth0Type
  }
\end{displaymath}
We may now directy adapt the definition of local diffeos as in def. \ref{LocalDiffeosGenerallyInCahiersTopos} simply by generalizing [[0-types]] to [[1-types]] and [[pullbacks]] to [[homotopy pullbacks]]:

\begin{defn}
\label{LocalDiffeosGenerallyInFormalSmooth1Types}\hypertarget{LocalDiffeosGenerallyInFormalSmooth1Types}{}
A morphism $f \colon X\to Y$ in $FormalSmooth1Type$, def. \ref{FormalSmoothGroupoids}, is a \emph{[[local diffeomorphism]]} (or [[formally étale morphism]]) if the [[natural transformation|naturality sqare]] of the [[unit of a monad|unit]] of its [[infinitesimal shape modality]]

\begin{displaymath}
\itexarray{
    X &\stackrel{}{\longrightarrow}& \Im X
    \\
    \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}}
    \\
    Y &\stackrel{}{\longrightarrow}& \Im Y
  }
\end{displaymath}
is a [[homotopy pullback]] diagram.

\end{defn}
\hypertarget{EtaleLieGroupoids}{}\paragraph*{{\'E{}tale Lie groupoids}}\label{EtaleLieGroupoids}

The traditional definition of smooth [[étale groupoids]] is the following:

\begin{defn}
\label{EtaleGroupoidTraditional}\hypertarget{EtaleGroupoidTraditional}{}
A [[Lie groupoid]] $\mathcal{G}_\bullet$ is \emph{[[étale groupoid|étale]]} if its target map

\begin{displaymath}
t \colon \mathcal{G}_1 \longrightarrow \mathcal{G}_0
\end{displaymath}
is a [[local diffeomorphism]].

\end{defn}
\begin{remark}
\label{ImplicitConditionsInEtaleGroupoidDef}\hypertarget{ImplicitConditionsInEtaleGroupoidDef}{}
The condition in def. \ref{EtaleGroupoidTraditional} 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.

\end{remark}
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]].

\begin{prop}
\label{EtaleGroupoidByInfinitesimalShape}\hypertarget{EtaleGroupoidByInfinitesimalShape}{}
A [[Lie groupoid]] $\mathcal{G}_\bullet$ is an [[étale groupoid]], def. \ref{EtaleGroupoidTraditional}, precisely if $\mathbb{G}_0 \to \mathcal{G}$ is a [[local diffeomorphism]] of smooth groupoids, def. \ref{LocalDiffeosGenerallyInFormalSmooth1Types} in that

\begin{displaymath}
\itexarray{
    \mathcal{G}_0 &\longrightarrow& \Im \mathcal{G}_0
    \\
    \downarrow && \downarrow
    \\
    \mathcal{G} &\longrightarrow& \Im \mathcal{G}
  }
\end{displaymath}
is a [[homotopy pullback]] diagram of [[formal smooth groupoids]]

\end{prop}
\begin{proof}
We compute the homotopy pulback by fibrant presentation of the morphism on the right, via the [[factorization lemma]].

\begin{displaymath}
\itexarray{
    \mathcal{G}_0 \underset{\mathcal{G}_\bullet}{\times} \mathcal{G}^I_\bullet  &\longrightarrow& \Im \mathcal{G}_0 \underset{\Im\mathcal{G}_\bullet}{\times} \Im\mathcal{G}^I_\bullet
    \\
    \downarrow && \downarrow
    \\
    \mathcal{G}_\bullet &\longrightarrow& \Im \mathcal{G}_\bullet
  }
\end{displaymath}
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. \ref{TraditionalLocalDiffeosByModality} this is a pullback in degree-0 precisely already if $\mathcal{G}_\bullet$ is \'e{}tale. By remark \ref{ImplicitConditionsInEtaleGroupoidDef} 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.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
In view of def./prop. \ref{ManifoldsAsEtaleGroupoids}, prop. \ref{EtaleGroupoidByInfinitesimalShape} 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]].

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
Another point that prop. \ref{EtaleGroupoidByInfinitesimalShape} makes maybe more manifest is that the traditional definition \ref{EtaleGroupoidTraditional} makes a silent assumption that one may want to make explicit: it characterizes a Lie groupoid as [[étale Lie groupoid|étale]] \emph{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 \'e{}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 $\mathcal{G}_0$, then also the composite

\begin{displaymath}
U \coloneqq \underset{i}{\coprod} \mathbb{R}^n \longrightarrow \mathcal{G}_0
  \longrightarrow
  \mathcal{G}
\end{displaymath}
is an \'e{}tale atlas. This means that the \'e{}tale nature of $\mathcal{G}_\bullet$ is really with respect to the chosen model space

\begin{displaymath}
V \coloneqq \mathbb{R}^n
  \,.
\end{displaymath}
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]]

\begin{displaymath}
\itexarray{
      && U
      \\
      & \swarrow && \searrow
      \\
     V && && X
  }
\end{displaymath}
where

\begin{enumerate}%
\item both morphisms are [[local diffeomorphisms]] of smooth groupoids, def. \ref{LocalDiffeosGenerallyInFormalSmooth1Types};


\item the right morphism in addition is an [[effective epimorphism]] ([[1-epimorphism]]).



\end{enumerate}
Jointly this says that $U \to X$ is an [[atlas]] which is \'e{}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]], \hyperlink{VManifolds}{below}.

\end{remark}
\hypertarget{semantics_layer}{}\subsubsection*{{Semantics Layer}}\label{semantics_layer}

\hypertarget{differential_cohesion}{}\paragraph*{{Differential cohesion}}\label{differential_cohesion}

In the above discussion we found an [[adjoint quadruple]], prop. \ref{AdjointQuadrupleOnFormalSmoothSets}, 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]]'').

\begin{defn}
\label{}\hypertarget{}{}
Given a [[cohesive (∞,1)-topos]] $\mathbf{H}$ then the structure of \emph{[[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]]

\begin{displaymath}
\mathbf{H}_{\Re}
   \stackrel{\overset{i_!}{\hookrightarrow}}{\stackrel{\overset{i^\ast}{\longleftarrow}}{\stackrel{\overset{i_\ast}{\hookrightarrow}}{\underset{i^!}{\longrightarrow}}}}
  \mathbf{H}
\end{displaymath}
and such that $i_!$ preserves finite products. Given this then we write

\begin{displaymath}
(\Re \dashv \Im \dashv \&)
  \;\colon\;
  \mathbf{H}
   \stackrel{\overset{i^\ast}{\longrightarrow}}{\stackrel{\overset{i_\ast}{\longleftarrow}}{\underset{i^!}{\longrightarrow}}}
   \mathbf{H}_{\Re}
   \stackrel{\overset{i_!}{\longrightarrow}}{\stackrel{\overset{i^\ast}{\longleftarrow}}{\underset{i_\ast}{\longrightarrow}}}
  \mathbf{H}
\end{displaymath}
for the induced [[adjoint triple]] of ([[(∞,1)-comonad|co]]-)[[(∞,1)-monads]] induced from the four [[(∞,1)-functors]]. At times we call these, respectively

\begin{itemize}%
\item $\Re$ -- [[reduction modality]];


\item $\Im$ -- [[infinitesimal shape modality]];


\item $\&$ -- [[infinitesimal flat modality]].



\end{itemize}
\end{defn}
\hypertarget{VManifolds}{}\paragraph*{{$V$-Manifolds}}\label{VManifolds}

\begin{defn}
\label{LocalDiffeomorphismsInDifferentialCohesion}\hypertarget{LocalDiffeomorphismsInDifferentialCohesion}{}
Given $X,Y\in \mathbf{H}$ then a morphism $f \;\colon\; X\longrightarrow Y$ is a \emph{[[local diffeomorphism]]} if its naturality square of the [[infinitesimal shape modality]]

\begin{displaymath}
\itexarray{
    X &\longrightarrow& \Im X
    \\
    \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\Im f}}
    \\
    Y &\longrightarrow& \Im Y
  }
\end{displaymath}
is a [[homotopy pullback]] square.

\end{defn}
Let now $V \in \mathbf{H}$ be given, equipped with the structure of a [[group]] ([[∞-group]]).

\begin{defn}
\label{VManifold}\hypertarget{VManifold}{}
A \emph{[[V-manifold]]} is an $X \in \mathbf{H}$ such that there exists a \emph{$V$-[[atlas]]}, namely a [[correspondence]] of the form

\begin{displaymath}
\itexarray{
    && U
    \\
    & \swarrow && \searrow
    \\
    V && && X
  }
\end{displaymath}
with both morphisms being [[local diffeomorphisms]], def. \ref{LocalDiffeomorphismsInDifferentialCohesion}, and the right one in addition being an [[epimorphism]], hence an [[atlas]].

\end{defn}
\hypertarget{FrameBundles}{}\paragraph*{{Frame bundles}}\label{FrameBundles}

\begin{defn}
\label{InfinitesimalDisk}\hypertarget{InfinitesimalDisk}{}
For $X \in \mathbf{H}$ an object and $x \colon \ast \to X$ a point, then we say that the \emph{[[infinitesimal neighbourhood]] of}, or the \emph{[[infinitesimal disk]] at} $x$ in $X$ is the [[homotopy fiber]] $\mathbb{D}^X_x$ of the [[unit of a monad|unit]] of the [[infinitesimal shape modality]] at $x$:

\begin{displaymath}
\itexarray{
    \mathbb{D}^X_x &\longrightarrow& X
    \\
    \downarrow && \downarrow
    \\
    \ast &\stackrel{x}{\longrightarrow}& \im X
  }
  \,.
\end{displaymath}
\end{defn}
\begin{defn}
\label{FormalDiskBundle}\hypertarget{FormalDiskBundle}{}
For $X$ any object in differential cohesion, its \emph{infinitesimal disk bundle} $T_{inf} X \to X$ is the [[homotopy pullback]]

\begin{displaymath}
\itexarray{
    T_{inf} X &\stackrel{ev}{\longrightarrow}& X
    \\
    \downarrow^{\mathrlap{p}} && \downarrow
    \\
    X &\longrightarrow& \Im X
  }
\end{displaymath}
of the [[unit of a monad|unit]] of its [[infinitesimal shape modality]] along itself.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
By the [[pasting law]], the [[homotopy fiber]] of the infinitesimal disk bundle, def. \ref{FormalDiskBundle}, over any point $x \in X$ is the infinitesimal disk $\mathbb{D}^X_x$ in $X$ at that point, def.\ref{InfinitesimalDisk}. 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. \ref{FormalDiskBundleOfRegularManifoldsTrivializesOverCover} 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$.

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
The [[Atiyah groupoid]] of $T_{inf} X$ is the [[jet groupoid]] of $X$.

\end{remark}
\begin{lemma}
\label{EtalePullbackOfFormalDiskBundleIsFormalDiskBundle}\hypertarget{EtalePullbackOfFormalDiskBundleIsFormalDiskBundle}{}
If $\iota \colon U \to X$ is a local diffeomorphism, def. \ref{LocalDiffeomorphismsInDifferentialCohesion}, then

\begin{displaymath}
\iota^\ast T_{inf} X \simeq T_{inf}U
  \,.
\end{displaymath}
\end{lemma}
\begin{proof}
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:

\begin{displaymath}
\itexarray{
     \iota^\ast T_{inf} X &\longrightarrow& T_{inf} &\longrightarrow& X
     \\
     \downarrow && \downarrow && \downarrow
     \\
     U &\longrightarrow& X &\longrightarrow& \Im X
  }
  \;\;\;\;
  \simeq
  \;\;\;\;
  \itexarray{
      T_{inf} U &\longrightarrow& U &\longrightarrow& X
       \\
       \downarrow && \downarrow && \downarrow
       \\
       U &\longrightarrow& \Im U &\longrightarrow& \Im X
  }
\end{displaymath}
\end{proof}
\begin{defn}
\label{Framing}\hypertarget{Framing}{}
For $V$ an object, a \textbf{[[framing]]} on $V$ is a trivialization of its infinitesimal disk bundle, def. \ref{FormalDiskBundle}, i.e. an object $\mathbb{D}^V$ -- the typical [[infinitesimal disk]] or [[formal disk]], def. \ref{InfinitesimalDisk}, -- and a (chosen) [[equivalence]]

\begin{displaymath}
\itexarray{
    T_{inf} V && \stackrel{\simeq}{\longrightarrow} && V \times \mathbb{D}^n
    \\
    & \searrow && \swarrow_{\mathrlap{p_1}}
    \\
    && V
  }
  \,.
\end{displaymath}
\end{defn}
\begin{defn}
\label{GeneralLinearGroup}\hypertarget{GeneralLinearGroup}{}
For $V$ a framed object, def. \ref{Framing}, we write

\begin{displaymath}
GL(V) \coloneqq \mathbf{Aut}(\mathbb{D}^V)
\end{displaymath}
for the [[automorphism ∞-group]] of its typical [[infinitesimal disk]]/[[formal disk]].

\end{defn}
\begin{remark}
\label{OrderOfInfinitesimalDisks}\hypertarget{OrderOfInfinitesimalDisks}{}
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.

\end{remark}
This class of examples of framings is important:

\begin{prop}
\label{DifferentialCohesiveInfinityGroupIsCanonicallyFramed}\hypertarget{DifferentialCohesiveInfinityGroupIsCanonicallyFramed}{}
Every differentially cohesive [[∞-group]] $G$ is canonically framed (def. \ref{Framing}) such that the horizontal map in def. \ref{FormalDiskBundle} is given by the left action of $G$ on its [[infinitesimal disk]] at the neutral element:

\begin{displaymath}
ev \;\colon\; T_{inf}G \simeq G \times \mathbb{D}^G_e \stackrel{\cdot}{\longrightarrow} G
  \,.
\end{displaymath}
\end{prop}
\begin{proof}
By the discussion at \emph{[[Mayer-Vietoris sequence]]} in the section \emph{\href{Mayer-Vietoris%20sequence#OverAGroupObject}{Over an ∞-group}} and using that the [[infinitesimal shape modality]] preserves group structure, the defining [[homotopy pullback]] of $T_{inf} G$, def. \ref{FormalDiskBundle}, is equivalent to the pasting of pullback diagrams

\begin{displaymath}
\itexarray{
    T_{inf} G &\stackrel{}{\longrightarrow}&
    \mathbb{D}^G_e
    &\stackrel{}{\longrightarrow}& \ast
    \\
    \downarrow &&  \downarrow && \downarrow
    \\
    G \times G &\stackrel{(-)\cdot (-)^{-1}}{\longrightarrow}& G
    &\stackrel{}{\longrightarrow}&
    \Im G
  }
\end{displaymath}
where the right square is the defining pullback for the [[infinitesimal disk]] $\mathbb{D}^G$. Finally for the left square we find by \href{Mayer-Vietoris%20sequence#HTTArgumentForPullback}{this proposition} that $T_{inf} G \simeq G\times \mathbb{D}^G$ and that the top horizontal morphism is as claimed.

\end{proof}
By lemma \ref{EtalePullbackOfFormalDiskBundleIsFormalDiskBundle} it follows that:

\begin{prop}
\label{FormalDiskBundleOfRegularManifoldsTrivializesOverCover}\hypertarget{FormalDiskBundleOfRegularManifoldsTrivializesOverCover}{}
For $V$ a framed object, def. \ref{Framing}, let $X$ be a $V$-manifold, def. \ref{VManifold}. Then the infinitesimal disk bundle, def. \ref{FormalDiskBundle}, of $X$ canonically trivializes over any $V$-cover $V \leftarrow U \rightarrow X$ , i.e. there is a [[homotopy pullback]] of the form

\begin{displaymath}
\itexarray{
     U \times \mathbb{D}^V &\longrightarrow& T_{inf} X
     \\
     \downarrow && \downarrow
     \\
     U &\longrightarrow& X
  }
  \,.
\end{displaymath}
This exhibits $T_{inf} X\to X$ as a $\mathbb{D}^V$-[[fiber ∞-bundle]].

\end{prop}
\begin{prop}
\label{ModulatingMapOfFormalDiskBundle}\hypertarget{ModulatingMapOfFormalDiskBundle}{}
By \href{fiber+infinity-bundle#Properties}{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

\begin{displaymath}
\itexarray{
     T_{inf} X \simeq 
     & 
   Fr(X) \underset{\mathbf{Aut}(\mathbb{D}^V)}{\times} \mathbb{D}^V 
     &\longrightarrow&
     V//\mathbf{Aut}(\mathbb{D}^V)
     \\
     & \downarrow && \downarrow
     \\
     & X &\stackrel{}{\longrightarrow}& \mathbf{B}\mathbf{Aut}(\mathbb{D}^V)
  }
  \,.
\end{displaymath}
\end{prop}
\begin{defn}
\label{FrameBundleMap}\hypertarget{FrameBundleMap}{}
Given a $V$-manifold $X$, def. \ref{VManifold}, for framed $V$, def. \ref{Framing}, then its \emph{[[frame bundle]]}

\begin{displaymath}
\itexarray{
     Fr(X)
     \\
     \downarrow
     \\
     X 
  }
\end{displaymath}
is the $GL(V)$-[[principal ∞-bundle]] given by prop. \ref{FormalDiskBundleOfRegularManifoldsTrivializesOverCover} via remark \ref{ModulatingMapOfFormalDiskBundle}.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
As in remark \ref{OrderOfInfinitesimalDisks}, this really axiomatizes in general [[higher order frame bundles]] with the order implicit in the nature of the [[infinitesimal shape modality]].

\end{remark}
\begin{remark}
\label{FrameBundlesFunctorial}\hypertarget{FrameBundlesFunctorial}{}
By prop. \ref{EtalePullbackOfFormalDiskBundleIsFormalDiskBundle} the construction of frame bundles in def. \ref{FrameBundleMap} is functorial in [[formally étale maps]] between $V$-manifolds.

\end{remark}
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 \emph{[[geometry of physics -- G-structure and Cartan geometry]]}.

\hypertarget{syntax_layer}{}\subsubsection*{{Syntax Layer}}\label{syntax_layer}

(\ldots{}) formulation of the above in [[homotopy type theory]] in \hyperlink{Wellen17}{Wellen 17} (\ldots{})

\hypertarget{references}{}\subsection*{{References}}\label{references}

The above formulation of [[V-manifolds]] in [[differential cohesion]] is due to [[schreiber:differential cohomology in a cohesive topos|dcct]] and

\begin{itemize}%
\item [[Igor Khavkine]], [[Urs Schreiber]], \emph{[[schreiber:Synthetic variational calculus|Synthetic geometry of differential equations: I. Jets and comonad structure]]} (\href{https://arxiv.org/abs/1701.06238}{arXiv:1701.06238})

\end{itemize}
and the formalization in [[homotopy type theory]] is in

\begin{itemize}%
\item [[Felix Wellen]], \emph{[[schreiber:thesis Wellen|Formalizing Cartan Geometry in Modal Homotopy Type Theory]]}, PhD Thesis, 2017

\end{itemize}


\end{document}