## Formalized Name Universal Cover Flux Homomorphism ## Formalized Statement Let $(M,\omega)$ be a closed smooth symplectic manifold, and let $\operatorname{Symp}_0(M,\omega)$ denote the identity component of the group of symplectomorphisms of $(M,\omega)$. Let $\operatorname{Ham}(M,\omega)\subseteq\operatorname{Symp}_0(M,\omega)$ denote the subgroup of time-one maps of smooth Hamiltonian isotopies. Here a Hamiltonian isotopy is a smooth symplectic path generated by a time-dependent vector field $X_t\in\mathfrak X(M)$ for which there is a smooth function $H:[0,1]\times M\to\mathbb R$ such that, with $H_t(x)=H(t,x)$, \begin{align*} \iota_{X_t}\omega=dH_t\quad\text{for every }t\in[0,1]. \end{align*} Let $\widetilde{\operatorname{Symp}}_0(M,\omega)$ be the universal cover represented by fixed-endpoint homotopy classes of smooth symplectic paths $\varphi:[0,1]\to\operatorname{Symp}_0(M,\omega)$ with $\varphi_0=\operatorname{id}_M$, with group operation represented by pointwise composition of paths. Let $\widetilde{\operatorname{Ham}}(M,\omega)$ denote the universal cover of $\operatorname{Ham}(M,\omega)$, mapped into $\widetilde{\operatorname{Symp}}_0(M,\omega)$ by inclusion. For such a symplectic path $\varphi$, define its generating vector field $X_t\in\mathfrak X(M)$ by \begin{align*} \frac{d}{dt}\varphi_t=X_t\circ\varphi_t. \end{align*} Define the flux class by \begin{align*} \operatorname{Flux}(\varphi)=\left[\int_0^1\iota_{X_t}\omega\,d\mathcal L^1(t)\right]\in H^1(M;\mathbb R), \end{align*} where the bracket denotes the de Rham cohomology class of the resulting closed $1$-form. Then this assignment descends to a well-defined group homomorphism \begin{align*} \operatorname{Flux}:\widetilde{\operatorname{Symp}}_0(M,\omega)\to H^1(M;\mathbb R). \end{align*} Assume the Banyaga flux exactness theorem for closed symplectic manifolds in the following form: \begin{align*} \operatorname{Flux}([\varphi])=0\quad\Longleftrightarrow\quad[\varphi]\text{ is represented by a Hamiltonian isotopy}. \end{align*} Then \begin{align*} \ker(\operatorname{Flux})=\operatorname{im}\!\left(\widetilde{\operatorname{Ham}}(M,\omega)\to\widetilde{\operatorname{Symp}}_0(M,\omega)\right), \end{align*} equivalently the kernel is the set of fixed-endpoint homotopy classes represented by Hamiltonian isotopies. ## Proof [proofplan] We first prove that the $1$-form integrated in the definition of flux is closed for every symplectic path. We then prove fixed-endpoint homotopy invariance by differentiating a two-parameter family of symplectic paths; the key identity is the Eulerian variation formula $\partial_sA_{s,t}-\partial_tB_{s,t}=[A_{s,t},B_{s,t}]$, whose contraction with $\omega$ changes the flux representative by an exact form. After that, we compute the flux of a pointwise product path and use the fact that diffeomorphisms isotopic to the identity act as the identity on de Rham cohomology. Finally, the kernel statement follows from the assumed Banyaga flux exactness theorem, together with the direct observation that Hamiltonian isotopies have exact flux representatives. [/proofplan] [step:Show that the flux form of a symplectic path is closed] Let $\varphi:[0,1]\to\operatorname{Symp}_0(M,\omega)$ be a smooth path with $\varphi_0=\operatorname{id}_M$, and let $X_t\in\mathfrak X(M)$ be its generating vector field, so that \begin{align*} \frac{d}{dt}\varphi_t=X_t\circ\varphi_t. \end{align*} For each $t\in[0,1]$, define $\alpha_t\in\Omega^1(M)$ by \begin{align*} \alpha_t=\iota_{X_t}\omega. \end{align*} Since $\varphi_t$ is symplectic, $\varphi_t^*\omega=\omega$. Differentiating this identity with respect to $t$ gives \begin{align*} 0=\frac{d}{dt}\varphi_t^*\omega=\varphi_t^*(\mathcal L_{X_t}\omega). \end{align*} Pullback by the diffeomorphism $\varphi_t$ is injective on differential forms, hence $\mathcal L_{X_t}\omega=0$. Cartan's formula and $d\omega=0$ give \begin{align*} 0=\mathcal L_{X_t}\omega=d(\iota_{X_t}\omega)+\iota_{X_t}(d\omega)=d\alpha_t. \end{align*} Thus $\alpha_t$ is closed for every $t\in[0,1]$. Define $\alpha\in\Omega^1(M)$ by \begin{align*} \alpha_x(v)=\int_0^1(\alpha_t)_x(v)\,d\mathcal L^1(t) \end{align*} for every $x\in M$ and $v\in T_xM$. Since $[0,1]$ is compact and $(t,x)\mapsto\alpha_t$ is smooth, exterior differentiation commutes with this parameter integral. Therefore \begin{align*} d\alpha=\int_0^1d\alpha_t\,d\mathcal L^1(t)=0. \end{align*} Hence $\operatorname{Flux}(\varphi)=[\alpha]\in H^1(M;\mathbb R)$ is defined. [/step] [step:Prove fixed-endpoint homotopy invariance] Let $\Phi:[0,1]\times[0,1]\times M\to M$ be a smooth fixed-endpoint homotopy through symplectic paths. Thus, for each $s\in[0,1]$, the path $\Phi_s:[0,1]\to\operatorname{Symp}_0(M,\omega)$ defined by $\Phi_s(t)=\Phi(s,t,\cdot)$ satisfies $\Phi_s(0)=\operatorname{id}_M$, and $\Phi_s(1)$ is independent of $s$. For each $(s,t)\in[0,1]\times[0,1]$, define $A_{s,t},B_{s,t}\in\mathfrak X(M)$ by \begin{align*} \frac{\partial}{\partial t}\Phi(s,t,\cdot)=A_{s,t}\circ\Phi(s,t,\cdot) \end{align*} and \begin{align*} \frac{\partial}{\partial s}\Phi(s,t,\cdot)=B_{s,t}\circ\Phi(s,t,\cdot). \end{align*} Define $\alpha_{s,t},\beta_{s,t}\in\Omega^1(M)$ by \begin{align*} \alpha_{s,t}=\iota_{A_{s,t}}\omega \end{align*} and \begin{align*} \beta_{s,t}=\iota_{B_{s,t}}\omega. \end{align*} The argument of the previous step applied to the $t$-curves and $s$-curves of $\Phi$ shows that $d\alpha_{s,t}=0$, $d\beta_{s,t}=0$, $\mathcal L_{A_{s,t}}\omega=0$, and $\mathcal L_{B_{s,t}}\omega=0$. Equality of mixed partial derivatives of $\Phi$ gives the Eulerian variation identity \begin{align*} \frac{\partial A_{s,t}}{\partial s}-\frac{\partial B_{s,t}}{\partial t}=[A_{s,t},B_{s,t}]. \end{align*} Indeed, this is the standard Maurer-Cartan identity for the right logarithmic derivatives $A_{s,t}=\partial_t\Phi(s,t,\cdot)\circ\Phi(s,t,\cdot)^{-1}$ and $B_{s,t}=\partial_s\Phi(s,t,\cdot)\circ\Phi(s,t,\cdot)^{-1}$. Contracting with $\omega$ yields \begin{align*} \frac{\partial\alpha_{s,t}}{\partial s}-\frac{\partial\beta_{s,t}}{\partial t}=\iota_{[A_{s,t},B_{s,t}]}\omega. \end{align*} Using the identity $\iota_{[A,B]}\omega=\mathcal L_A(\iota_B\omega)-\iota_B(\mathcal L_A\omega)$ with $A=A_{s,t}$ and $B=B_{s,t}$, and using $\mathcal L_{A_{s,t}}\omega=0$ and $d\beta_{s,t}=0$, Cartan's formula gives \begin{align*} \iota_{[A_{s,t},B_{s,t}]}\omega=d(\iota_{A_{s,t}}\iota_{B_{s,t}}\omega). \end{align*} Since $\iota_{A_{s,t}}\iota_{B_{s,t}}\omega=\omega(B_{s,t},A_{s,t})=-\omega(A_{s,t},B_{s,t})$, we have \begin{align*} \frac{\partial\alpha_{s,t}}{\partial s}=\frac{\partial\beta_{s,t}}{\partial t}-d(\omega(A_{s,t},B_{s,t})). \end{align*} For each $s\in[0,1]$, define $\alpha_s\in\Omega^1(M)$ by \begin{align*} (\alpha_s)_x(v)=\int_0^1(\alpha_{s,t})_x(v)\,d\mathcal L^1(t) \end{align*} for every $x\in M$ and $v\in T_xM$. Differentiating under the integral sign gives \begin{align*} \frac{d\alpha_s}{ds}=\beta_{s,1}-\beta_{s,0}-d\left(\int_0^1\omega(A_{s,t},B_{s,t})\,d\mathcal L^1(t)\right). \end{align*} Because the homotopy has fixed endpoints, $B_{s,0}=0$ and $B_{s,1}=0$. Therefore \begin{align*} \frac{d\alpha_s}{ds}=-d\left(\int_0^1\omega(A_{s,t},B_{s,t})\,d\mathcal L^1(t)\right). \end{align*} The derivative of $\alpha_s$ is exact, so the cohomology class $[\alpha_s]\in H^1(M;\mathbb R)$ is independent of $s$. Taking $s=0$ and $s=1$ proves that fixed-endpoint homotopic symplectic paths have the same flux class. [guided] Let $\Phi:[0,1]\times[0,1]\times M\to M$ be a smooth fixed-endpoint homotopy through symplectic paths. For each $s\in[0,1]$, define $\Phi_s:[0,1]\to\operatorname{Symp}_0(M,\omega)$ by $\Phi_s(t)=\Phi(s,t,\cdot)$. The assumptions are that $\Phi_s(0)=\operatorname{id}_M$ for every $s$, and that $\Phi_s(1)$ is independent of $s$. We want to prove that the flux class of $\Phi_s$ does not change with $s$. There are two velocities in a two-parameter family. For $(s,t)\in[0,1]\times[0,1]$, define $A_{s,t}\in\mathfrak X(M)$ by \begin{align*} \frac{\partial}{\partial t}\Phi(s,t,\cdot)=A_{s,t}\circ\Phi(s,t,\cdot) \end{align*} and define $B_{s,t}\in\mathfrak X(M)$ by \begin{align*} \frac{\partial}{\partial s}\Phi(s,t,\cdot)=B_{s,t}\circ\Phi(s,t,\cdot). \end{align*} The corresponding $1$-forms are \begin{align*} \alpha_{s,t}=\iota_{A_{s,t}}\omega \end{align*} and \begin{align*} \beta_{s,t}=\iota_{B_{s,t}}\omega. \end{align*} Since each $t$-curve and each $s$-curve lies in $\operatorname{Symp}_0(M,\omega)$, the same differentiation argument used for a single symplectic path gives $\mathcal L_{A_{s,t}}\omega=0$, $\mathcal L_{B_{s,t}}\omega=0$, $d\alpha_{s,t}=0$, and $d\beta_{s,t}=0$. The central point is to compute how $\alpha_{s,t}$ changes as $s$ changes. With the right logarithmic derivative convention \begin{align*} A_{s,t}=\partial_t\Phi(s,t,\cdot)\circ\Phi(s,t,\cdot)^{-1} \end{align*} and \begin{align*} B_{s,t}=\partial_s\Phi(s,t,\cdot)\circ\Phi(s,t,\cdot)^{-1}, \end{align*} equality of mixed partial derivatives gives the Eulerian Maurer-Cartan identity \begin{align*} \frac{\partial A_{s,t}}{\partial s}-\frac{\partial B_{s,t}}{\partial t}=[A_{s,t},B_{s,t}]. \end{align*} This is the place where the sign matters: the bracket is $[A_{s,t},B_{s,t}]$ for these conventions. Contracting this identity with $\omega$ gives \begin{align*} \frac{\partial\alpha_{s,t}}{\partial s}-\frac{\partial\beta_{s,t}}{\partial t}=\iota_{[A_{s,t},B_{s,t}]}\omega. \end{align*} We now rewrite the bracket term as an exact $1$-form. For vector fields $A,B\in\mathfrak X(M)$, the naturality of contraction and Lie derivative gives \begin{align*} \iota_{[A,B]}\omega=\mathcal L_A(\iota_B\omega)-\iota_B(\mathcal L_A\omega). \end{align*} Apply this with $A=A_{s,t}$ and $B=B_{s,t}$. Since $A_{s,t}$ is an infinitesimal symplectic vector field, $\mathcal L_{A_{s,t}}\omega=0$. Since $\beta_{s,t}=\iota_{B_{s,t}}\omega$ is closed, Cartan's formula gives \begin{align*} \mathcal L_{A_{s,t}}\beta_{s,t}=d(\iota_{A_{s,t}}\beta_{s,t})+\iota_{A_{s,t}}d\beta_{s,t}=d(\iota_{A_{s,t}}\iota_{B_{s,t}}\omega). \end{align*} Therefore \begin{align*} \iota_{[A_{s,t},B_{s,t}]}\omega=d(\iota_{A_{s,t}}\iota_{B_{s,t}}\omega). \end{align*} Because $\iota_{A_{s,t}}\iota_{B_{s,t}}\omega=\omega(B_{s,t},A_{s,t})=-\omega(A_{s,t},B_{s,t})$, this becomes \begin{align*} \frac{\partial\alpha_{s,t}}{\partial s}=\frac{\partial\beta_{s,t}}{\partial t}-d(\omega(A_{s,t},B_{s,t})). \end{align*} For each $s\in[0,1]$, define the flux representative $\alpha_s\in\Omega^1(M)$ by \begin{align*} (\alpha_s)_x(v)=\int_0^1(\alpha_{s,t})_x(v)\,d\mathcal L^1(t) \end{align*} for $x\in M$ and $v\in T_xM$. The smoothness of $\Phi$ permits differentiation under the parameter integral, and the preceding identity gives \begin{align*} \frac{d\alpha_s}{ds}=\int_0^1\frac{\partial\beta_{s,t}}{\partial t}\,d\mathcal L^1(t)-d\left(\int_0^1\omega(A_{s,t},B_{s,t})\,d\mathcal L^1(t)\right). \end{align*} The first integral is $\beta_{s,1}-\beta_{s,0}$. Because the endpoints of the homotopy are fixed, the $s$-velocity vanishes at $t=0$ and $t=1$, so $B_{s,0}=0$ and $B_{s,1}=0$. Hence $\beta_{s,0}=0$ and $\beta_{s,1}=0$, and therefore \begin{align*} \frac{d\alpha_s}{ds}=-d\left(\int_0^1\omega(A_{s,t},B_{s,t})\,d\mathcal L^1(t)\right). \end{align*} Thus $\frac{d\alpha_s}{ds}$ is exact. Passing to de Rham cohomology gives $\frac{d}{ds}[\alpha_s]=0$, so $[\alpha_s]$ is constant in $s$. Consequently the two endpoint paths of the homotopy have the same flux. [/guided] [/step] [step:Compute the flux of a pointwise product path] Let $\varphi:[0,1]\to\operatorname{Symp}_0(M,\omega)$ and $\psi:[0,1]\to\operatorname{Symp}_0(M,\omega)$ be smooth paths with $\varphi_0=\psi_0=\operatorname{id}_M$. Let $X_t,Y_t\in\mathfrak X(M)$ be defined by \begin{align*} \frac{d}{dt}\varphi_t=X_t\circ\varphi_t \end{align*} and \begin{align*} \frac{d}{dt}\psi_t=Y_t\circ\psi_t. \end{align*} Define the product path $\eta:[0,1]\to\operatorname{Symp}_0(M,\omega)$ by \begin{align*} \eta_t=\varphi_t\circ\psi_t. \end{align*} Let $Z_t\in\mathfrak X(M)$ be the generating vector field of $\eta$. Differentiating $\eta_t=\varphi_t\circ\psi_t$ gives \begin{align*} Z_t=X_t+(\varphi_t)_*Y_t. \end{align*} Since $\varphi_t$ is symplectic, \begin{align*} \iota_{Z_t}\omega=\iota_{X_t}\omega+(\varphi_t^{-1})^*(\iota_{Y_t}\omega). \end{align*} For each fixed $t\in[0,1]$, the path $r\mapsto\varphi_{rt}^{-1}$ is a smooth isotopy from $\operatorname{id}_M$ to $\varphi_t^{-1}$. Hence $\varphi_t^{-1}$ is homotopic to $\operatorname{id}_M$, and homotopy invariance of de Rham cohomology implies that $(\varphi_t^{-1})^*$ acts as the identity on $H^1(M;\mathbb R)$. Therefore $(\varphi_t^{-1})^*(\iota_{Y_t}\omega)$ and $\iota_{Y_t}\omega$ determine the same cohomology class for each $t$. Let $q$ denote the quotient map from closed $1$-forms on $M$ to $H^1(M;\mathbb R)$. By linearity of $q$ and by integration of a smooth family of closed $1$-forms, \begin{align*} q\left(\int_0^1(\varphi_t^{-1})^*(\iota_{Y_t}\omega)\,d\mathcal L^1(t)\right)=\int_0^1q\left((\varphi_t^{-1})^*(\iota_{Y_t}\omega)\right)\,d\mathcal L^1(t). \end{align*} Since each $(\varphi_t^{-1})^*$ acts as the identity on cohomology, this equals \begin{align*} \int_0^1q(\iota_{Y_t}\omega)\,d\mathcal L^1(t)=q\left(\int_0^1\iota_{Y_t}\omega\,d\mathcal L^1(t)\right). \end{align*} Consequently \begin{align*} \operatorname{Flux}(\eta)=\operatorname{Flux}(\varphi)+\operatorname{Flux}(\psi). \end{align*} Thus flux is additive under pointwise composition of paths. [/step] [step:Descend the additive assignment to the universal cover] By fixed-endpoint homotopy invariance, $\operatorname{Flux}(\varphi)$ depends only on the class $[\varphi]\in\widetilde{\operatorname{Symp}}_0(M,\omega)$. Hence the formula \begin{align*} \operatorname{Flux}([\varphi])=\operatorname{Flux}(\varphi) \end{align*} defines a well-defined map \begin{align*} \operatorname{Flux}:\widetilde{\operatorname{Symp}}_0(M,\omega)\to H^1(M;\mathbb R). \end{align*} The computation for pointwise products gives, for all $[\varphi],[\psi]\in\widetilde{\operatorname{Symp}}_0(M,\omega)$, \begin{align*} \operatorname{Flux}([\varphi][\psi])=\operatorname{Flux}([\varphi])+\operatorname{Flux}([\psi]). \end{align*} Since $H^1(M;\mathbb R)$ is written additively, $\operatorname{Flux}$ is a group homomorphism. [/step] [step:Identify the kernel with the Hamiltonian universal cover] Let $[\varphi]\in\widetilde{\operatorname{Symp}}_0(M,\omega)$ be represented by a Hamiltonian isotopy. Thus its generating vector field $X_t\in\mathfrak X(M)$ satisfies \begin{align*} \iota_{X_t}\omega=dH_t \end{align*} for a smooth Hamiltonian $H:[0,1]\times M\to\mathbb R$, where $H_t:M\to\mathbb R$ is given by $H_t(x)=H(t,x)$. Since exterior differentiation commutes with smooth integration over the compact interval $[0,1]$, \begin{align*} \int_0^1\iota_{X_t}\omega\,d\mathcal L^1(t)=d\left(\int_0^1H_t\,d\mathcal L^1(t)\right). \end{align*} Thus every class represented by a Hamiltonian isotopy has zero flux, and the image of $\widetilde{\operatorname{Ham}}(M,\omega)$ in $\widetilde{\operatorname{Symp}}_0(M,\omega)$ is contained in $\ker(\operatorname{Flux})$. Conversely, let $[\varphi]\in\ker(\operatorname{Flux})$. We invoke the assumed Banyaga flux exactness theorem in the precise form stated in the theorem: for a closed symplectic manifold $(M,\omega)$, a class in $\widetilde{\operatorname{Symp}}_0(M,\omega)$ has zero universal-cover flux if and only if it is represented by a Hamiltonian isotopy. Its hypotheses are satisfied here because $M$ is closed by assumption, $[\varphi]$ is a fixed-endpoint homotopy class of smooth symplectic paths beginning at $\operatorname{id}_M$, and $[\varphi]\in\ker(\operatorname{Flux})$ means exactly that its universal-cover flux class is zero. Therefore $[\varphi]$ is represented by a Hamiltonian isotopy, so it lies in the image of the inclusion-induced map \begin{align*} \widetilde{\operatorname{Ham}}(M,\omega)\to\widetilde{\operatorname{Symp}}_0(M,\omega). \end{align*} This proves the reverse containment. Combining both containments gives \begin{align*} \ker(\operatorname{Flux})=\operatorname{im}\left(\widetilde{\operatorname{Ham}}(M,\omega)\to\widetilde{\operatorname{Symp}}_0(M,\omega)\right), \end{align*} equivalently the kernel is precisely the set of fixed-endpoint homotopy classes represented by Hamiltonian isotopies. [/step]