\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*{formal smooth infinity-groupoid} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{cohesive_toposes}{}\paragraph*{{Cohesive $\infty$-Toposes}}\label{cohesive_toposes} [[!include cohesive infinity-toposes - contents]] \hypertarget{differential_geometry}{}\paragraph*{{Differential geometry}}\label{differential_geometry} [[!include synthetic differential geometry - contents]] \hypertarget{lie_theory}{}\paragraph*{{$\infty$-Lie theory}}\label{lie_theory} [[!include infinity-Lie theory - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{Localic}{1-localic definition}\dotfill \pageref*{Localic} \linebreak \noindent\hyperlink{DerivedDefinition}{$\infty$-localic}\dotfill \pageref*{DerivedDefinition} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{structures}{Structures}\dotfill \pageref*{structures} \linebreak \noindent\hyperlink{StrucLieTheory}{$\infty$-Lie algebroids and deformation theory}\dotfill \pageref*{StrucLieTheory} \linebreak \noindent\hyperlink{StrucPaths}{Paths and geometric Postnikov towers}\dotfill \pageref*{StrucPaths} \linebreak \noindent\hyperlink{StrucCohomology}{Cohomology and principal $\infty$-bundles}\dotfill \pageref*{StrucCohomology} \linebreak \noindent\hyperlink{cohomology_localization}{Cohomology localization}\dotfill \pageref*{cohomology_localization} \linebreak \noindent\hyperlink{cohomology_of_lie_groups}{Cohomology of Lie groups}\dotfill \pageref*{cohomology_of_lie_groups} \linebreak \noindent\hyperlink{CohomologyOfLieAlgebroids}{Cohomology of $\infty$-Lie algebroids}\dotfill \pageref*{CohomologyOfLieAlgebroids} \linebreak \noindent\hyperlink{de_rham_theorem}{de Rham theorem}\dotfill \pageref*{de_rham_theorem} \linebreak \noindent\hyperlink{StructureSheaves}{Formally \'e{}tale morphisms and cohesive \'e{}tale $\infty$-groupoids}\dotfill \pageref*{StructureSheaves} \linebreak \noindent\hyperlink{formally_smooth__formally_unramified_morphisms}{Formally smooth / formally unramified morphisms}\dotfill \pageref*{formally_smooth__formally_unramified_morphisms} \linebreak \noindent\hyperlink{LieDifferentiation}{Lie differentiation}\dotfill \pageref*{LieDifferentiation} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A \emph{formal smooth $\infty$-groupoid} is an [[∞-groupoid]] equipped with a [[cohesive (∞,1)-topos|cohesive structure]] that subsumes that of [[smooth ∞-groupoid]]s as well as of [[infinitesimal object|infinitesimal]] $\infty$-groupoids -- [[∞-Lie algebroids]], hence equipped with ``[[differential cohesion]]''. In the [[cohesive (∞,1)-topos]] of formal smooth $\infty$-groupoids the canonical [[fundamental ∞-groupoid in a locally ∞-connected (∞,1)-topos]] $\mathbf{\Pi}(X)$ factors through a version relative to [[Smooth∞Grpd]]: the [[infinitesimal singular simplicial complex|infinitesimal path ∞-functor]] $\mathbf{\Pi}_{inf}(X)$. In traditional terms this is the object modeled by the [[tangent Lie algebroid]] and the [[de Rham space]] of $X$. The [[quasicoherent ∞-stack]]s on $\mathbf{\Pi}_{inf}(X)$ are [[D-module]]s on $X$. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} We consider [[(∞,1)-sheaves]] over a ``twisted semidirect product'' [[site]] or [[(∞,1)-site]] of \begin{itemize}% \item [[Cartesian spaces]] with [[smooth functions]] between them as for [[smooth ∞-groupoids]], \item and a [[category]] or [[(∞,1)-category]] of [[infinitesimally thickened points]]. \end{itemize} First in \begin{itemize}% \item \hyperlink{Localic}{1-localic definition} \end{itemize} we consider the 1-site, then in \begin{itemize}% \item \hyperlink{DerivedDefinition}{∞-localic definition} \end{itemize} we consider the $(\infty,1)$-site. \hypertarget{Localic}{}\subsubsection*{{1-localic definition}}\label{Localic} \begin{defn} \label{}\hypertarget{}{} Let $T :=$ [[CartSp]]${}_{smooth}$ be the [[syntactic category]] of the [[Lawvere theory]] of [[smooth algebra]]s: the category of [[Cartesian space]]s $\mathbb{R}^n$ and [[smooth function]]s between them. Write \begin{displaymath} SmoothAlg := T Alg \end{displaymath} for its category of [[algebras over a Lawvere theory|T-algebras]] -- the [[smooth algebra]]s ($C^\infty$-rings). Let \begin{displaymath} InfPoint \hookrightarrow SmoothAlg^{op} \end{displaymath} be the [[full subcategory]] on the [[infinitesimally thickened point]]s: this smooth algebras whose underlying abelian group is a [[vector space]] of the form $\mathbb{R} \oplus V$ with $V$ a finite-[[dimension]]al real [[vector space]] and nilpotent in the algebra structure. \end{defn} \begin{defn} \label{}\hypertarget{}{} Let \begin{displaymath} FormalCartSp \hookrightarrow SmoothLoc \end{displaymath} be the [[full subcategory]] of the category of [[smooth loci]] on the objects of the form \begin{displaymath} U = \mathbb{R}^n \times D \end{displaymath} that are [[product]]s of a [[Cartesian space]] $\mathbb{R}^n \in$ [[CartSp]] for $n \in \mathbb{N}$ and an [[infinitesimally thickened point]] $D \in InfPoint$. (See at \emph{[[FormalCartSp]]}.) Equip this category with the [[coverage]] where a family of morphisms is [[covering]] precisely if it is of the form $\{U_i \times D \stackrel{(f_i, Id_D)}{\to} U \times D\}$ for $\{f_i : U_i \to U\}$ a covering in [[CartSp]]${}_{smooth}$ (a [[good open cover]]). \end{defn} This appears as (Kock 86, (5.1)). \begin{remark} \label{}\hypertarget{}{} The [[sheaf topos]] over [[FormalCartSp]] is ([[equivalence of categories|equivalent]] to) the [[topos]] known as the [[Cahiers topos]], a [[smooth topos]] that constitutes a [[Models for Smooth Infinitesimal Analysis|well adapted model]] for [[synthetic differential geometry]]. See at \emph{[[Cahiers topos]]} for further references. \end{remark} \begin{defn} \label{}\hypertarget{}{} We say the [[(∞,1)-topos]] of \textbf{formal smooth $\infty$-groupoids} is the [[(∞,1)-category of (∞,1)-sheaves]] \begin{displaymath} FormalSmooth \infty Grpd := Sh_{(\infty,1)}(FormalCartSp) \end{displaymath} on $FormalCartSp$. \end{defn} \hypertarget{DerivedDefinition}{}\subsubsection*{{$\infty$-localic}}\label{DerivedDefinition} We now generalize the 1-category $InfPoint$ of [[infinitesimally thickened points]] to the [[(∞,1)-category]] $InfPoint_\infty$ of ``derived infinitesimally thickened points'', the formal dual of ``small commutative $\infty$-algebras'' from (\hyperlink{Hinich}{Hinich}, \hyperlink{Lurie}{Lurie}). (\ldots{}) \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \begin{prop} \label{}\hypertarget{}{} $FormalSmooth \infty Grpd$ is a [[cohesive (∞,1)-topos]]. \end{prop} \begin{proof} Because [[FormalCartSp]] is an [[∞-cohesive site]]. See there for details. \end{proof} \begin{defn} \label{}\hypertarget{}{} Write $FormalSmoothMfd \hookrightarrow SmoothAlg^{op}$ for the [[full subcategory]] of [[smooth loci]] on the \textbf{[[formal smooth manifolds]]}: those modeled on [[FormalCartSp]] equipped with the evident [[coverage]]. \end{defn} \begin{prop} \label{CartSpAsDenseSubOfFSmoothMfd}\hypertarget{CartSpAsDenseSubOfFSmoothMfd}{} $FormalCartSp$ is a [[dense sub-site]] of $FormalSmoothMfd$. \end{prop} \begin{prop} \label{EquivalenceToToposOverSoothSynthMfd}\hypertarget{EquivalenceToToposOverSoothSynthMfd}{} There is an [[equivalence of (∞,1)-categories]] \begin{displaymath} FormalSmooth\infty Grpd \simeq \hat Sh_{(\infty,1)}(FSmoothMfd) \end{displaymath} with the [[hypercomplete (∞,1)-topos]] over $FSmoothMfd$. \end{prop} \begin{proof} With the \hyperlink{CartSpAsDenseSubOfFSmoothMfd}{above observation} this is directly analogous to the corresponding proof at [[ETop∞Grpd]]. \end{proof} \begin{defn} \label{}\hypertarget{}{} Write $i : CartSp_{smooth} \hookrightarrow FormalCartSp$ for the canonical [[full subcategory|embedding]]. \end{defn} \begin{prop} \label{CohesivenessUnderSmoothInfGrpd}\hypertarget{CohesivenessUnderSmoothInfGrpd}{} The functor $i^*$ given by restriction along $i$ exhibits $FormalSmooth\infty Grpd$ as an of the [[(∞,1)-topos]] [[Smooth∞Grpd]] of [[smooth ∞-groupoids]] in that we have a quadruple of [[adjoint (∞,1)-functor]]s \begin{displaymath} ( i_! \dashv i^* \dashv i_* \dashv i^! ) : Smooth \infty Grpd \stackrel{\overset{i_!}{\hookrightarrow}}{\stackrel{\overset{i^*}{\leftarrow}}{\stackrel{\overset{i_*}{\to}}{\stackrel{i^!}{\leftarrow}}}} FormalSmooth \infty Grpd \,, \end{displaymath} such that $i_!$ is a [[full and faithful (∞,1)-functor]]. \end{prop} \begin{proof} Since $i : CartSp_{smooth} \hookrightarrow CartSp_{formalsmooth}$ is an \href{cohesive+%28infinity%2C1%29-topos+--+infinitesimal+cohesion#InfinitesimalNeighbourhoodFromInfinitesimalSite}{infinitesimally ∞-cohesive site} this follows with \href{cohesive+%28infinity%2C1%29-topos+--+infinitesimal+cohesion#InfinitesimalNeighbourhoodFromInfinitesimalSite}{a proposition} discussed at \emph{[[cohesive (infinity,1)-topos -- infinitesimal cohesion]]}. \end{proof} \hypertarget{structures}{}\subsection*{{Structures}}\label{structures} We discuss the realization of the general abstract in $FormalSmooth \infty Grpd$. Since by the \hyperlink{RelativeInftyConnectedness}{above discussion} $FormalSmooth\infty Grpd$ is strongly $\infty$-connected \emph{relative} to [[Smooth∞Grpd]] all of these structures that depend only on $\infty$-connectedness (and not on [[local (∞,1)-topos|locality]]) acquire a relative version. \hypertarget{StrucLieTheory}{}\subsubsection*{{$\infty$-Lie algebroids and deformation theory}}\label{StrucLieTheory} This subsection is at \begin{itemize}% \item [[∞-Lie algebroid]]. \end{itemize} \hypertarget{StrucPaths}{}\subsubsection*{{Paths and geometric Postnikov towers}}\label{StrucPaths} We discuss the realized in $FormalSmooth\infty Grpd$. \begin{displaymath} (\mathbf{Red} \dashv \mathbf{\Pi}_{inf} \dashv \mathbf{\flat}_{inf}) := (i \circ \Pi_{inf} \dashv Disc_{inf} \Pi_{inf} \dashv Disc_{inf} \circ \Gamma_{inf}) : FormalSmooth \infty Grpd \to FormalSmooth \infty Grpd \,. \end{displaymath} \begin{prop} \label{}\hypertarget{}{} For $U \times D \in CartSp_{smooth} \ltimes InfinSmoothLoc = FormalCartSp \hookrightarrow FormalSmooth\infty Grpd$ we have that \begin{displaymath} \mathbf{Red}(U \times D) \simeq U \end{displaymath} is the \textbf{reduced [[smooth locus]]}: the [[Isbell duality|formal dual]] of the [[smooth algebra]] obtained by quotienting out all nilpotent elements in the [[smooth algebra]] $C^\infty(K \times D) \simeq C^\infty(K) \otimes C^\infty(D)$. \end{prop} \begin{proof} By the [[model category]] presentation of $\mathbf{Red} \simeq \mathbb{L} Lan_i \circ \mathbb{R}i^*$ of the \hyperlink{CohesivenessUnderSmoothInfGrpd}{above proof} and using that every [[representable functor|representable]] is cofibrant and fibrant in the local projective [[model structure on simplicial presheaves]] we have \begin{displaymath} \begin{aligned} \mathbf{Red}(U \times D) & \simeq (\mathbb{L}Lan_i) (\mathbb{R}i^*) (U \times D) \\ &\simeq (\mathbb{L}Lan_i) i^* (U \times D) \\ & \simeq (\mathbb{L} Lan_i) U \\ & \simeq Lan_i U \\ & \simeq U \end{aligned} \end{displaymath} (using that $i$ is a [[full and faithful functor]]). \end{proof} \begin{prop} \label{PiInfYieldsDeRahmSpace}\hypertarget{PiInfYieldsDeRahmSpace}{} For $X \in SmoothAlg^{op} \to FormalSmooth \infty Grpd$ a [[smooth locus]], we have that $\mathbf{\Pi}_{inf}(X)$ is the corresponding [[de Rham space]], the object in which all [[infinitesimal object|infinitesimal]] neighbour points in $X$ are equivalent, characterized by \begin{displaymath} \mathbf{\Pi}_{inf}(X) : U \times D \mapsto X(U) \,. \end{displaymath} \end{prop} \begin{proof} By the $(\mathbf{Red} \dashv \mathbf{\Pi}_{inf})$-adjunction relation \begin{displaymath} \begin{aligned} \mathbf{\Pi}_{inf}(X)(U \times D) & = FormalSmooth \infty Grpd(U \times D, \mathbf{\Pi}_{inf}(X)) \\ & \simeq FormalSmooth \infty Grpd( \mathbf{Red}(U \times D), X) \\ & \simeq FormalSmooth \infty Grpd( U, X ) \end{aligned} \,. \end{displaymath} \end{proof} \hypertarget{StrucCohomology}{}\subsubsection*{{Cohomology and principal $\infty$-bundles}}\label{StrucCohomology} We discuss the realized in $FormalSmooth\infty Grpd$. \hypertarget{cohomology_localization}{}\paragraph*{{Cohomology localization}}\label{cohomology_localization} \begin{prop} \label{}\hypertarget{}{} The canonical [[line object]] of the [[Lawvere theory]] [[CartSp]]${}_{smooth}$ is the [[real line]], regarded as an object of the [[Cahiers topos]], and hence of $FormalSmooth \infty Grpd$ \begin{displaymath} \mathbb{A}^1_{CartSp_{smooth}} = \mathbb{R} \,. \end{displaymath} \end{prop} We shall write $\mathbb{R}$ also for the underlying additive group \begin{displaymath} \mathbb{G}_a = \mathbb{R} \end{displaymath} regarded as an abelian [[∞-group]] object in $FormalSmooth\infty Grpd$. For $n \in \mathbb{N}$ write $\mathbf{B}^n \mathbb{R} \in FormalSmooth\infty Grpd$ for its $n$-fold [[delooping]]. For $n \in \mathbb{N}$ and $X \in FormalSmooth\infty Grpd$ write \begin{displaymath} H^n_{synthdiff}(X) := \pi_0 FormalSmooth\infty Grpd(X,\mathbf{B}^n \mathbb{R}) \end{displaymath} for the [[cohomology group]] of $X$ with coefficients in the canonical line object in degree $n$. \begin{defn} \label{}\hypertarget{}{} Write \begin{displaymath} \mathbf{L}_{sdiff} \hookrightarrow FormalSmooth \infty Grpd \end{displaymath} for the [[cohomology localization]] of $FormalSmooth\infty Grpd$ at $\mathbb{R}$-[[cohomology]]: the full [[sub-(∞,1)-category]] on the $W$-[[local object]] with respect to the [[class]] $W$ of [[morphism]]s that induce [[isomorphism]]s in all $\mathbb{R}$-cohomology groups. \end{defn} \begin{prop} \label{PresentationOfCohomologyLocalization}\hypertarget{PresentationOfCohomologyLocalization}{} Let $SmoothAlg^{\Delta}_{proj}$ be the [[model structure on cosimplicial algebras|projective model structure on cosimplicial smooth algebras]] and let $j : (SmoothAlg^{\Delta})^{op} \to [FormalCartSp, sSet]$ be the prolonged external [[Yoneda embedding]]. \begin{enumerate}% \item This constitutes the [[right adjoint]] of a [[Quillen adjunction]] \begin{displaymath} (\mathcal{O} \dashv j) : (SmoothAlg^\Delta)^{op} \stackrel{\overset{\mathcal{O}}{\leftarrow}}{\underset{j}{\to}} [FSmoothMfd^{op}, sSet]_{proj,loc} \,. \end{displaymath} \item Restricted to [[simplicial object|simplicial]] [[formal smooth manifold]]s along \begin{displaymath} FSmoothMfd^{\Delta^{op}} \hookrightarrow (SmoothAlg^\Delta)^{op} \end{displaymath} the right [[derived functor]] of $j$ is a [[full and faithful (∞,1)-functor]] that factors through the [[cohomology localization]] and thus identifies a full [[reflective sub-(∞,1)-category]] \begin{displaymath} (FSmoothMfd^{\Delta^{op}})^\circ \hookrightarrow \mathbf{L}_{sdiff} \hookrightarrow FormalSmooth\infty Grpd \end{displaymath} \item The intrinsic $\mathbb{R}$-cohomology of any object $X \in FormalSmooth\infty Grpd$ is computed by the ordinary [[cochain cohomology]] of the [[Moore complex|Moore cochain complex]] underlying the cosimplicial abelian group of the image under the left [[derived functor]]$(\mathbb{L}\mathcal{O})(X)$ under the [[Dold-Kan correspondence]]: \begin{displaymath} H_{fSmooth}^n(X) \simeq H^n_{cochain}(N^\bullet(\mathbb{L}\mathcal{O})(X)) \,. \end{displaymath} \end{enumerate} \end{prop} \begin{proof} First a remark on the sites. By the \hyperlink{EquivalenceToToposOverSoothSynthMfd}{above proposition} $FormalSmooth\infty Grpd$ is equivalent to the [[hypercomplete (∞,1)-topos]] over [[formal smooth manifold]]s. This is [[presentable (∞,1)-category|presented]] by the [[nLab:Bousfield localization of model categories|left Bousfield localization]] of $[FSmoothMfd^{op}, sSet]_{proj,loc}$ at the [[∞-connected]] morphisms. But a fibrant object in $[FSmoothMfd^{op}, sSet]_{proj,loc}$ that is also [[n-truncated]] for $n \in \mathbb{N}$ is also fibrant in the hyperlocalization (only for the untruncated object there is an additional condition). Therefore the right Quillen functor claimed above indeed lands in truncated objects in $FormalSmooth \inftyGrpd$. The proof of the above statements is given in (\hyperlink{Stel}{Stel}), following (\hyperlink{Toen}{To\"e{}n}). Some details are spelled out at [[function algebras on ∞-stacks]]. \end{proof} \hypertarget{cohomology_of_lie_groups}{}\paragraph*{{Cohomology of Lie groups}}\label{cohomology_of_lie_groups} \begin{prop} \label{RealCohomologyOfCompactLieGroup}\hypertarget{RealCohomologyOfCompactLieGroup}{} Let $G \in SmoothMfd \hookrightarrow Smooth\infty Grpd \hookrightarrow FormalSmooth\infty Grpd$ be a [[Lie group]]. Then the intrinsic group cohomology in [[Smooth∞Grpd]] and in $FormalSmooth\infty Grpd$ of $G$ with coefficients in $\mathbb{R}$ coincides with [[Graeme Segal|Segal]]`s refined [[Lie group cohomology]] (\hyperlink{Segal}{Segal}, \hyperlink{Brylinski}{Brylinski}). \begin{displaymath} H^n_{smooth}(\mathbf{B}G, \mathbb{R}) \simeq H^n_{fsmooth}(\mathbf{B}G, \mathbb{R}) \simeq H^n_{Segal}(G,\mathbb{R}) \,. \end{displaymath} \end{prop} For the full proof please see [[schreiber:differential cohomology in a cohesive topos|here, section 3.4]] for the moment. \begin{cor} \label{}\hypertarget{}{} For $G$ a [[compact topological space|compact]] [[Lie group]] we have for all $n \geq 1$ that \begin{displaymath} H^n_{smooth}(G,U(1)) \simeq H_{top}^{n+1}(B G, \mathbb{Z}) \,. \end{displaymath} \end{cor} \begin{proof} This follows from applying the \hyperlink{RealCohomologyOfCompactLieGroup}{above result} to the [[fiber sequence]] induced by the sequence $\mathbb{Z} \to \mathbb{R} \to \mathbb{R}/\mathbb{Z} = U(1)$. \end{proof} \begin{note} \label{}\hypertarget{}{} This means that the intrinsic cohomology of [[compact topological space|compact]] [[Lie group]]s in [[Smooth∞Grpd]] and $FormalSmooth\infty Grpd$ coincides for these coefficients with the Segal-Blanc-Brylinski refined Lie group cohomology (\hyperlink{Brylinski}{Brylinski}). \end{note} \hypertarget{CohomologyOfLieAlgebroids}{}\paragraph*{{Cohomology of $\infty$-Lie algebroids}}\label{CohomologyOfLieAlgebroids} \begin{prop} \label{IntrinsicRealCohomologyByCECohomology}\hypertarget{IntrinsicRealCohomologyByCECohomology}{} Let $\mathfrak{a} \in L_\infty \mathrm{Algd}$ be an [[L-∞ algebroid]]. Then its intrinsic real cohomology in $\mathrm{FormalSmooth}\infty \mathrm{Grpd}$ \begin{displaymath} H^n(\mathfrak{a}, \mathbb{R}) := \pi_0 \mathrm{FormalSmooth}\infty \mathrm{Grpd}(\mathfrak{a}, \mathbf{B}^n \mathbb{R}) \end{displaymath} coincides with its ordinary [[∞-Lie algebroid cohomology|L-∞ algebroid cohomology]]: the cochain cohomology of its [[Chevalley-Eilenberg algebra]] \begin{displaymath} H^n(\mathfrak{a}, \mathbb{R}) \simeq H^n(\mathrm{CE}(\mathfrak{a})) \,. \end{displaymath} \end{prop} \begin{proof} By the \hyperlink{PresentationOfCohomologyLocalization}{above propoposition} we have that \begin{displaymath} H^n(\mathfrak{a}, \mathbb{R}) \simeq H^n N^\bullet(\mathbb{L}\mathcal{O})(i(\mathfrak{a})) \,. \end{displaymath} By \href{http://ncatlab.org/nlab/source/Lie+infinity-algebroid#CofibrantResolutionOfLinfinityAlgebroid}{this lemma} this is \begin{displaymath} \cdots \simeq H^n N^\bullet \left( \int^{[k] \in \Delta} \mathbf{\Delta}[k] \cdot \mathcal{O}(i(\mathfrak{a})_k) \right) \,. \end{displaymath} Observe that $\mathcal{O}(\mathfrak{a})_\bullet$ is cofibrant in the Reedy model structure $[\Delta^{\mathrm{op}}, (\mathrm{SmoothAlg}^\Delta_{\mathrm{proj}})^{\mathrm{op}}]_{\mathrm{Reedy}}$ relative to the opposite of the projective model structure on cosimplicial algebras:\newline the map from the latching object in degree $n$ in $\mathrm{SmoothAlg}^\Delta)^{\mathrm{op}}$ is dually in $\mathrm{SmoothAlg} \hookrightarrow \mathrm{SmoothAlg}^\Delta$ the projection \begin{displaymath} \oplus_{i = 0}^n \mathrm{CE}(\mathfrak{a})_i \otimes \wedge^i \mathbb{R}^n \to \oplus_{i = 0}^{n-1} \mathrm{CE}(\mathfrak{a})_i \otimes \wedge^i \mathbb{R}^n \end{displaymath} hence is a surjection, hence a fibration in $\mathrm{SmoothAlg}^\Delta_{\mathrm{proj}}$ and therefore indeed a cofibration in $(\mathrm{SmoothAlg}^\Delta_{\mathrm{proj}})^{\mathrm{op}}$. Therefore using the Quillen bifunctor property of the coend over the tensoring in reverse to \href{http://ncatlab.org/nlab/source/Lie+infinity-algebroid#CofibrantResolutionOfLinfinityAlgebroid}{this lemma}, the above is equivalent to \begin{displaymath} \cdots \simeq H^n N^\bullet \left( \int^{[k] \in \Delta} \Delta[k] \cdot \mathcal{O}(i(\mathfrak{a})_k) \right) \end{displaymath} with the fat simplex replaced again by the ordinary simplex. But in brackets this is now by definition the image under the monoidal Dold-Kan correspondence of the Chevalley-Eilenberg algebra \begin{displaymath} \cdots \simeq H^n( N^\bullet \Xi \mathrm{CE}(\mathfrak{a}) ) \,. \end{displaymath} By the [[Dold-Kan correspondence]] we have hence \begin{displaymath} \cdots \simeq H^n(\mathrm{CE}(\mathfrak{a})) \,. \end{displaymath} \end{proof} It follows that a degree-$n$ $\mathbb{R}$-cocycle on $\mathfrak{a}$ is presented by a morphism \begin{displaymath} \mu : \mathfrak{a} \to b^n \mathbb{R} \,, \end{displaymath} where on the right we have the $L_\infty$-algebroid whose $\mathrm{CE}$-algebra is concentrated in degree $n$. Notice that if $\mathfrak{a} = b \mathfrak{g}$ is the delooping of an $L_\infty$- algebra $\mathfrak{g}$ this is equivalently a morphism of $L_\infty$-algebras \begin{displaymath} \mu : \mathfrak{g} \to b^{n-1} \mathbb{R} \,. \end{displaymath} \hypertarget{de_rham_theorem}{}\paragraph*{{de Rham theorem}}\label{de_rham_theorem} \begin{quote}% under construction \end{quote} We consider the [[de Rham theorem]] in $FormalSmooth \infty Grpd$, with respect to the infinitesimal de Rham cohomology \begin{displaymath} H_{dR,inf}^n(X) := \pi_0 FormalSmooth \infty Grpd(X, \mathbf{\flat}_{inf} \mathbf{B}^n \mathbb{R}) \,. \end{displaymath} \begin{prop} \label{deRhamTheorem}\hypertarget{deRhamTheorem}{} For all $n \in \mathbb{N}$ The canonical morphism \begin{displaymath} \mathbf{\flat}_{inf} \mathbf{B}^n \mathbb{R} \to \mathbf{\flat} \mathbf{B}^n \mathbb{R} \end{displaymath} is an [[equivalence in an (∞,1)-category|equivalence]]. \end{prop} This means that for all $X \in \mathbf{H}$ the infinitesimal de Rham cohomology coincides with the ordinary real cohomology of the geometric realization of $X$ \begin{displaymath} H^n_{dR, inf}(X) \simeq H^n(|X|, \mathbb{R}) \,. \end{displaymath} \begin{proof} Since all representables are formally smooth, we have a colimit \begin{displaymath} U \times_{\mathbf{\Pi}_{inf}(U)} U \stackrel{\to}{\to} U \stackrel{}{\to} \mathbf{\Pi}_{inf}(U) \,. \end{displaymath} In the presentation over the site we have that \begin{displaymath} X \times_{\mathbf{\Pi}_{inf}(X)} X : K \times D \mapsto \{ f,g : K \times D \to U | K \to K \times D \stackrel{\to}{\to} U \} \,. \end{displaymath} Therefore a morphism $\mathbf{\Pi}_{inf}(U) \to \mathbb{R}$ is equivalently a morphism $\phi : U \to \mathbb{R}$ such that for all $K \times D \to U$ that coincide on $K$ we have that all the composites \begin{displaymath} K \times D \to U \stackrel{\phi}{\to} \mathbf{B}^n \mathbb{R} \end{displaymath} are equals. If $U$ is the point, then $\phi$ is necessarily constant. If $U$ is not the point, there is one nontrivial tangent vector $v$ in $U$. The composite produces the corresponding tangent vector $\phi_*(v)$ in $\mathbb{R}$. But all these tangent vectors must be equal. Hence $\phi$ must be constant. \end{proof} This kind of argument is indicated in (\hyperlink{SimpsonTeleman}{Simpson-Teleman, prop. 3.4}). \begin{prop} \label{PiInfAndTangents}\hypertarget{PiInfAndTangents}{} Let $X \in$ [[SmoothMfd]] and write $X^{\Delta^\bullet_{inf}} \in [CartSp_{formalsmooth}^{op}, sSet]$ for the [[tangent Lie algebroid]] regarded as a simplicial object (see [[L-infinity algebroid]] for the details). Then there is a morphism $X^{\Delta^\bullet_{inf}} \to \mathbf{\Pi}_{inf}(X)$ which is an equivalence in $\mathbb{R}$-cohomology. \end{prop} (\ldots{}) \hypertarget{StructureSheaves}{}\subsubsection*{{Formally \'e{}tale morphisms and cohesive \'e{}tale $\infty$-groupoids}}\label{StructureSheaves} We discuss \hyperlink{http://ncatlab.org/nlab/show/cohesive+%28infinity%2C1%29-topos+--+infinitesimal+cohesion#FormallySmoothEtaleUnramified}{formally \'e{}tale morphisms} and \hyperlink{}{\'e{}tale objects} with respect to the cohesive infinitesimal neighbourhood $i :$ [[Smooth∞Grpd]] $\hookrightarrow FormalSmooth\infty Grpd$. \begin{prop} \label{}\hypertarget{}{} Let $X_\bullet$ be a degreewise smooth [[paracompact topological space|paracompact]] [[simplicial manifold]], canonically regarded as an object of [[Smooth∞Grpd]]. Then $j_! X_\bullet$ in $FormalSmooth \infty Grpd$ is presented by the same simplicial manifold. \end{prop} \begin{proof} First consider an ordinary smooth paracompact manifold $X$. It admits a [[good open cover]] $\{U_i \to X\}$ and the corresponding [[Cech nerve]] $C(\{U_i\}) in [CartSp_{smooth}^{op}, sSet]_{proj}$ is a [[cofibrant resolution]] of $X$. Therefore the $\infty$-functor $j_!$ is computed on $X$ by evaluating the corresponding simplicial functor (of which it is the [[derived functor]]) on $C(\{U_i\})$. Since the simplicial functor \begin{displaymath} j_! : [CartSp_{smooth}^{op}, sSet]_{proj, loc} \to [CartSp_{formalsmooth}^{op}, sSet]_{proj, loc} \end{displaymath} is a [[left adjoint]] (indeed a [[left Quillen functor]]) it preserves the [[coproducts]] and [[coend]] that the Cech nerve is built from: \begin{displaymath} \begin{aligned} j_! C(\{U_i\}) & = j_! \int^{[n] \in \Delta} \Delta[n] \cdot \coprod_{i_0, \cdots, i_n} U_{i_0, \cdots, i_n} \\ & = \int^{[n] \in \Delta} \Delta[n] \cdot \coprod_{i_0, \cdots, i_n} j_! (U_{i_0, \cdots, i_n}) \\ & = \int^{[n] \in \Delta} \Delta[n] \cdot \coprod_{i_0, \cdots, i_n} U_{i_0, \cdots, i_n} \end{aligned} \,. \end{displaymath} Here we used that, by assumption on a [[good open cover]], all the $U_{i_0, \cdots, i_n}$ are [[Cartesian spaces]], and that $j_!$ coincides on [[representable functor|representables]] with the inclusion $CartSp_{smooth} \hookrightarrow CartSp_{formalsmooth}$. Let now $X_\bullet$ be a general simplicial manifold. Assume that in each degree there is a [[good open cover]] $\{U_{p,i} \to X_p\}$ such that these fit into a simplicial system giving a bisimplicial Cech nerve such that there is a morphism of [[bisimplicial object|bisimplicial presheaves]] \begin{displaymath} C(\mathcal{U})_{\bullet, \bullet} \to X_{\bullet} \end{displaymath} with $X_\bullet$ regarded as simplicially constant in one direction. Each $C(\mathcal{U})_{p, \bullet} \to X_p$ is a cofibrant resolution. We claim that the [[coend]] \begin{displaymath} \int^{[n] \in \Delta} C(\mathcal{U})_{n, \bullet} \cdot \mathbf{\Delta}[n] \;\;\; \to \;\;\; X \end{displaymath} is a cofibrant resolution of $X$, where $\mathbf{\Delta}$ is the [[fat simplex]]. From this the proposition follows by again applying the left Quillen functor $j_!$ degreewise and pulling it through all the colimits. This remaining claim follows from the same argument as used above in prop. \ref{RealCohomologyOfCompactLieGroup}. \end{proof} \begin{prop} \label{RecoveringLocalDiffeomorphisms}\hypertarget{RecoveringLocalDiffeomorphisms}{} A morphism in $FormalSmooth\infty Grpd$, is a [[formally étale morphism]] with respect to the [[infinitesimal cohesion]] $i \colon Smooth \infty Grpd \hookrightarrow FormalSmooth\infty Grpd$ precisely if for all [[infinitesimally thickened points]] $D$ the diagram \begin{displaymath} \itexarray{ X^D &\stackrel{f^D}{\to}& Y^D \\ \downarrow && \downarrow \\ Y &\stackrel{f}{\to}& Y } \end{displaymath} is an $\infty$-pullback under $i^*$. \end{prop} \begin{remark} \label{}\hypertarget{}{} Since $i^*$ preserves $\infty$-limits, this is the case in particular if the diagram is an $\infty$-pullback already in $FormalSmooth\infty Grod$. In this form, restricted to 0-truncated objects, hence to the [[Cahiers topos]], this characterization of formally \'e{}tale morphisms appears axiomatized around p. 82 of (\hyperlink{Kock}{Kock 81, p. 82}). In particular, a [[smooth function]] $f : X \to Y$ in [[SmoothMfd]] $\hookrightarrow$ [[Smooth∞Grpd]] between [[smooth manifolds]] is a [[formally étale morphism]] with respect to the [[infinitesimal cohesion]] $Smooth \infty Grpd \hookrightarrow FormalSmooth\infty Grpd$ precisely if it is a [[local diffeomorphism]] in the traditional sense. \end{remark} \begin{proof} We spell out the case for smooth manifolds. Here we need to to show that \begin{displaymath} \itexarray{ i_! X &\stackrel{i_! f}{\to}& i_! Y \\ \downarrow && \downarrow \\ i_* X &\stackrel{i_* f}{\to}& i_* Y } \end{displaymath} is a [[pullback]] in $Sh(CartSp_{formalsmooth})$ precisely if $f$ is a local diffeomorphism. This is a pullback precisely if for all $U \times D \in CartSp_{smooth} \ltimes InfPoint \simeq CartSp_{formalsmooth}$ the diagram of sets of plots \begin{displaymath} \itexarray{ Hom(U \times D, i_! X) &\stackrel{i_! f}{\to}& Hom(U \times D, i_! Y) \\ \downarrow && \downarrow \\ Hom(U \times D, i_* X) &\stackrel{i_* f}{\to}& Hom(U \times D, i_* Y) } \end{displaymath} is a pullback. Using, by the discussion at [[∞-cohesive site]], that $i_!$ preserves colimits and restricts to $i$ on representables, and using that $i^* (U \times D ) = U$, this is equivalently the diagram \begin{displaymath} \itexarray{ Hom(U \times D, X) &\stackrel{f_*}{\to}& Hom(U \times D, Y) \\ \downarrow && \downarrow \\ Hom(U , X) &\stackrel{f_*}{\to}& Hom(U , Y) } \,, \end{displaymath} where the vertical morphisms are given by restriction along the inclusion $(id_U, *) : U \to U \times D$. For one direction of the claim it is sufficient to consider this situation for $U = *$ the point and $D$ the first order infinitesimal interval. Then $Hom(*,X)$ is the underlying set of points of the manifold $X$ and $Hom(D,X)$ is the set of tangent vectors, the set of points of the [[tangent bundle]] $T X$. The pullback \begin{displaymath} Hom(*,X) \times_{Hom(*,Y)} Hom(D,Y) \end{displaymath} is therefore the set of pairs consisting of a point $x \in X$ and a tangent vector $v \in T_{f(x)} Y$. This set is in fiberwise bijection with $Hom(D, X) = T X$ precisely if for each $x \in X$ there is a bijection $T_x X \simeq T_{f(x)}Y$, hence precisely if $f$ is a [[local diffeomorphism]]. Therefore $f$ being a local diffeo is necessary for $f$ being formally \'e{}tale with respect to the given notion of infinitesimal cohesion. To see that this is also sufficient notice that this is evident for the case that $f$ is in fact a [[monomorphism]], and that since [[smooth function]]s are characterized locally, we can reduce the general case to that case. \end{proof} \begin{prop} \label{}\hypertarget{}{} A [[Lie groupoid]] $\mathcal{G}$ is an [[étale groupoid]] in the traditional sense, precisely if regarded as an object in $i :$ [[Smooth∞Grpd]] $\hookrightarrow$ [[FormalSmooth∞Grpd]] it is an \href{http://ncatlab.org/nlab/show/cohesive+%28infinity%2C1%29-topos+--+infinitesimal+cohesion#EtaleObjects}{cohesive \'e{}tale ∞-groupoid}. \end{prop} \begin{proof} Let $\mathcal{G}_0 \to \mathcal{G}$ be the inclusion of the smooth manifold of objects. This is an [[effective epimorphism in an (infinity,1)-category|effective epimorphism]]. It remains to show that this is \href{http://ncatlab.org/nlab/show/cohesive+%28infinity%2C1%29-topos+--+infinitesimal+cohesion#FormallySmoothEtaleUnramified}{formally \'e{}tale} with respect to the given cohesive neighbourhood. By the discussion at \emph{[[(∞,1)-pullback]]} we may compute the characteristic $(\infty,1)$-pullback by an ordinary pullback of a [[fibration]] of [[simplicial presheaves]] that presents $\mathcal{G}_0 \to \mathcal{G}$. By the [[factorization lemma]] such is given by \begin{displaymath} \mathcal{G}^I \times_{\mathcal{G}} \mathcal{G}_0 \to \mathcal{G} \,. \end{displaymath} By inspection one see that this morphism is \begin{itemize}% \item in degree 0 the target-map $t : Mor(\mathcal{G}) \to \mathcal{G}_0$; \item in degree 1 the projection $Mor(\mathcal{G}) {}_t\times_{s} Mor(\mathcal{G}) \to Mor(\mathcal{G})$. \end{itemize} By prop. \ref{RecoveringLocalDiffeomorphisms} both of these need to be [[étale maps]] in the ordinary sense. By definition, this is the case precisely if $\mathcal{G}$ is an [[étale groupoid]]. \end{proof} \hypertarget{formally_smooth__formally_unramified_morphisms}{}\subsubsection*{{Formally smooth / formally unramified morphisms}}\label{formally_smooth__formally_unramified_morphisms} As a direct consequence of prop. \ref{RecoveringLocalDiffeomorphisms} we have the following \begin{prop} \label{}\hypertarget{}{} A [[smooth function]] $f : X \to Y$ between [[smooth manifolds]], is a [[submersion]] or [[immersion]], respectively, precisely if, when canonically regarded as a morphism in $FormalSmooth \infty Grpd$, it is a [[formally smooth morphism]] or [[formally unramified morphism]], respectively. \end{prop} \begin{proof} As in the proof of prop. \ref{RecoveringLocalDiffeomorphisms} we find that the pullback $i_* X \times_{i_* Y} i_! Y$ is over the [[infinitesimal interval]] isomorphic to \begin{displaymath} X \times_Y T Y \end{displaymath} and the canonical morphism from $i_! X$ into this pullback is \begin{displaymath} T X \to X \times_Y T Y \,. \end{displaymath} \end{proof} \hypertarget{LieDifferentiation}{}\subsubsection*{{Lie differentiation}}\label{LieDifferentiation} We indicate how to formalize [[Lie differentiation]] in the context of formal smooth $\infty$-groupoids. Let \begin{displaymath} inf : InfPoint_\infty \hookrightarrow \mathbf{H}^{*/} \end{displaymath} be the canonical inclusion. By (\hyperlink{Lurie}{Lurie, theorem 0.0.13, remark 0.0.15}, also \hyperlink{Formal+Moduli+Problems+and+DG-Lie+Algebras#Pridham}{Pridham 07}) we have a full inclusion \begin{displaymath} Lie_\infty \hookrightarrow Sh_\infty(InfPoint_\infty) \end{displaymath} on those objects whose space of global sections is contractible and which are [[cohesive (∞,1)-presheaf on E-∞ rings|infinitesimally cohesive]] (for a somewhat different notion of ``infinitesimal cohesion'', beware the terminology). Consider then the $\infty$-functor \begin{displaymath} Grp(\mathbf{H}) \simeq \mathbf{H}^{*/}_{\geq 1} \stackrel{yoneda}{\to} PSh_\infty( \mathbf{H}^{*/}) \stackrel{inf^*}{\to} PSh_\infty(InfPoint_\infty) \end{displaymath} which sends a pointed connected formal smooth $\infty$-groupoid $\mathbf{B}G$ to the $(\infty,1)$-presheaf of pointed morphisms \begin{displaymath} \mathbf{pt} \to \mathbf{B}G \end{displaymath} for $\mathbf{pt} \in InfPoint_\infty$. By assumption that $\mathbf{B}G$ is connected (and we need to assume that it is [[geometric infinity-stack|geometric]], which will gives infinitesimal cohesion by the [[Artin-Lurie representability theorem]]) this factors as \begin{displaymath} \mathbf{H}^{*/}_{\geq 1} \stackrel{Lie}{\to} Lie_\infty \hookrightarrow Sh_\infty(InfPoint_\infty) \,. \end{displaymath} The resulting $\infty$-functor \begin{displaymath} Lie : Grp(\mathbf{H}) \simeq \mathbf{H}^{*/}_{\geq 1} \to Lie_\infty \end{displaymath} is Lie differentiation. For differentiation of smooth groupoids with [[atlas]] $U \to X$ to [[L-infinity algebroids]] this happens under $U$ \begin{displaymath} \mathbf{H}^{U/} \end{displaymath} (\ldots{}) \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[cohesive (∞,1)-topos]] \begin{itemize}% \item [[Euclidean-topological ∞-groupoid]] \end{itemize} \end{itemize} [[!include geometries of physics -- table]] \hypertarget{references}{}\subsection*{{References}}\label{references} The site [[FormalCartSp]] is discussed in section 5 of \begin{itemize}% \item [[Anders Kock]], \emph{Convenient vector spaces embed into the Cahiers topos} , Cahiers de Topologie et G\'e{}om\'e{}trie Diff\'e{}rentielle Cat\'e{}goriques, 27 no. 1 (1986), p. 3-17 (\href{http://www.numdam.org/item?id=CTGDC_1986__27_1_3_0}{numdam}). \end{itemize} For more on this see at \emph{[[Cahiers topos]]}. The notion of formally \'e{}tale maps as obtained here from the general abstract definition in [[differential cohesion]] coincided on 0-truncated objects with that defined on p. 82 of \begin{itemize}% \item [[Anders Kock]], \emph{Synthetic Differential Geometry} (1981) (\href{http://home.imf.au.dk/kock/sdg99.pdf}{pdf}) \end{itemize} The \hyperlink{StrucPaths}{infinitesimal path ∞-groupoid adjunction} $(\mathbf{Red} \dashv \mathbf{\Pi}_{inf} \dashv \mathbf{\flat}_{inf})$ and the de Rham theorem for $\infty$-stacks is discussed at the level of [[homotopy categories]] in section 3 of \begin{itemize}% \item [[Carlos Simpson]], [[Constantin Teleman]], \emph{deRham theorem for $\infty$-stacks} (\href{http://math.berkeley.edu/~teleman/math/simpson.pdf}{pdf}) \end{itemize} The $(\infty,1)$-topos $SynthDiff\infty Grpd$ is discussed in section 4.4 of \begin{itemize}% \item [[Urs Schreiber]], \emph{[[schreiber:differential cohomology in a cohesive topos]]} (\href{http://arxiv.org/abs/1310.7930}{arXiv:1310.7930}) \end{itemize} The [[cohomology localization]] of $SynthDiff\infty Grpd$ and the infinitesimal singular simplicial complex as a presentation for infinitesimal paths objects in $SynthDiff\infty Grpd$ is discussed in \begin{itemize}% \item [[Herman Stel]], \emph{$\infty$-Stacks and their function algebras -- with applications to $\infty$-Lie theory} , master thesis (2010) ([[schreiber:master thesis Stel|web]]) \end{itemize} The discussion of the cohomology localization of $SynthDiff\infty Grpd$ follows that in another context in \begin{itemize}% \item [[nLab:Bertrand Toën]], \emph{Champs affine} (\href{http://arxiv.org/abs/math/0012219}{arXiv:math/0012219}) \end{itemize} The construction of the infinitesimal path object has been amplified and discussed by [[Anders Kock]] under the name \emph{combinatorial differential forms}, for instance in \begin{itemize}% \item [[Anders Kock]], \emph{Synthetic Geometry of Manifolds} (\href{http://home.imf.au.dk/kock/SGM-final.pdf}{pdf}) \end{itemize} The discussion that the normalized [[cosimplicial algebra]] of functions on the [[infinitesimal singular simplicial complex]] is the [[de Rham complex]] is further discussed in \begin{itemize}% \item Herman Stel, \emph{[[schreiber:Cosimplicial C-infinity rings and the de Rham complex of Euclidean space]]} (\href{http://arxiv.org/abs/arXiv:1310.7407}{arXiv:arXiv:1310.7407}) \end{itemize} The results on differentiable [[Lie group cohomology]] used above is in \begin{itemize}% \item P. Blanc, \emph{Cohomologie diff\'e{}rentiable et changement de groupes} Ast\'e{}risque, vol. 124-125 (1985), pp. 113-130. \end{itemize} recalled in \begin{itemize}% \item [[Jean-Luc Brylinski]], \emph{Differentiable Cohomology of Gauge Groups} (\href{http://arxiv.org/abs/math/0011069}{arXiv}) \end{itemize} which parallels \begin{itemize}% \item [[Graeme Segal]], \emph{Cohomology of topological groups} , Symposia Mathematica, Vol IV (1970) (1986?) p. 377 \end{itemize} The $(\infty,1)$-site of derived infinitesimal points is discussed in \begin{itemize}% \item [[Jacob Lurie]], \emph{[[Formal moduli problems]]} \end{itemize} following \begin{itemize}% \item [[Vladimir Hinich]], \emph{DG coalgebras as formal stacks}, J. Pure Appl. Algebra, 162 (2001), 209-250 (\href{http://arxiv.org/abs/math/9812034}{arXiv:math/9812034}) \end{itemize} [[!redirects formal smooth infinity-groupoids]] [[!redirects formal smooth ∞-groupoid]] [[!redirects formal smooth ∞-groupoids]] [[!redirects synthetic differential infinity-groupoid]] [[!redirects synthetic differential infinity-groupoids]] [[!redirects synthetic differential ∞-groupoid]] [[!redirects synthetic differential ∞-groupoids]] [[!redirects synthetic-differential ∞-groupoid]] [[!redirects synthetic-differential ∞-groupoids]] [[!redirects formal smooth homotopy type]] [[!redirects formal smooth homotopy types]] [[!redirects formal smooth groupoid]] [[!redirects formal smooth groupoids]] [[!redirects SynthDiff∞Grpd]] [[!redirects FormalSmooth∞Groupoid]] [[!redirects FormalSmooth∞Groupoids]] [[!redirects FormalSmooth∞Grpd]] \end{document}