After all this time, I came up with a very nice tensor calculus proof of the Hairy Ball Theorem.
It only depends on Stokes theorem and standard laws of tensor calculus like the Ricci identity and symmetries of curvature tensors.
All the topology is done by Stokes theorem.
The remainder of the proof is equational, local and geometrical.
It is coordinate/basis independent (only abstract indexes are used) and proves the theorem for all orientable closed 2-manifolds with non-zero total curvature.
The basic logic of the proof is, given a vector field $x$ the closed orientable manifold $M$, define a 1-form $z$ such that $dz$ is independent of $x$ when $||x|| = 1$ everywhere.
By Stokes theorem, such an $x$ can only exist for a manifold with $\int_M dz = 0$.
For the 1-form defined in the proof $dz$ is the scalar curvature,
proving the theorem for all 2-manifolds with nonzero total curvature, which includes spheres.
The code for automating the equational part of the proof is at the end.
This was certainly a fun way to learn about tensor calculus, Mathematica & xAct all at the same time
and the folks on the xAct mailing list were very helpful, not to mention extremely patient.
Definitions
The hair field
$$ \begin{align}
||x||^2 &= x^i x_j = 1 \\
\end{align}$$
Auxiliary 1-forms
$$ \begin{align}
y_i &\triangleq \varepsilon_{ij} x^j \\
\end{align}$$
$$ \begin{align}
z_i &\triangleq y_j \nabla_i x^j\\
\end{align}$$
Properties
$y$ is unit norm
: $$\begin{align}
||y||^2 &=y_i y^i \\
&= \varepsilon_{ij} x^j \varepsilon^{ik} x_k \\
&= 2 g_{[i}{}^{i} g_{j]}{}^k x^j x_k \\
&= 2 g_{[i}{}^i x_{j]}x^j \\
&= g_i{}^i x_j x^j - g_j{}^i x_i x^j \\
&= 2 x_j x^j - x_j x^j \\
&= x_j x^j = 1
\end{align}$$
$x$ is orthogonal to its derivative
: $$x_i\nabla_jx^i= \frac{1}{2} \nabla_j x_i x^i= \frac{1}{2} \nabla_j 1=0$$
$y$ is orthogonal to $x$
: $$
y_i x^i = x^j\varepsilon_{ji} x^i = -x^j\varepsilon_{ij} x^i = -x^jy_j = -y_ix^i\\
\ \therefore\ y_i x^i = 0$$
Curvature in 2 dimensions
Riemann curvature of a 2-manifold
: $$ \begin{align}
R_{ij}{}^{kl} &= R_{[ij]}{}^{[kl]} \\
&= (\frac{1}{2} \varepsilon_{ij} \varepsilon^{mn}) (\frac{1}{2} \varepsilon^{kl} \varepsilon_{op}) R_{mn}{}^{op} \\
&= (\frac{1}{2} \varepsilon_{ij} \varepsilon^{kl}) (\frac{1}{2} \varepsilon^{mn} \varepsilon_{op}) R_{mn}{}^{op} \\
&= \frac{1}{2} \varepsilon_{ij} \varepsilon^{kl} R_{mn}{}^{[mn]} \\
&= \frac{1}{2} \varepsilon_{ij} \varepsilon^{kl} R_{mn}{}^{mn} \\
&= \frac{1}{2} \varepsilon_{ij} \varepsilon^{kl} R \\
&= g_{[i}{}^k g_{j]}{}^{l}R
\end{align}$$
Proof
1
: $$\begin{align}
\varepsilon_{jk} (\nabla_{[l} x^j) (\nabla_{m]} x^k)
&= y_l y^i \varepsilon_{jk} (\nabla_{[l} x^j) (\nabla_{m]} x^k) \\
&= y_l \varepsilon^{in} x_n \varepsilon_{jk} (\nabla_{[l} x^j) (\nabla_{m]} x^k) \\
&= 2 y_l x_n (\nabla_{[j} x^{[i}) (\nabla_{k]} x^{n]}) \\
&= 2 y_l 0_{[j}{}^{[i} (\nabla_{k]} x^{n]}) \\
&= 0 \end{align}$$
2
: $$\begin{align}
(\nabla_{[j} \nabla_{i]} x^k) y_k
&= R_{ji}{}^{k}{}_m x^m y_k / 2, & & \text{by the Ricci identity}\\
&= R \ \varepsilon_{ji}\varepsilon^k{}_m x^m y_k / 4, & & \text{because of 2 dimesions}\\
&= R \ \varepsilon_{ji} y^k y_k /4\\
&= R \varepsilon_{ji}/4
\end{align}$$
3
: $$\begin{align}
(\nabla_{[i} x^k) \nabla_{j]} y_k
&= (\nabla_{[i} x^k) \nabla_{j]} x^l \varepsilon_{lk}\\
&= (\nabla_{[i} x^k) (\nabla_{j]} x^l) \varepsilon_{lk} \\
&= 0, & &\text{by step 1}
\end{align}$$
4
: $$\begin{align}
(dz_i)_j
&= \nabla_{[j}z_{i]} \\
&= \nabla_{[j} (\nabla_{i]} x^k ) y_k \\
&= (\nabla_{[j} \nabla_{i]} x^k) y_k + (\nabla_{[i} x^k) \nabla_{j]} y_k \\
&= R\varepsilon_{ji}/4, & &\text{by steps 2 and 3}
\end{align}
$$
6
: $$\int_{M}(dz_j)_i = \int_{M} R \varepsilon_{ij}/4 = \int_{M} R/4\ dM$$
7
: So far the only assumptions are Riemannian metric on M and the existence of a differentiable unit vector field x. If the manifold $M$ is also closed and orientable then $z$ has compact support and Stokes theorem implies that
$$\int_{M}(dz_j)_i = \int_{\partial M} z_j = \int_{\emptyset} z_j = 0$$
This yields a contradiction when the total curvature of $M$ is not 0, proving the hairy ball theorem for all closed orientable manifolds with non-zero total curvature. $\square$
In particular a 2-sphere $S$ with radius $r$ has constant positive scalar curvature $R=2/r^2$.
$$\begin{align}
\int_{S} R \varepsilon_{ij}/4
= r^{-2}/2\int_{S} dS
= 2 \pi \neq 0 \
\end{align}
$$
As it stands this only proves the nonexistence of smooth vector fields without zeros on manifolds with nonzero total curvature.
Boothby $\S 4$ proves that this automatically implies the general continuous case.
Code
The use of Stokes theorem can not easilly be automated since xAct does not really support integration on manifolds,
but the equational proof of $(dz_i)_j = R\varepsilon_{ji}/2$ is within the capabilities of xAct using the xTras extension.
load xAct
Needs["xAct`xTras`"]
$PrePrint = ScreenDollarIndices;
$CovDFormat = "Prefix";
$CVVerbose = False;
$DefInfoQ = False;
define abstract 2-manifold
DefManifold[S2, 2, IndexRange[a, n]]
DefMetric[1, met[-a, -b], CD, {";", "\[Del]"}, PrintAs -> "g"]
some shortcuts
eps = epsilon[met]
EV[x_] := FullSimplification[][ToCanonical[x]]
define the hair field and associated forms
DefTensor[x[a], {S2}]
AutomaticRules[x,
MakeRule[{Evaluate[ToCanonical[x[-a] CD[-b]@x[a]]], 0}]]
AutomaticRules[x, MakeRule[{Evaluate[ToCanonical[x[-a] x[a]]], 1}]]
DefTensor[y[a], {S2}]
IndexSetDelayed[y[a_], eps[a, -b] x[b]]
DefTensor[z[-a], {S2}]
IndexSetDelayed[z[a_], CD[a][x[b]] y[-b]]
DefTensor[dz[-a, -b], {S2}]
IndexSetDelayed[dz[a_, b_] , Antisymmetrize[CD[a]@z[b]]]
check definitions
UpValues[y]
UpValues[x]
DownValues[x]
verify proof
check that
y is unit norm
y[a] y[-a] // EV
show that $dz - R\,dM = 0$
dz[-a, -b] - RicciScalar[CD][] eps[-a, -b]/4
% // EV
% // RiemannToWeyl
EV[% y[c]] y[-c]
The above line returns 0.
Each of the preceding lines is an identity transformation.
The last line is just multiplication by 1.
Other neat proofs of the hairy ball theorem
Milnor
: http://scholar.google.com/scholar?cluster=16974770955727113693
Boothby
: http://www.jstor.org/discover/10.2307/2317520
Eisenberg & Guy
: http://www.jstor.org/discover/10.2307/2320587
Dan Piponi
: http://blog.sigfpe.com/2012/11/a-pictorial-proof-of-hairy-ball-theorem.html
