\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*{prequantized Lagrangian correspondence} \begin{quote}% This entry is a sub-chapter of \emph{[[geometry of physics]]}. See there for background The following is effectively a derivation of, and an introduction to, [[classical mechanics]] by studying [[correspondences]] in what is called (as we will explain) the \emph{[[slice topos]] over the [[moduli stack]] of [[prequantum line bundles]]}. One such correspondence in this slice topos is precisely a \emph{[[prequantized Lagrangian correspondence]]} and the reader looking for just these should skip ahead to the section \emph{\hyperlink{TheClassicalActionFunctionalPrequantizesHamiltonianCorrespondences}{The classical action functional prequantizes Lagrangian correspondences}}. But for completeness and to introduce the technology used here, we start with introducing also more basic concepts, such as [[phase space]] etc. \end{quote} \vspace{.5em} \hrule \vspace{.5em} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{physics}{}\paragraph*{{Physics}}\label{physics} [[!include physicscontents]] \hypertarget{symplectic_geometry}{}\paragraph*{{Symplectic geometry}}\label{symplectic_geometry} [[!include symplectic geometry - contents]] \hypertarget{classical_mechanics_via_prequantum_correspondences}{}\section*{{Classical Mechanics via Prequantum Correspondences}}\label{classical_mechanics_via_prequantum_correspondences} \noindent\hyperlink{ModelLayer}{Model Layer}\dotfill \pageref*{ModelLayer} \linebreak \noindent\hyperlink{PhaseSpaceAndSymplecticManifolds}{Phase spaces and symplectic manifolds}\dotfill \pageref*{PhaseSpaceAndSymplecticManifolds} \linebreak \noindent\hyperlink{CanonicalTransformations}{Canonical transformations and symplectomorphisms}\dotfill \pageref*{CanonicalTransformations} \linebreak \noindent\hyperlink{TrajectoriesAndLagrangianCorrespondences}{Trajectories and Lagrangian correspondences}\dotfill \pageref*{TrajectoriesAndLagrangianCorrespondences} \linebreak \noindent\hyperlink{TheClassicalActionFunctionalPrequantizesHamiltonianCorrespondences}{Hamiltonian (time evolution) trajectories and Hamiltonian correspondences}\dotfill \pageref*{TheClassicalActionFunctionalPrequantizesHamiltonianCorrespondences} \linebreak \noindent\hyperlink{KineticAction}{The kinetic action and Planck's constant}\dotfill \pageref*{KineticAction} \linebreak \noindent\hyperlink{Prequantization}{Pre-Quantization and Differential cohomology}\dotfill \pageref*{Prequantization} \linebreak \noindent\hyperlink{HamiltonianTrajectoriesAndPrequantizedLagrangianCorrespondences}{Hamiltonian flows, the Legendre transform and the Hamilton-Jacobi action}\dotfill \pageref*{HamiltonianTrajectoriesAndPrequantizedLagrangianCorrespondences} \linebreak \noindent\hyperlink{heisenberg_group_and_poisson_bracket}{Heisenberg group and Poisson bracket}\dotfill \pageref*{heisenberg_group_and_poisson_bracket} \linebreak \noindent\hyperlink{hamiltonian_actions_and_moment_maps}{Hamiltonian actions and moment maps}\dotfill \pageref*{hamiltonian_actions_and_moment_maps} \linebreak \noindent\hyperlink{SemanticsLayer}{Semantic Layer}\dotfill \pageref*{SemanticsLayer} \linebreak \noindent\hyperlink{SyntacticLayer}{Syntactic Layer}\dotfill \pageref*{SyntacticLayer} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{ModelLayer}{}\subsection*{{Model Layer}}\label{ModelLayer} Here we discuss the notion of \emph{prequantized Lagrangian correspondences} and how it serves to embed traditional [[classical mechanics]] in its formulation as [[Hamiltonian mechanics]] and [[Lagrangian mechanics]] into the general context of [[local prequantum field theory]] and its [[motivic quantization]]. A traditional notion is that of a plain \emph{[[Lagrangian correspondence]]}, which is a [[Lagrangian submanifold]] of the [[Cartesian product]] of a [[symplectic manifold]] and another one, with opposite [[symplectic structure]]. As discussed there, plain [[Lagrangian correspondences]] naturally generalize [[symplectomorphisms]] -- hence transformations between [[phase spaces]] in [[physics]] -- via [[correspondences]] of [[symplectic manifolds]]. But in [[prequantum field theory]] proper, and in particular with an eye towards [[geometric quantization]], one considers the [[prequantization]] of these symplectic manifolds by lifting them to [[prequantum circle bundles]] with [[principal connection]]. The notion of \emph{prequantized Lagrangian correspondence} is the refinement of that of plain [[Lagrangian correspondence]] which does properly respect and reflect this [[prequantization]] information: a prequantized Lagrangian correspondence is a [[Lagrangian subspace]] as before, but now equipped with an explicit [[gauge transformation]] between the pullbacks of the two [[prequantum circle bundles]] to the correspondence space. We discuss below how the concept of prequantized Lagrangian correspondences neatly induces and unifies ingredients and aspects of [[classical mechanics]], notably the [[Hamiltonian mechanics]] of [[symplectic manifolds]] and the [[Lagrangian mechanics]] of [[action functionals]] associated to it via the [[Legendre transform]]. Specifically, below in \emph{\hyperlink{TheClassicalActionFunctionalPrequantizesHamiltonianCorrespondences}{The classical action prequantizes Hamiltonian correspondences}} we see that prequantized Lagrangian correspondences are [[diagrams]] which schematically express this data as follows: \begin{displaymath} \itexarray{ && {{space\,of} \atop {trajectories}} \\ & {}^{\mathllap{{initial}\atop {values}}}\swarrow && \searrow^{\mathrlap{{Hamiltonian} \atop {evolution}}} \\ phase\,space_{in} && \swArrow_{{action} \atop {functional}} && phase \,space_{out} \\ & {}_{\mathllap{{prequantum}\atop {bundle}_{in}}}\searrow && \swarrow_{\mathrlap{{prequantum} \atop {bundle}_{out}}} \\ && {{2\text{-}group} \atop {of\,phases}} } \,. \end{displaymath} This describes a [[diagram]] in what is called the [[slice topos]] of [[smooth sets]] over the [[moduli stack]] of [[prequantum circle bundles]]. Once formulated this way, there is an evident refinement to [[moduli infinity-stack|higher moduli stacks]] of [[prequantum n-bundles]]. For $n = 2$ we show how the notion of prequantized Lagrangian correspondence is -- still naturally in the context of [[local prequantum field theory]] -- further refined from the context of [[symplectic manifolds]] to that of [[Poisson manifolds]]. Specifically, this is obtained by realizing that prequantized Lagrangian correspondences are really naturally to be regarded as correspondences-of-correspondences in a [[higher category of correspondences|2-category of correspondences]], where now the new lower-order correspondences are instead [[boundary field theories]] for a [[2d Chern-Simons theory]] (a non-perturbative [[Poisson sigma-model]]). \hypertarget{PhaseSpaceAndSymplecticManifolds}{}\subsubsection*{{Phase spaces and symplectic manifolds}}\label{PhaseSpaceAndSymplecticManifolds} Given a [[physical system]], one says that its \emph{[[phase space]]} is the space of its possible (``classical'') histories or \emph{[[trajectories]]}. The first two of [[Newton's laws of motion]] say that [[trajectories]] of [[physical systems]] are (typically) determined by [[differential equations]] of \emph{second} order, and therefore these spaces of trajectories are (typically) equivalent to initial value data of 0th and of 1st derivatives. In [[physics]] this data (or rather its linear dual) is referred to as the \emph{[[canonical coordinates]]} and the \emph{[[canonical momenta]]}, respectively, traditionally denoted by the symbols ``$q$'' and ``$p$''. But being [[coordinates]], these are actually far from being canonical in the mathematical sense; all that has invariant meaning is, locally, the surface element $\mathbf{d}p \wedge \mathbf{d}q$ spanned by a change of coordinates and momenta. So far this says that a physical phase space is mathematically formalized by a sufficiently [[smooth manifold]] $X$ which is equipped with a closed and non-degenerate [[differential 2-form]] $\omega \in \Omega^2_{\mathrm{cl}}(X)$, hence by a [[symplectic manifold]] $(X,\omega)$. The non-degeneracy of a symplectic form encodes the special property (as we will make explicit below) that (time) evolution of coordinates and momenta is uniquely induced by an [[action functional]]/[[Hamiltonian]] generating the evolution. This is however famously not the case for systems with \emph{[[gauge equivalences]]}, hence such systems which have configurations that are nominally different but nevertheless physically equivalent. Presence of such gauge equivalences is not the exception, but the rule for physical systems, and therefore we want to include this case. In the presence of gauge equivalences, the phase space form $\omega$ is still a closed differential 2-form, it just need not be non-degenerate anymore. While in such a case the pair $(X,\omega)$ could just be called a \emph{smooth manifold equipped with a closed differential 2-form\}}, it is traditional to call this a \emph{[[pre-symplectic manifold]]} in order to amplify the indented use as a model for phase spaces. (Some authors demand that a pre-symplectic form be a closed form with constant rank, but here this technical condition will not be relevant and will not be considered.) \begin{example} \label{CanonicalR2PhaseSpace}\hypertarget{CanonicalR2PhaseSpace}{} The [[sigma-model]] describing the propagation of a [[particle]] on the [[real line]] $\mathbb{R}$ has as [[phase space]] the [[plane]] $\mathbb{R}^2 = T^\ast \mathbb{R}$ and as [[symplectic form]] its canonical [[volume form]]. Traditionally the two canonical [[coordinate functions]] on this phase space are denoted $q,p \;\colon\; \mathbb{R}^2 \longrightarrow \mathbb{R}$ (called the ``[[canonical coordinate]]'' and the ``[[canonical momentum]]'', respectively), and in terms of these the symplectic form in this example is $\omega = \mathbf{d} q \wedge \mathbf{d} p$. \end{example} When dealing with spaces $X$ that are equipped with extra structure, such as $\omega \in \Omega^2_{\mathrm{cl}}(X)$, then it is useful to have a \emph{universal [[moduli space]]} for these structures, and this will be central for our developments here. So we need a ``[[smooth set]]'' $\mathbf{\Omega}^2_{\mathrm{cl}}$ of sorts, characterized by the property that there is a [[natural bijection]] between smooth closed differential 2-forms $\omega \in \Omega^2_{\mathrm{cl}}(X)$ and [[smooth maps]] $X \longrightarrow \mathbf{\Omega}^2_{\mathrm{cl}}$. Of course such a universal moduli spaces of closed 2-forms does not exist in the [[category]] of [[smooth manifolds]]. But it does exist canonically if we slightly generalize the notion of ``smooth set'' suitably. \begin{defn} \label{}\hypertarget{}{} A \emph{[[smooth set]]} or \emph{smooth 0-type} $X$ is \begin{enumerate}% \item an assignment to each $n \in \mathbb{N}$ of a set, to be written $X(\mathbb{R}^n)$ and to be called the \emph{set of smooth maps from $\mathbb{R}^n$ into $X$}, \item an assignment to each ordinary smooth function $f : \mathbb{R}^{n_1} \to \mathbb{R}^{n_2}$ between Cartesian spaces of a function of sets $X(f) : X(\mathbb{R}^{n_2}) \to X(\mathbb{R}^{n_1})$, to be called the \emph{pullback of smooth functions into $X$ along $f$}; \end{enumerate} such that \begin{enumerate}% \item this assignment respects composition of smooth functions; \item this assignment respects the [[covering]] of [[Cartesian spaces]] by [[open disks]]: for every [[good open cover]] $\{\mathbb{R}^n \simeq U_i \hookrightarrow \mathbb{R}^n\}_i$, the set $X(\mathbb{R}^n)$ of smooth functions out of $\mathbb{R}^n$ into $X$ is in natural bijection with the set $\left\{ (\phi_i)_i \in \prod_i X(U_i) \;|\; \forall_{i,j}\; \phi_i|_{U_{i} \cap U_j} = \phi_j|_{U_{i} \cap U_j} \right\}$ of tuples of smooth functions out of the patches of the cover which agree on all intersections of two patches. \end{enumerate} \end{defn} For more on this see at \emph{[[geometry of physics]]} in the section \emph{\href{geometry%20of%20physics#SmoothSpaces}{Smooth sets}}. While the formulation of this definition is designed to make transparent its geometric meaning, of course equivalently but more abstractly this says the following: \begin{defn} \label{SheavesOnCartSp}\hypertarget{SheavesOnCartSp}{} Write [[CartSp]] for the [[category]] of [[Cartesian spaces]] with [[smooth functions]] between them, and consider it as a [[site]] by equipping it with the [[coverage]] of [[good open covers]]. A \emph{[[smooth set]]} or \emph{smooth 0-type} is a [[sheaf]] on this site. The \emph{[[topos]] of smooth 0-types} is the [[category of sheaves]] \begin{displaymath} \mathrm{Smooth}0\mathrm{Type} \coloneqq \mathrm{Sh}(\mathrm{CartSp}) \,. \end{displaymath} \end{defn} In the following we will abbreviate the notation to \begin{displaymath} \mathbf{H} \coloneqq \mathrm{Smooth}0\mathrm{Type} \,. \end{displaymath} The topos of prop. \ref{SheavesOnCartSp} also has another site of definition. \begin{prop} \label{Smooth0TypeIsSheavesOnSmoothMfd}\hypertarget{Smooth0TypeIsSheavesOnSmoothMfd}{} Write $SmoothMfd$ for the [[category]] of [[smooth manifolds]] regarded as a [[site]] with the standard [[Grothendieck topology]] of [[open covers]]. There is an [[equivalence of categories]] \begin{displaymath} Sh(SmoothMfd) \simeq \mathrm{Smooth}0\mathrm{Type} \,. \end{displaymath} \end{prop} \begin{proof} The canonical inclusion $CartSp\hookrightarrow SmoothMfd$ is readily seen to be a [[dense subsite]]. (This is just the statement that -- by definition -- every smooth manifold may be covered by Cartesian spaces.) The statement hence follows by the [[comparison lemma]]. \end{proof} For the discussion of presymplectic manifolds, we need the following two examples. \begin{example} \label{}\hypertarget{}{} Every smooth manifold $X \in \mathrm{SmoothManifold}$ becomes a smooth 0-type by the assignment \begin{displaymath} X \;\colon\; n \mapsto C^\infty(\mathbb{R}^n, X) \,. \end{displaymath} This construction extends to a [[full subcategory|full embedding]] of [[smooth manifolds]] into [[smooth sets]] \begin{displaymath} SmoothManifold \hookrightarrow \mathbf{H} \end{displaymath} \end{example} \begin{proof} This follows via prop. \ref{Smooth0TypeIsSheavesOnSmoothMfd} by the [[Yoneda lemma]]. \end{proof} \begin{example} \label{SmoothSetOfDifferentialPForms}\hypertarget{SmoothSetOfDifferentialPForms}{} For $p \in \mathbb{N}$, write $\mathbf{\Omega}^p_{\mathrm{cl}}$ for the [[smooth set]] whose $n$-dimensional plots are smooth [[differential p-forms]] on $\mathbb{R}^n$: \begin{displaymath} \mathbf{\Omega}^p_{\mathrm{cl}} \colon \mathbb{R}^n \mapsto \Omega^p_{\mathrm{cl}}(\mathbb{R}^n) \end{displaymath} and which sends a [[smooth function]] $f \colon \mathbb{R}^{n_1} \to \mathbb{R}^{n_2}$ to the [[pullback of differential forms]] along this map \begin{displaymath} \itexarray{ \mathbb{R}^{n_1} &\mapsto& \Omega^p_cl(\mathbb{R}^{n_1}) \\ \downarrow^{\mathrlap{f}} && \uparrow^{\mathrlap{f^\ast}} \\ \mathbb{R}^{n_2} &\mapsto& \Omega^p_cl(\mathbb{R}^{n_2}) } \,. \end{displaymath} \end{example} For more on this example see at \emph{[[geometry of physics]]} in the section \emph{\href{geometry%20of%20physics#DifferentialForms}{Differential forms}}. This solves the [[moduli problem]] for closed smooth differential forms: \begin{prop} \label{PresymplecticFormsAsMapsIntoASmoothSpace}\hypertarget{PresymplecticFormsAsMapsIntoASmoothSpace}{} For $p \in \mathbb{N}$ and $X \in SmoothManifold \hookrightarrow Smooth0Type$, there is a [[natural bijection]] \begin{displaymath} \mathbf{H}(X,\mathbf{\Omega}^p_{\mathrm{cl}}) \simeq \Omega^p_{\mathrm{cl}}(X) \end{displaymath} between morphisms (of smooth sets) \begin{displaymath} X \longrightarrow \Omega^2_{cl} \end{displaymath} and smooth closed 2-forms \begin{displaymath} \omega \in \Omega^2_{cl}(X) \end{displaymath} on $X$. \end{prop} \begin{proof} This follows via prop. \ref{Smooth0TypeIsSheavesOnSmoothMfd} by the [[Yoneda lemma]]. \end{proof} So a [[presymplectic manifold]] $(X,\omega)$ is equivalently a map of smooth sets of the form \begin{displaymath} \omega \;\colon\; X \longrightarrow \mathbf{\Omega}^2_{\mathrm{cl}} \,. \end{displaymath} \hypertarget{CanonicalTransformations}{}\subsubsection*{{Canonical transformations and symplectomorphisms}}\label{CanonicalTransformations} An [[equivalence]] between two [[phase spaces]], hence a re-expression of the ``[[canonical coordinates]]'' and ``[[canonical momenta]]'', is called a \emph{[[canonical transformation]]} in [[physics]]. Mathematically this is a \emph{[[symplectomorphism]]}. \begin{defn} \label{}\hypertarget{}{} Given two [[symplectic manifolds]] $(X_1, \omega_1)$ and $(X_2, \omega_2)$ (which might be two copies of one single symplectic manifold), a \emph{[[symplectomorphism]]} between them \begin{displaymath} f \;\colon\; (X_1, \omega_1) \longrightarrow (X_2, \omega_2) \end{displaymath} is a [[diffeomorphism]] \begin{displaymath} f \;\colon\; X_1 \longrightarrow X_2 \end{displaymath} of the underlying [[smooth manifolds]], such that the [[pullback of differential forms|pullback]] of the second [[symplectic form]] along $f$ equals the first, \begin{displaymath} f^\ast \omega_2 = \omega_1 \,. \end{displaymath} \end{defn} The above formulation of pre-symplectic manifolds as maps into a [[moduli space]] of closed [[differential 2-forms]] yields the following formulation of symplectomorphisms, which is very simple in itself, but contains in it the seed of an important phenomenon: \begin{prop} \label{Symplectomorphism}\hypertarget{Symplectomorphism}{} A [[symplectomorphism]] $f \colon (X_1, \omega_2) \longrightarrow (X_2, \omega_2)$ as above is, under the identification of prop. \ref{PresymplecticFormsAsMapsIntoASmoothSpace}, equivalently a [[commuting diagram]] in $\mathbf{H}$ of the form \begin{displaymath} \itexarray{ X_1 && \stackrel{f}{\longrightarrow}&& X_2 \\ & {}_{\mathllap{\omega_1}}\searrow && \swarrow_{\mathrlap{\omega_2}} \\ && \Omega^2_{cl} } \,. \end{displaymath} \end{prop} \begin{proof} This is the [[natural transformation|naturality]] of the [[Yoneda lemma]]: By prop. \ref{PresymplecticFormsAsMapsIntoASmoothSpace} the identification of $\omega_i \in \Omega^2_{cl}(X_i)$ with $\omega_i \colon X \to \Omega^2_{cl}$ is via the [[natural equivalence]] \begin{displaymath} Hom_{Smooth0Type}(X,\mathbf{\Omega}^2_{cl}) \stackrel{\simeq}{\longrightarrow} \Omega^2_{cl}(X) \,. \end{displaymath} This being natural means that for every morphism $X_1 \stackrel{f}{\longrightarrow} X_2$ there is a [[commuting diagram]] of the form \begin{displaymath} \itexarray{ Hom(X_2,\mathbf{\Omega}^2_{cl}) &\stackrel{\simeq}{\longrightarrow}& \Omega^2_{cl}(X_2) \\ \downarrow^{\mathrlap{(-) \circ f}} && \downarrow^{\mathrlap{f^\ast}} \\ Hom(X_1,\mathbf{\Omega}^2_{cl}) &\stackrel{\simeq}{\longrightarrow}& \Omega^2_{cl}(X_1) } \end{displaymath} where on the left we have the pre-[[composition]] operation on morphisms and on the right we have, by example \ref{SmoothSetOfDifferentialPForms}, the [[pullback of differential forms]]. Consider then the element \begin{displaymath} (X_2 \stackrel{\omega_2}{\to} \mathbf{\Omega}^2_{cl}) \in Hom(X_2,\mathbf{\Omega}^2_{cl}) \end{displaymath} in the top left set in this diagram. Sending it along the top and right maps yields the [[pullback of differential forms]] $f^\ast \omega_2 \in \Omega^2_{cl}(X_1)$. On the other hand, sending it along the left and bottom maps yields the differential form represented by the composite morphism $(X_1 \stackrel{f}{\to} X_2 \stackrel{\omega_1}{\to}\mathbf{\Omega}^2_{cl})$. Commutativity of the above naturality diagram means that these two elements of $\Omega^2_{cl}(X_1)$ coincide. This is the claim to be proven. \end{proof} Situations like this are naturally interpreted in a \emph{[[slice topos]]}: \begin{defn} \label{TheSliceTopos}\hypertarget{TheSliceTopos}{} For $A \in \mathbf{H}$ any [[smooth set]], the \emph{[[slice topos]]} $\mathbf{H}_{/A}$ is the [[category]] whose [[objects]] are objects $X \in \mathbf{H}$ equipped with [[maps]] $X \to A$, and whose [[morphisms]] are [[commuting diagrams]] in $\mathbf{H}$ of the form \begin{displaymath} \itexarray{ X &&\longrightarrow&& Y \\ & \searrow && \swarrow \\ && A } \end{displaymath} \end{defn} \begin{defn} \label{}\hypertarget{}{} Write $\mathrm{SymplManifold}$ for the [[category]] with [[symplectic manifold|presymplectic]] [[smooth manifolds]] as [[objects]] and [[symplectomorphisms]], def. \ref{Symplectomorphism}, betwen them as [[morphisms]] \end{defn} \begin{prop} \label{SymplecticManifoldsAsObjectsInSliceOverModuliOf2Forms}\hypertarget{SymplecticManifoldsAsObjectsInSliceOverModuliOf2Forms}{} The construction of prop. \ref{PresymplecticFormsAsMapsIntoASmoothSpace} which sends a smooth symplectic manifold $(X,\omega)$ to the classifying morphism of smooth sets $(X \stackrel{\omega}{\longrightarrow}\mathbf{\Omega}^2_{cl})$ regarded as an object in the [[slice topos]], def. \ref{TheSliceTopos} constitutes a [[full and faithful functor]] \begin{displaymath} SymplManifold \hookrightarrow Smooth0Type_{/\mathbf{\Omega}^2_{\mathrm{cl}}} \end{displaymath} of pre-symplectic manifolds with symplectomorphisms between them into the slice topos of smooth sets over the smooth moduli space of closed differential 2-forms. \end{prop} \begin{proof} By prop. \ref{Symplectomorphism}. \end{proof} \hypertarget{TrajectoriesAndLagrangianCorrespondences}{}\subsubsection*{{Trajectories and Lagrangian correspondences}}\label{TrajectoriesAndLagrangianCorrespondences} A [[symplectomorphism]] clearly puts two [[symplectic manifolds]] ``in \emph{[[relation]]}'' to each other. But it does so also in the formal sense of [[relations]] in mathematics. Recall: \begin{defn} \label{}\hypertarget{}{} For $X,Y \in$ [[Set]] two [[sets]], a [[relation]] $R$ between [[elements]] of $X$ and [[elements]] of $Y$ is a [[subset]] of the [[Cartesian product]] set \begin{displaymath} R \hookrightarrow X \times Y \,. \end{displaymath} More generally, for $X, Y \in \mathbf{H}$ two [[objects]] of a [[topos]] (such as the topos of [[smooth sets]]), then a [[relation]] $R$ between them is a [[subobject]] of their [[Cartesian product]] \begin{displaymath} R \hookrightarrow X \times Y \,. \end{displaymath} \end{defn} In particular any [[function]] induces the [[relation]] ``$y$ is the image of $x$'': \begin{example} \label{FunctionsAsCorrespondences}\hypertarget{FunctionsAsCorrespondences}{} For $f \;\colon\; X \longrightarrow Y$ a [[function]], its \emph{induced relation} is the [[relation]] which is exhibited by the [[graph of a function|graph]] of $f$ \begin{displaymath} graph(f) \coloneqq \left\{ (x,y) \in X \times Y \;|\; f(x) = y \right\} \end{displaymath} canonically regarded as a subobject \begin{displaymath} graph(f) \hookrightarrow X \times Y \,. \end{displaymath} \end{example} Hence in the context of classical mechanics, in particular any [[symplectomorphism]] $f \;\colon\; (X_1, \omega_1) \longrightarrow (X_2, \omega_2)$ induces the relation \begin{displaymath} graph(f) \hookrightarrow X_1 \times X_2 \,. \end{displaymath} Since we are going to think of $f$ as a kind of ``physical process'', it is useful to think of the [[smooth set]] $graph(f)$ here as the \emph{space of [[trajectories]]} of that process. To make this clearer, notice that we may equivalently rewrite every [[relation]] $R \hookrightarrow X \times Y$ as a [[diagram]] of the following form: \begin{displaymath} \itexarray{ && R \\ & {}^{\mathllap{i_X}}\swarrow && \searrow^{\mathrlap{i_Y}} \\ X && && Y } \;\; = \;\; \itexarray{ && R \\ && \downarrow \\ && X \times Y \\ & {}^{\mathllap{p_X}}\swarrow && \searrow^{\mathrlap{p_Y}} \\ X && && Y } \end{displaymath} reflecting the fact that every [[element]] $(x \sim y) \in R$ defines an element $x = i_X(x \sim y) \in X$ and an element $y = i_Y(x \sim y) \in Y$. Then if we think of $R = graph(f)$ we may read the relation as ``there is a trajectory from an incoming configuration $x_1$ to an outgoing configuration $x_2$'' \begin{displaymath} \itexarray{ && graph(f) \\ & {}^{\mathllap{incoming}}\swarrow && \searrow^{\mathrlap{outgoing}} \\ X_1 && && X_2 } \,. \end{displaymath} Notice here that the defining property of a relation as a [[subset]]/[[subobject]] translates into the property of [[classical physics]] that there is \emph{at most one trajectory} from some incoming configuration $x_1$ to some outgoing trajectory $x_2$ (for a fixed parameter time interval at least, we will formulate this precisely in the next section when we genuinely consider Hamiltonian correspondences). In a more general context one could consider there to be several such trajectories, and even a whole smooth set of such trajectories between given incoming and outgoing configurations. Each such trajectory would ``relate'' $x_1$ to $x_2$, but each in a possible different way. We can also say that each trajectory makes $x_1$ \emph{correspond} to $x_2$ in a different way, and that is the mathematical term usually used: \begin{defn} \label{CorrespondencesAndEquivalences}\hypertarget{CorrespondencesAndEquivalences}{} For $X, Y \in \mathbf{H}$ two spaces, a [[correspondence]] between them is a [[diagram]] in $\mathbf{H}$ of the form \begin{displaymath} \itexarray{ && Z \\ & \swarrow && \searrow \\ X && && Y } \end{displaymath} with no further restrictions. Here $Z$ is also called the \emph{[[correspondence space]]}. An [[equivalence]] between two such correspondences is an equivalence $Z_1 \stackrel{\simeq}{\to}Z_2$ that gives a [[commuting diagram]] of the form \begin{displaymath} \itexarray{ && Z_1 \\ & {}^{}\swarrow && \searrow^{} \\ X &&\downarrow^{\mathrlap{\simeq}} && Y \\ & {}_{}\nwarrow && \nearrow_{} \\ && Z_2 } \end{displaymath} Correspondences between $X$ any $Y$ with such equivalences between them form a \emph{[[groupoid]]}. (See at \emph{[[geometry of physics]]} the section \emph{\href{geometry%20of%20physics#GroupoidsAndBasicHomotopy1TypeTheory}{Essence of gauge theory: Groupoids and basic homotopy 1-type theory}} for more on this.) Hence we write \begin{displaymath} Corr\left(\mathbf{H}\right)(X,Y) \in Grpd \,. \end{displaymath} \end{defn} \begin{example} \label{EquivalenceOfCorrespndencesInducedByFunction}\hypertarget{EquivalenceOfCorrespndencesInducedByFunction}{} The correspondence induced by the [[graph of a function]] $f \colon X \to Y$ as in example \ref{FunctionsAsCorrespondences} is equivalent, in the sense of def. \ref{CorrespondencesAndEquivalences}, to the correspondence \begin{displaymath} \itexarray{ && X \\ & {}^{\mathllap{id}}\swarrow && \searrow^{\mathrlap{f}} \\ X && && Y } \,. \end{displaymath} The equivalence \begin{displaymath} \itexarray{ && X \\ & {}^{\mathllap{id}}\swarrow && \searrow^{\mathrlap{f}} \\ X &&\downarrow^{\mathrlap{\simeq}} && Y \\ & {}_{\mathllap{i_X}}\nwarrow && \nearrow_{\mathrlap{i_Y}} \\ && graph(f) } \end{displaymath} is induced by \begin{displaymath} X \stackrel{\simeq}{\longrightarrow} graph(f) \end{displaymath} \begin{displaymath} x \mapsto (x,f(x)) \end{displaymath} \end{example} Moreover, if we think of correspondences as modelling spaces of [[trajectories]], then it is clear that their should be a notion of [[composition]]: \begin{defn} \label{}\hypertarget{}{} Given two consecutive correspondences, then their \emph{composite} is the correspondence obtained by forming the [[fiber product]] of the two coincident morphisms: \begin{displaymath} \left( \itexarray{ && Y_1 &&&& Y_2 \\ & \swarrow && \searrow && \swarrow && \searrow \\ X_1 && && X_2 && && X_3 } \right) \;\;\;\; \mapsto \;\;\;\; \left( \itexarray{ && Y_1 \circ_{X_2} Y_2 \\ & \swarrow && \searrow \\ X_1 && && X_3 } \right) \,. \end{displaymath} \end{defn} \begin{remark} \label{}\hypertarget{}{} Heuristically, the composite space of trajectories $Y_1 \circ_{X_2} Y_2$ should consist precisely of those pairs of trajectories $( f, g ) \in Y_1 \times Y_2$ such that the endpoint of $f$ is the starting point of $g$. The space with this property is precisely the \emph{[[fiber product]]} of $Y_1$ with $Y_2$ over $X_2$, denoted $Y_1 \underset{X_2}{\times} Y_2$ (also called the [[pullback]] of $Y_2 \longrightarrow X_2$ along $Y_1 \longrightarrow X_2$ and then abbreviated $(pb)$): \begin{displaymath} \left( \itexarray{ && Y_1 \circ_{X_2} Y_2 \\ & \swarrow && \searrow \\ X_1 && && X_3 } \right) \;\;\; = \;\;\; \left( \itexarray{ && && Z_1 \underset{Y}{\times} Z_2 \\ && & \swarrow && \searrow \\ && Z_1 && (pb) && Z_2 \\ & \swarrow && \searrow && \swarrow && \searrow \\ X && && Y && && Z } \right) \,. \end{displaymath} Hence given a [[topos]] $\mathbf{H}$, [[correspondences]] between its objects form a [[category]] which [[composition]] the [[fiber product]] operation, where however the collection of [[morphisms]] between any two objects is not just a [[set]], but is a [[groupoid]] (the groupoid of correspondences between two given objects and [[equivalences]] between them). \end{remark} One says that correspondences form a \emph{[[(2,1)-category]]} \begin{displaymath} Corr(\mathbf{H}) \in (2,1)Cat \,. \end{displaymath} But for most purposes here, the reader unwilling to enter [[higher category theory]] can, to good approximation, pretend that correspondences form an ordinary [[category]]. One reason for formalizing this notion of correspondences so much in the present context that it is useful now to apply it not just to the ambient [[topos]] $\mathbf{H}$ of [[smooth sets]], but also to its [[slice topos]] $\mathbf{H}_{/\mathbf{\Omega}_{cl}^2}$ over the universal [[moduli space]] of closed [[differential 2-forms]]. To see how this is useful in the present context, notice the following basic observation: \begin{defn} \label{}\hypertarget{}{} Given a [[symplectic manifold]] $(X,\omega)$, then a [[submanifold]] \begin{displaymath} L \hookrightarrow X \end{displaymath} is called \begin{itemize}% \item an \emph{[[isotropic submanifold]]} if $\omega|_{L}= 0$; \item a \emph{[[Lagrangian submanifold]]} if in addition $L$ has [[dimension]] $dim(L) = dim(X)/2$. \end{itemize} \end{defn} \begin{prop} \label{}\hypertarget{}{} Let $f \colon X_1 \to X_2$ be a [[smooth function]] between [[smooth manifolds]] and let \begin{displaymath} \itexarray{ && graph(f) \\ && \downarrow \\ && X_1 \times X_2 \\ & {}^{\mathllap{p_1}}\swarrow && \searrow^{\mathrlap{p_2}} \\ X_1 && && X_2 } \end{displaymath} be the induced [[correspondence]]. If $\omega_1$ and $\omega_2$ are [[symplectic forms]] on $X_1$ and $X_2$, respectively, then $p_1^\ast \omega_1 - p_2^\ast \omega_2$ is a pre-symplectic form on $X_1 \times X_2$, and $f$ is a [[symplectomorphism]] precisely if $graph(f) \hookrightarrow X_1 \times X_2$ is a [[Lagrangian submanifold]]. \end{prop} To capture this phenomenon, one traditionally sets: \begin{defn} \label{LagrangianCorrespondence}\hypertarget{LagrangianCorrespondence}{} For $(X_1,\omega_1)$ and $(X_2,\omega_2)$ two [[symplectic manifolds]] (not necessarily of the same [[dimension]]), an \emph{isotropic correspondence} or \emph{[[Lagrangian correspondence]]} between them is a [[correspondence]] of the underlying [[manifolds]] \begin{displaymath} \itexarray{ && R \\ && \downarrow \\ && X_1 \times X_2 \\ & {}^{\mathllap{p_1}}\swarrow && \searrow^{\mathrlap{p_2}} \\ X_1 && && X_2 } \end{displaymath} such that the [[correspondence space]] $R \hookrightarrow X_1 \times X_2$ is an [[isotropic submanifold]] or [[Lagrangian submanifold]], respectively of the product symplectic manifold given by \begin{displaymath} (X_1 \times X_2 , p_1^\ast \omega_1 - p_2^\ast \omega_2) \,. \end{displaymath} \end{defn} \begin{prop} \label{IsotropicCorrespondenceDiagrammatically}\hypertarget{IsotropicCorrespondenceDiagrammatically}{} Under the identification of prop. \ref{PresymplecticFormsAsMapsIntoASmoothSpace}, isotropic correspondences as in def. \ref{LagrangianCorrespondence} are equivalent to diagrams of [[smooth sets]] of the form \begin{displaymath} \itexarray{ && R \\ & {}^{\mathllap{p_1}}\swarrow && \searrow^{\mathrlap{p_2}} \\ X_1 && \swArrow_= && X_2 \\ & {}_{\mathllap{\omega_1}}\searrow && \swarrow_{\mathrlap{\omega_2}} \\ && \Omega^2_{cl} } \,. \end{displaymath} This in turn is equivalent to being a [[correspondence]] in the [[slice topos]] $\mathbf{H}_{/\Omega^2_{cl}}$, def. \ref{TheSliceTopos}, under the identification of prop. \ref{SymplecticManifoldsAsObjectsInSliceOverModuliOf2Forms}. \end{prop} \begin{proof} By prop. \ref{Symplectomorphism} the commutativity of this diagram says precisely that on $R$ we have \begin{displaymath} p_1^\ast \omega_1 = p_2^\ast \omega_2 \end{displaymath} hence \begin{displaymath} p_1^\ast \omega_1 - p_2^\ast \omega_2 = 0 \,. \end{displaymath} \end{proof} Therefore we have: \begin{prop} \label{}\hypertarget{}{} For $(X_1, \omega_2)$ and $(X_2, \omega_2)$ two [[symplectic manifolds]], there is a [[full subcategory|full embedding]] \begin{displaymath} LagrangianCorrespondences\left(\left(X_1,\omega_1\right), \left(X_2, \omega_2\right)\right) \hookrightarrow Corr\left(\mathbf{H}_{/\mathbf{\Omega}^2_{cl}}\right)\left(\left(X_1,\omega_1\right), \left(X_2, \omega_2\right)\right) \end{displaymath} of the Lagrangian correspondences into the space of correspondences between the two manifolds as objects in the [[slice topos]] over the universal moduli space of closed differential 2-forms. \end{prop} \begin{example} \label{}\hypertarget{}{} The [[graph of a function]] $f \colon X_1\to X_2$ between [[symplectic manifold]] $(X_i, \omega_i)$ is a [[Lagrangian correspondence]] precisely if $f$ is a [[symplectomorphism]]. \end{example} \begin{proof} Under the identification of \begin{displaymath} \itexarray{ && graph(f) \\ & {}^{\mathllap{p_1}}\swarrow && \searrow^{\mathrlap{p_2}} \\ X_1 && && X_2 } \end{displaymath} \end{proof} \hypertarget{TheClassicalActionFunctionalPrequantizesHamiltonianCorrespondences}{}\subsubsection*{{Hamiltonian (time evolution) trajectories and Hamiltonian correspondences}}\label{TheClassicalActionFunctionalPrequantizesHamiltonianCorrespondences} An important class of [[symplectomorphisms]] are the following \begin{defn} \label{HamiltonianCorrespondence}\hypertarget{HamiltonianCorrespondence}{} Let $(X,\omega)$ be a [[symplectic manifold]]. The induced [[Poisson bracket]] $\{-,-\}$ takes a [[smooth function]] $H \in C^\infty(X)$ (the ``[[Hamiltonian]]'') to the [[derivation]] $\{H,-\}$ on $C^\infty(X)$. This is equivalently a [[vector field]] $v_H \in \Gamma T X$, the corresponding [[Hamiltonian vector field]]. A [[Hamiltonian symplectomorphisms]] from a [[symplectic manifold]] $(X,\omega)$ to itself, is a [[symplectomorphism]] $X \to X$ which is the [[flow]] of a [[Hamiltonian vector field]] for some parameter ``time'' $t \in \mathbb{R}$ \begin{displaymath} \exp( t \{H,-\}) \;\colon\; (X,\omega) \longrightarrow (X,\omega) \,. \end{displaymath} We call a [[Lagrangian correspondence]], def. \ref{LagrangianCorrespondence}, induced from [[Hamiltonian symplectomorphisms]] a \emph{Hamiltonian correspondences}. \end{defn} \begin{remark} \label{HamiltonianCorrespondencesAreSpacesOfTrajectories}\hypertarget{HamiltonianCorrespondencesAreSpacesOfTrajectories}{} Under the interpretation of [[correspondences]] as spaces of [[trajectories]] as in example \ref{FunctionsAsCorrespondences}, the [[smooth set|smooth]] [[correspondence space]] of a Hamiltonian correspondence is naturally identified with the space of \emph{classical [[trajectories]]} of the [[Hamiltonian mechanics|Hamiltonian]] [[dynamics]] of $H$ \begin{displaymath} Fields_{traj}^{class}(t) = graph\left( \exp(t\{H,-\}) \right) \end{displaymath} in that \begin{enumerate}% \item every point in the space corresponds uniquely to a [[trajectory]] of parameter time length $t$ characterized as satisfying the [[equations of motion]] as given by [[Hamilton's equations]] for $H$; \item the two projection maps to $X$ send a trajectory to its initial and to its final configuration, respectively. \end{enumerate} \end{remark} \begin{remark} \label{}\hypertarget{}{} Forming Hamiltonian correspondences consitutes a [[functor]] from 1-dimensional [[cobordisms]] with [[Riemannian structure]] to the [[category of correspondences]] in the [[slice topos]]: \begin{displaymath} \exp((-)\{H,-\}) \;\colon\; Bord^{Riem}_1 \longrightarrow Corr_1(\mathbf{H}_{/\Omega^2}) \end{displaymath} since for all (``time'') parameter valued $t_1, t_2 \in \mathbb{R}$ we have a [[composition]] (by [[fiber product]]) of [[correspondences]] exhibited by the following [[pasting diagram]]: \begin{displaymath} \itexarray{ &&&& graph\left(\exp\left(\left(t_1+t_2\right)\right) \left\{H,-\right\} \right) \\ && & \swarrow && \searrow \\ && graph\left(\exp\left(t_1\right)\left\{H,-\right\}\right) && (pb) && graph\left(\exp\left(t_2 \left\{H,-\right\}\right)\right) \\ & \swarrow && \searrow & & \swarrow && \searrow \\ X && && X && && X \\ & \searrow &&& \downarrow &&& \swarrow \\ &&&& \Omega^2_{cl} } \,. \end{displaymath} \end{remark} \hypertarget{KineticAction}{}\subsubsection*{{The kinetic action and Planck's constant}}\label{KineticAction} To naturally see why there would be any [[Hamiltonian]] associated to a (to some) [[symplectomorphism]] in the first place, we step back and consider \emph{local trivializations} or \emph{local potentials} for [[symplectic forms]]. Doing so turns out to give rise to what in physics is called the [[kinetic action]], what in the context of [[geometric quantization]] is called [[prequantization]] and what in [[mathematics]] is called lifting to \emph{[[differential cohomology]]}. All these concepts arise directly from the following simple consideration. Given a [[pre-symplectic form]] $\omega \in \Omega^2_{\mathrm{cl}}(X)$, by the [[Poincaré lemma]] there is a [[good open cover]] $\{U_i \hookrightarrow X\}_i$ such that one can find smooth [[differential 1-forms]] $\theta_i \in \Omega^1(U_i)$ such that these are local trivializations/potentials for the [[symplectic form]] on each patch $U_i$ of the cover: \begin{displaymath} \mathbf{d}\theta_i = \omega_{|U_i} \,. \end{displaymath} Physically such a 1-form is (up to a factor of 2) a choice of \emph{[[kinetic energy]] [[density]]} called a \emph{[[kinetic Lagrangian]]} $L_{\mathrm{kin}}$ (below in example \ref{StandardPrequantizationOfStandardR2PhaseSpace} we connect this statement to a maybe more familiar formla): \begin{displaymath} \theta_i = 2 L_{\mathrm{kin}, i} \,. \end{displaymath} \begin{example} \label{StandardPrequantizationOfStandardR2PhaseSpace}\hypertarget{StandardPrequantizationOfStandardR2PhaseSpace}{} Consider the [[phase space]] $(\mathbb{R}^2, \; \omega = \mathbf{d} q \wedge \mathbf{d} p)$ of example \ref{CanonicalR2PhaseSpace}. Since $\mathbb{R}^2$ is a [[contractible topological space]] we consider the trivial [[covering]] ($\mathbb{R}^2$ covering itself) since this is already a [[good covering]] in this case. Then all the $\{g_{i j}\}$ are trivial and the data of a [[prequantization]] consists simply of a choise of 1-form $\theta \in \Omega^1(\mathbb{R}^2)$ such that \begin{displaymath} \mathbf{d}\theta = \mathbf{d}q \wedge \mathbf{d}p \,. \end{displaymath} A standard such choice is \begin{displaymath} \theta = - p \wedge \mathbf{d}q \,. \end{displaymath} Then given a [[trajectory]] $\gamma \colon [0,1] \longrightarrow X$ which satisfies [[Hamilton's equation]] for a standard [[kinetic energy]] term, then $(p \mathbf{d}q)(\dot\gamma)$ is this [[kinetic energy]] of the [[particle]] which traces out this [[trajectory]]. \end{example} Given a path $\gamma : [0,1] \to X$ in phase space, its \emph{[[kinetic action]]} $S_{\mathrm{kin}}$ is supposed to be the integral of $L_{\mathrm{kin}}$ along this trajectory. In order to make sense of this in the generality where there is no globally defined $\theta$, there need to be functions $g_{i j} \in C^\infty(U_i \cap U_j, \mathbb{R})$ for each double intersection of patches of the cover, such that these the local $\theta$`s differ on these double intersection only by the total [[derivative]] ([[de Rham cohomology|de Rham]] [[differential]] $\mathbf{d}$ ) of these functions: \begin{displaymath} \theta_j|_{U_j} - \theta_i|_{U_i} = \mathbf{d}g_{i j} \,. \end{displaymath} One then finds (from the theory of [[Cech cohomology]]) that if on triple intersections these functions satisfy \begin{displaymath} g_{ij} + g_{j k} = g_{i k} \end{displaymath} then there is a well defined action functional \begin{displaymath} S_{\mathrm{kin}}(\gamma) \in \mathbb{R} \end{displaymath} obtained by dividing $\gamma$ into small pieces that each map to a single patch $U_i$, integrating $\theta_i$ along this piece, and adding the contribution of $g_{i j}$ at the point where one switches from using $\theta_i$ to using $\theta_j$. Technically this is called the [[holonomy]] or [[parallel transport]] of the $(\mathbb{R},+)$-[[principal connection]] which is defined by the data $(\{\theta_i\}, \{g_{i j}\} )$. However, requiring this condition on triple overlaps as an equation between $\mathbb{R}$-valued functions makes the local patch structure trivial: if this is possible then one can in fact already find a single $\theta \in \Omega^1(X)$ and functions $h_i \in C^\infty(U_i, \mathbb{R})$ such that $\theta_i = \theta|_{U_i} + \mathbf{d}h_i$. This has the superficially pleasant effect that the action is simply the integral against this globally defined 1-form, $S_{\mathrm{kin}} = \int_{[0,1]} \gamma^\ast L_{\mathrm{kin}}$, but it also means that the pre-symplectic form $\omega$ is exact, which is not the case in many important examples. (In more abstract terms what this is saying is that every $(\mathbb{R},+)$-[[principal bundle]] over a manifolds is trivializable.) On the other hand, what really matters in [[prequantum field theory|prequantum]] [[physics]] is not the [[action functional]] $S_{\mathrm{kin}} \in \mathbb{R}$ itself, but the \emph{exponentiated} action \begin{displaymath} \exp\left( \tfrac{i}{\hbar} S \right) \in \mathbb{R}/(2\pi \hbar)\cdot\mathbb{Z} \,, \end{displaymath} which takes values in the [[quotient]] of the additive group of [[real numbers]] by [[integer|integral]] multiples of [[Planck's constant]] $2\pi \hbar$. In more detail, consider the canonical inclusion \begin{displaymath} \mathbb{Z} \hookrightarrow \mathbb{R} \end{displaymath} of the [[integers]] as an addiditve [[subgroup]] of the [[real numbers]]. Strictly speaking what appears in [[physics]] is the [[real line]] on which a [[unit]] is chosen as part of the identification of mathematical formalism with physical reality, one should really consider \emph{all} possible additive group homomorphisms $\mathbb{Z}\to \mathbb{R}$. These are parameterized by \begin{displaymath} h \in (\mathbb{R}- \{0\}) \hookrightarrow \mathbb{R} \end{displaymath} \begin{displaymath} (-)\cdot h \;\colon\; \mathbb{Z} \longrightarrow \mathbb{R} \end{displaymath} and this ``physical [[unit]]'' $h$ is what is called \emph{Planck's constant}. In particular the induced [[circle group]] is identified as the [[quotient]] of $\mathbb{R}$ by $h \mathbb{Z}$, in this sense \begin{displaymath} U(1) \simeq \mathbb{R}/h \mathbb{Z} \end{displaymath} and under this identification its [[quotient]] map is expressed in terms of the [[exponential function]] $\exp \colon z \mapsto \sum_{k = 0}^\infty \frac{z^k}{k!} \in \mathbb{C}$ as \begin{displaymath} \exp(2 \pi \tfrac{i}{h}(-)) = \exp(\tfrac{i}{\hbar} (-)) \;\colon\; \mathbb{R} \longrightarrow U(1) \,, \end{displaymath} where \begin{displaymath} \hbar \coloneqq h/2\pi \,. \end{displaymath} The resulting [[short exact sequence]] is the real [[exponential exact sequence]] \begin{displaymath} 0 \to \mathbb{Z} \longrightarrow \mathbb{R} \stackrel{\exp(\tfrac{i}{\hbar}(-))}{\longrightarrow} U(1) \to 0 \,. \end{displaymath} This is the source of the ubiquity of the expression $\exp(\tfrac{i}{\hbar} (-))$ in [[quantum physics]], say in the [[path integral]], where the exponentiated [[action functional]] appears as $\exp(\tfrac{i}{\hbar} S)$. \hypertarget{Prequantization}{}\subsubsection*{{Pre-Quantization and Differential cohomology}}\label{Prequantization} By the above discussion, for the exponentiated kinetic action functional to be well defined, one only needs that the equation $g_{i j} + g_{j k} = g_{i k}$ on triple intersection holds modulo addition of an integral multiple of [[Planck's constant]] $h = 2\pi \hbar$. If this is the case, then one says that the data $(\{\theta_i\}, \{g_{i j}\})$ defines equivalently \begin{itemize}% \item a $U(1)$-[[principal connection]]; \item a degree-2 cocycle in [[ordinary differential cohomology]] \end{itemize} on $X$, with \emph{[[curvature]]} the given symplectic 2-form $\omega$. Such data is called a \emph{[[pre-quantization]]} of the symplectic manifold $(X,\omega)$. Since it is the exponentiated action functional $\exp(\frac{i}{\hbar} S)$ that enters the quantization of the given mechanical system (for instance as the integrand of a [[path integral]]), the [[prequantization]] of a symplectic manifold is indeed precisely the data necessary before quantization. Therefore, in the spirit of the above discussion of pre-symplectic structures, we would like to refine the smooth moduli space of closed differential 2-forms to a moduli space of prequantized differential 2-forms. Again this does naturally exist if only we allow for a good notion of ``space''. An additional phenomenon to be taken care of now is that while pre-symplectic forms are either equal or not, their pre-quantizations can be different and yet be \emph{[[equivalence|equivalent]]}: because there is still a remaining freedom to change this data without changing the exponentiated action along a \emph{closed} path: we say that a choice of functions $h_i \in C^\infty(U_i, \mathbb{R}/(2\pi\hbar)\mathbb{Z})$ defines an equivalence between $(\{\theta_i\}, \{g_{i j}\})$ and $(\{\tilde \theta_i\}, \{\tilde g_{i j}\})$ if $\tilde \theta_i - \theta_i = \mathbf{d}h_i$ and $\tilde g_{i j} - g_{i j} = h_j - h_i$. This means that the space of prequantizations of $(X,\omega)$ is similar to an \emph{[[orbifold]]}: it has points which are connected by gauge equivalences: there is a \emph{[[groupoid]]} of pre-quantum structures on a manifold $X$. In just the same way then that above we found a [[smooth set|smooth]] [[moduli space]] $\mathbf{\Omega}^2_{cl}$ of closed differential 2-forms, one can find a [[smooth groupoid]] (for more on this see at \emph{[[geometry of physics]]} the section \emph{\href{geometry%20of%20physics#SmoothnGroupoids}{Smooth homotopy types}} ), which we denote \begin{displaymath} \mathbf{B}U(1)_{\mathrm{conn}} \in \mathbf{H} \end{displaymath} \begin{prop} \label{PrequantumGaugeTransformation}\hypertarget{PrequantumGaugeTransformation}{} The [[smooth groupoid]] $\mathbf{B}U(1)_{\mathrm{conn}}$ is \emph{characterized} as follows, \begin{enumerate}% \item For $X$ a [[smooth manifold]], maps \begin{displaymath} \nabla \colon X \longrightarrow \mathbf{B}U(1)_{conn} \end{displaymath} are equivalent to the above prequantum data $(\{\theta_i\}, \{g_{i j}\})$ on $X$; \item for $\nabla_1, \nabla_2 \colon X \longrightarrow \mathbf{B}U(1)_{conn}$ two such maps, [[homotopies]] \begin{displaymath} \itexarray{ & \nearrow \searrow^{\mathrlap{\nabla_1}} \\ X & \Downarrow & \mathbf{B}U(1)_{conn} \\ & \searrow \nearrow_{\mathrlap{\nabla_2}} } \end{displaymath} between these are equivalent to the above [[gauge transformations]] $(\{h_i\})$ between this data \end{enumerate} \begin{displaymath} (\theta_2)_i - (\theta_1)_i = \mathbf{d} \tfrac{\hbar}{i} log (h_i) \,. \end{displaymath} \end{prop} \begin{prop} \label{UniverselCurvatureMap}\hypertarget{UniverselCurvatureMap}{} There is a universal [[curvature]] map, a morphism of [[smooth groupoids]] \begin{displaymath} F \;\colon\; \mathbf{B}U(1)_{\mathrm{conn}} \longrightarrow \mathbf{\Omega}^2_{\mathrm{cl}} \end{displaymath} which is such that for $\nabla \colon X \longrightarrow \mathbf{B}U(1)_{conn}$ a $U(1)$-[[principal connection]], the composite \begin{displaymath} F_\nabla \;\colon\; X \stackrel{\nabla}{\longrightarrow} \mathbf{B}U(1)_{conn} \stackrel{F_{(-)}}{\longrightarrow} \mathbf{\Omega}^2_{cl} \end{displaymath} is its [[curvature]] 2-form. \end{prop} Hence this is the map that sends $(\{\theta_i\}, \{g_{i j}\})$ to $\omega$ with $\omega|_{U_i} = \mathbf{d}\theta_i$. Therefore: \begin{defn} \label{Prequantization}\hypertarget{Prequantization}{} A \emph{[[prequantization]]} of a [[symplectic manifold]] $(X,\omega)$ is -- if it exists -- a choice of [[circle group]]-[[principal connection]] $\nabla$ on $X$ whose [[curvature]] 2-form is the given [[symplectic form]] \begin{displaymath} F_\nabla = \omega \,. \end{displaymath} \end{defn} In terms of the classifying morphism of differential forms as in prop. \ref{PresymplecticFormsAsMapsIntoASmoothSpace} this reads as follows. \begin{prop} \label{PrequantizationByLiftingClassifyingMap}\hypertarget{PrequantizationByLiftingClassifyingMap}{} Given a [[presymplectic manifold]] $(X,\omega)$, regarded equivalently as an object $(X \stackrel{\omega}{\longrightarrow} \mathbf{\Omega}^2_{cl}) \in \mathbf{H}_{/\mathbf{\Omega}^2_{cl}}$ by prop. \ref{SymplecticManifoldsAsObjectsInSliceOverModuliOf2Forms}, then a \textbf{[[prequantization]]} of $(X,\omega)$, def. \ref{Prequantization}, is equivalently a choice of lift $\nabla$ in \begin{displaymath} \itexarray{ X &\stackrel{\nabla}{\longrightarrow}& \mathbf{B}U(1)_{conn} \\ & {}_{\mathllap{\omega}}\searrow & \downarrow^{\mathrlap{F_{(-)}}} \\ && \mathbf{\Omega}^2_{cl} } \,. \end{displaymath} \end{prop} Phrased this way, there is an evident concept of prequantization of Lagrangian correspondences: \begin{defn} \label{PrequantizedLagrangianCorrespondence}\hypertarget{PrequantizedLagrangianCorrespondence}{} Given prequantized symplectic manifolds $(X_i,\nabla_i)$ as in prop. \ref{PrequantizationByLiftingClassifyingMap}, and given a Lagrangian correspondence as in prop. \ref{IsotropicCorrespondenceDiagrammatically}, then a prequantization of this correspondence is a lift of the whole diagram through the universal curvature map of prop. \ref{UniverselCurvatureMap}: \begin{displaymath} \itexarray{ && Z \\ & \swarrow && \searrow \\ X_1 && && X_2 \\ & {}_{\mathllap{\omega_1}}\searrow && \swarrow_{\mathrlap{\omega_2}} \\ && \mathbf{\Omega}^2_{cl} } \;\;\;\; \mapsto \;\;\;\; \itexarray{ && Z \\ & \swarrow && \searrow \\ X_1 && \swArrow_{\simeq} && X_2 \\ & {}_{\mathllap{\nabla_1}}\searrow && \swarrow_{\mathrlap{\nabla_2}} \\ && \mathbf{B}U(1)_{conn} \\ && \downarrow^{\mathrlap{F}} \\ && \mathbf{\Omega}^2_{cl} } \,. \end{displaymath} \end{defn} \begin{remark} \label{}\hypertarget{}{} This means in words that a prequantized Lagrangian correspondence is a [[prequantization]] of the in- and out-going [[symplectic manifolds]] together with a choice of [[equivalence]]/[[gauge transformation]] between the two [[prequantum circle bundles]] pulled back to the [[correspondences]] space. \end{remark} \begin{remark} \label{}\hypertarget{}{} By [[duality]] in the [[symmetric monoidal (infinity,1)-category|smmetric monoidal]] [[(infinity,n)-category of correspondences|(2,1)-category of correspondences]], a prequantized Lagragian correspondence is equivalently a [[diagram]] of the form \begin{displaymath} \itexarray{ && Y \\ & \swarrow && \searrow \\ \ast && \swArrow && X_1 \times X_2 \\ & \searrow && \swarrow_{\mathrlap{\nabla_2- \nabla}} \\ \\ && \mathbf{B}U(1)_{conn} } \end{displaymath} hence a trivialization of the product of one prequantum bundle with the negative (the inverse under tensor product) of the other, on the correspondence space. \end{remark} \hypertarget{HamiltonianTrajectoriesAndPrequantizedLagrangianCorrespondences}{}\subsubsection*{{Hamiltonian flows, the Legendre transform and the Hamilton-Jacobi action}}\label{HamiltonianTrajectoriesAndPrequantizedLagrangianCorrespondences} \begin{prop} \label{HamiltonianTransformationIsPrequantizedByTheExponentiatedAction}\hypertarget{HamiltonianTransformationIsPrequantizedByTheExponentiatedAction}{} Consider the [[phase space]] $(\mathbb{R}^2, \; \omega = \mathbf{d} q \wedge \mathbf{d} p)$ of example \ref{CanonicalR2PhaseSpace} equipped with its canonical [[prequantization]] by $\theta = p \, \mathbf{d}q$ from example \ref{StandardPrequantizationOfStandardR2PhaseSpace}, Then smooth 1-parameter flows of this data via prequantized correspondences, def. \ref{PrequantizedLagrangianCorrespondence}, \begin{displaymath} t \;\;\;\; \mapsto \;\;\;\; \itexarray{ X && \stackrel{f_t}{\longrightarrow} && X \\ & {}_{\mathllap{\theta}} \searrow & \swArrow_{ F_t } & \swarrow_{\mathrlap{\theta}} \\ && \mathbf{B}U(1)_{conn} } \end{displaymath} are in bijection with smooth functions $H \colon \mathbb{R}^2 \longrightarrow \mathbb{R}$. This bijection works by regarding $H$ as a [[Hamiltonian]], def. \ref{HamiltonianCorrespondence}, and assigning the [[flow]] $f_t = \exp(t \{H,-\})$ of its [[Hamiltonian vector field]] \begin{displaymath} t \;\; \mapsto \;\; \itexarray{ X && \stackrel{\exp(t \{H,-\})}{\longrightarrow} && X \\ & {}_{\mathllap{\theta}} \searrow & \swArrow_{\exp( \tfrac{i}{\hbar} S_t )} & \swarrow_{\mathrlap{\theta}} \\ && \mathbf{B}U(1)_{conn} } \,, \end{displaymath} where the prequantization is given by \begin{itemize}% \item $S_t \;\colon\; \mathbb{R}^2 \longrightarrow \mathbb{R}$ is the [[Hamilton-Jacobi action]] of the classical [[trajectories]] induced by $H$, \item which is the [[integral]] $S_t = \int_{0}^t L \, d t$ of the [[Lagrangian]] $L \,d t$ induced by $H$, \item which is the [[Legendre transform]] of the [[Hamiltonian]] \begin{displaymath} L \coloneqq p \frac{\partial H}{\partial p} - H \;\colon\; \mathbb{R}^2 \longrightarrow \mathbb{R} \,. \end{displaymath} \end{itemize} \end{prop} \begin{proof} By prop. \ref{PrequantumGaugeTransformation} the prequantum filler of the diagram is given by a function $F_t =\exp(\tfrac{i}{\hbar} S_t)$ satisfying \begin{displaymath} f_t^\ast \theta - \theta = -\mathbf{d}S_t \,. \end{displaymath} By standard [[Lie theory]] a smooth such 1-parameter flow is fixed by its [[derivative]] by $t$. For the above equation this yields \begin{displaymath} \mathcal{L}_v \theta = -\mathbf{d}L \end{displaymath} where \begin{enumerate}% \item $v \in \Gamma(T X)$ is the [[vector field]] of the [[flow]] $t\mapsto f_t$; \item $\mathcal{L}_v$ is the [[Lie derivative]] along $v$; \item $L \coloneqq \frac{\partial S}{\partial t}$. \end{enumerate} By [[Cartan's magic formula]] this equation is equivalent to \begin{displaymath} \iota_v \omega = -\mathbf{d}L - \mathbf{d} \iota_v \theta \,. \end{displaymath} This is the symplectic form of [[Hamilton's equations]] for $v$ and says that \begin{displaymath} H \coloneqq - L - \iota_v \theta \end{displaymath} is a [[Hamiltonian]] that makes $v$ a [[Hamiltonian vector field]]. The correction term is \begin{displaymath} \begin{aligned} \iota_v \theta &= \iota_v ( p \, \mathbf{d}q ) \\ & = p \partial_v q \\ \end{aligned} \,. \end{displaymath} But since $v$ is Hamiltonian, this is given by one component of [[Hamilton's equations]] $\iota_v (\mathbf{d}p \wedge \mathbf{d}q) = \mathbf{d}H$ saying that $\partial_v q = \frac{\partial H}{\partial p}$. Hence in summary the flow is Hamiltonian and the pre-quntum filler is the choice of Hamiltonian $H$ specified by \begin{displaymath} \frac{\partial S}{\partial t} = L = p \frac{\partial H}{\partial p} - H \,. \end{displaymath} \end{proof} \begin{remark} \label{}\hypertarget{}{} In particular, this induces a [[functor]] \begin{displaymath} \exp(\tfrac{i}{\hbar} S) \;\colon\; Bord_1^{Riem} \longrightarrow Corr_1(\mathbf{H}_{/\mathbf{B}U(1)_{conn}}) \,. \end{displaymath} In summary, prop. \ref{HamiltonianTransformationIsPrequantizedByTheExponentiatedAction} and remark \ref{HamiltonianCorrespondencesAreSpacesOfTrajectories} say that a prequantized Lagrangian correspondence is conceptually of the following form \begin{displaymath} \itexarray{ && {{space\,of} \atop {trajectories}} \\ & {}^{\mathllap{{initial}\atop {values}}}\swarrow && \searrow^{\mathrlap{{Hamiltonian} \atop {evolution}}} \\ phase\,space_{in} && \swArrow_{{action} \atop {functional}} && phase \,space_{out} \\ & {}_{\mathllap{{prequantum}\atop {bundle}_{in}}}\searrow && \swarrow_{\mathrlap{{prequantum} \atop {bundle}_{out}}} \\ && {{2-group} \atop {of\,phases}} } \,. \end{displaymath} \end{remark} \begin{remark} \label{}\hypertarget{}{} The proof of prop. \ref{HamiltonianTransformationIsPrequantizedByTheExponentiatedAction} recovers, from general abstract input, precisely all the ingredients known in physics as \emph{[[canonical transformations]]}. The proposition says that the slice topos $\mathbf{H}_{/\mathbf{B}U(1)_{conn}}$ unifies [[classical mechanics]] in its two incarnations as [[Hamiltonian mechanics]] and as [[Lagrangian mechanics]], where the relation between the two via the [[Legendre transform]] is exhibited by the [[homotopies]] that fill diagrams in the slice topos over $\mathbf{B}U(1)_{conn}$. [[!include Hamiltonian and Lagrangian -- table]] \end{remark} \hypertarget{heisenberg_group_and_poisson_bracket}{}\subsubsection*{{Heisenberg group and Poisson bracket}}\label{heisenberg_group_and_poisson_bracket} Above we have interpreted [[maps]] $f \colon X \to Y$ as [[correspondences]] between $X$ and $Y$ by taking the [[correspondence space]] to be the [[graph of a function|graph]] of $f$. There is also another natural way to regard maps as correspondences: we may simply take $X$ as the correspondence space, take the left map out of it to be the identity and the right map to be $f$ itself: \begin{displaymath} \left( X \stackrel{f}{\longrightarrow} Y \right) \;\; \mapsto \;\; \left( \itexarray{ && X \\ & {}^{\mathllap{id}}\swarrow && \searrow^{\mathrlap{f}} \\ X && && Y } \right) \,. \end{displaymath} Consider now those correspondences which are [[equivalences]] ([[isomorphisms]]) in the [[category of correspondences]] $Corr_1(\mathbf{H})$. If we forget the [[smooth structure]] on everything and consider just correspondences of the underlying [[sets]], hence $Corr_1(Set)$, then it is easy to see that under the [[cardinality]] map correspondences are given by [[matrices]] with [[cardinality]] entries and [[composition]] of correspondence by [[fiber product]] induces [[matrix multiplication]]. Therefore for a correspondence to be an equivalence-transformation it has to be of the form above, induced by a direct [[map]], which in addition is an [[equivalence]] $f \colon X \stackrel{\simeq}{\longrightarrow} Y$. \begin{prop} \label{}\hypertarget{}{} Let $(X,\omega)$ be a [[symplectic manifold]] and choose any [[prequantization]] $(L,\nabla)$, thought of, via remark \ref{PrequantizationIsLiftThroughCurvatureBaseChange}, as an object in the [[slice (infinity,1)-topos|slice (2,1)-topos]], $\nabla \in \mathbf{H}_{/\mathbf{B}U(1)_{conn}}$. Then \begin{itemize}% \item the [[automorphism group]] of $\nabla$ in the [[category of correspondences]] $Corr_1(\mathbf{H}_{/\mathbf{B}U(1)_{conn}})$ is what is called the \emph{[[quantomorphism group]]}; \item its [[Lie algebra]] is the [[Poisson bracket]] Lie algebra of $(X,\omega)$. \end{itemize} \end{prop} See (\hyperlink{FiorenzaRogersSchreiber13a}{hgp 13}) For some reason, the [[quantomorphism group]] which is the [[Lie integration]] of the [[Poisson bracket]] is less famous than the [[Heisenberg group]] that sits inside it: \begin{remark} \label{}\hypertarget{}{} Suppose that $(X,\omega)$ itself has the structure of a [[group]] (for instance if $(X,\omega)$ is a [[symplectic vector space]] such as $(\mathbb{R}^{2n}, \sum_i p_i \mathbf{d}q^i)$ ), then the [[subgroup]] of the [[quantomorphism group]] whose underlying [[diffeomorphisms]] are given by the action of $X$ is the \emph{[[Heisenberg group]]} of $X$. \end{remark} \hypertarget{hamiltonian_actions_and_moment_maps}{}\subsubsection*{{Hamiltonian actions and moment maps}}\label{hamiltonian_actions_and_moment_maps} For $G$ a [[Lie group]], a [[Hamiltonian action]] of $G$ on $(X,\omega)$ is equivalently an action by prequantized Lagrangian correspondences, hence a group [[homomorphism]] \begin{displaymath} G \longrightarrow \mathbf{Aut}_\nabla(Corr_1(\mathbf{H}_{/\mathbf{B}U(1)_{conn}})) \,. \end{displaymath} The [[Lie differentiation]] of this is the corresponding [[moment map]]. See (\hyperlink{FiorenzaRogersSchreiber13a}{hgp 13}) \hypertarget{SemanticsLayer}{}\subsection*{{Semantic Layer}}\label{SemanticsLayer} We now discuss the above constructions more abstractly in [[cohesive topos|cohesive]] [[topos theory]]. \begin{quote}% under construction \end{quote} given $V$ then the [[delooping]] $\mathbf{B} \mathbf{Aut}(V)$ of its [[automorphism group]] $\mathbf{Aut}(V)$ is the [[1-image]] factorization of the name $\ast \stackrel{\vdash V}{\longrightarrow} Type$ of $V$ \begin{displaymath} \ast \stackrel{}{\longrightarrow} \mathbf{B}\mathbf{Aut}(V) \hookrightarrow Type \,. \end{displaymath} for the slice over $\mathbf{B}U(1)_{conn}$ this needs to be subjected to [[differential concretification]] (\ldots{}) \hypertarget{SyntacticLayer}{}\subsection*{{Syntactic Layer}}\label{SyntacticLayer} We now discuss the above constructions yet more abstractly in [[homotopy type theory]]. (\ldots{}) prequantization is lift through [[dependent sum]] along the universal [[curvature]] map of prop. \ref{UniverselCurvatureMap} \begin{displaymath} \underset{F_{(-)}}{\sum} \;\colon\; \mathbf{H}_{/\mathbf{B}U(1)_{conn}} \longrightarrow \mathbf{H}_{/\mathbf{\Omega}^2_{cl}} \end{displaymath} (\ldots{}) \hypertarget{references}{}\subsection*{{References}}\label{references} As far as it is not covered by traditional material, the above discussion is taken from \begin{itemize}% \item [[Domenico Fiorenza]], [[Chris Rogers]], [[Urs Schreiber]], \emph{[[schreiber:Higher geometric prequantum theory]]} \item [[Urs Schreiber]], \emph{[[schreiber:Classical field theory via Cohesive homotopy types]]} \end{itemize} For more and related references see there and see at \emph{[[motivic quantization]]}. [[!redirects prequantized Lagrangian correspondences]] [[!redirects prequantum Lagrangian correspondence]] [[!redirects prequantum Lagrangian correspondences]] \end{document}