Orthogonal splitting of a vector subbundle (source code)

= Orthogonal splitting of a vector subbundle
{title2=$E\cong F\oplus(E/F)$}

A <fiber metric> on a smooth <vector bundle> $E$ gives a smooth <orthogonal projection> $P:E\to F$ onto any <vector subbundle>. In a <local frame> of $E$, let $G$ be the metric <matrix> and $A$ the columns of a frame of $F$. Then $P=A(A^tGA)^{-1}A^tG$, proving smoothness. The complementary subbundle $F^\perp=\ker P$ maps isomorphically onto the <quotient vector bundle>. Explicitly $v\mapsto(Pv,[v])$ is a <vector bundle isomorphism> $E\to F\oplus(E/F)$, with inverse $(f,[v])\mapsto f+(I-P)v$. This inverse is independent of the representative $v$, but the splitting depends on the chosen metric.