I am trying to prove that a simple diagram commutes. Namely, if $f:(M,g)\rightarrow (N,g')$ is an isometry of Riemannian manifolds, I want to show that $Tf\circ \sharp = \sharp \circ (T^*f)^{-1}$.
(Where $\sharp:T^*M\rightarrow TM$ is the sharp map ).
My attempt at a proof so far is this:
Pick $q\in M$, and compute for $v\in T_{f(q)}N$: $(T^*f)^{-1}\circ \flat \circ (Tf)^{-1}(v) = (T^*f)^{-1}\circ g_q((Tf)^{-1}(v), \bullet )= g_q((Tf)^{-1}(v), (Tf)^{-1}(\bullet)) = (f^{-1})^*g_{f(q)}'(v,\bullet) = g_{f(q)}'(v,\bullet) = \flat(v)$
Is this even true, does this proof work, and is there a nicer one? (I feel like there should be). In particular, I feel like I might be missing something in the definition of $(Tf)^*$ that could make this very easy without having a bunch of inverses everywhere.
I guess this works and is a little nicer:
Prove that $(Tf)^*\circ \flat \circ (Tf) = \flat$ by taking $v\in T_qM$ and then $[(Tf)_q(v)]^\flat = g_{f(q)}'((Tf_q(v), \bullet)$. So composing with $(Tf)^*_{f(q)}$, we get $g'_{f(q)}((Tf)_q(v), (Tf)_q(\bullet))$, which equals $g_q(v,\bullet) = v^\flat$.
Then since everything in sight is a linear isomorphism you can reverse whichever arrows you want.