# Is it possible to “lower” a $\pi_1$-invariant differential function defined over the universal covering manifold to the base one?

Consider a differentiable manifold $M$ and its smooth universal covering $\pi:\tilde{M}\rightarrow M$. There is a canonical action of the fundamental group $\pi_1(M)$ on the covering manifold $\tilde{M}$ denoted by $x\mapsto g\cdot x$ for $g\in\pi_1(M)$. Suppose to have a differentiable function $f:M\rightarrow \mathbb{R}$. The function $\tilde{f}:\tilde{M}\rightarrow \mathbb{R}$ given by $\tilde{f}:=f\circ\pi$ is differentiable and satisfies $\tilde{f}(g\cdot x)=\tilde{f}(x)$ for every $g\in\pi_1(M)$. On the other hand suppose to have a differentiable function $\tilde{f}:\tilde{M}\rightarrow \mathbb{R}$ such that $\tilde{f}(g\cdot x)=\tilde{f}(x)$ for every $g\in\pi_1(M)$. There does exist a $\textit{differentiable}$ function $f:M\rightarrow\mathbb{R}$ such that $\tilde{f}:=f\circ\pi$? This is probably a trivial question. It seems right to me but I'm not sure. Thank you.

For manifolds, the group of deck transformations operates transitively on the fibres of $\pi$, and the canonical action of $\pi_1(M)$ on $\tilde{M}$ gives an isomorphism to the deck transformation group. Thus $\tilde{f}$ being $\pi_1(M)$-invariant means nothing else than $\tilde{f}$ is constant on the fibres of $\pi$.
Hence there is a unique mapping $f\colon M\to\mathbb{R}$ with $\tilde{f} = f\circ \pi$. Since $\pi$ is a local diffeomorphism, for every $x \in M$ and $y\in \pi^{-1}(x)$ we find open neighbourhoods $U$ of $x$ and $V$ of $y$ such that $\pi\lvert_V\colon V\to U$ is a diffeomorphism. Writing $f\lvert_U = \tilde{f}\circ \bigl(\pi\lvert_V\bigr)^{-1}$ then shows that $f$ is smooth.