Proving the hairy ball theorem using xAct

I would like to formally prove the hairy ball theorem in Mathematica, initially just for $S^2$, and then see about generalizing.

An approach I thought about to use the xAct package to define $S^2$ and then derive a contradiction from \begin{align} x^i x_i &= 1 \text{ (unit norm)} \end{align} on $S^2$. This will turn into a rats nest of Christoffel symbols on multiple charts, but with Mathematica that should not be a problem.

Is this a reasonable approach?

Also I am new to xAct, what do I need to do to set up $S^2$ in xAct? Is that what xCoba is for?

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.

Needs["xActxTras"]

$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]]]

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

Eisenberg & Guy : http://www.jstor.org/discover/10.2307/2320587

• Always nice to see a citation to a 35-year-old paper I co-authored! – murray Mar 2 '15 at 21:25
• @murray Even nicer to meet the author :) – Daniel Mahler Mar 2 '15 at 21:36