Hopf Fibrations

The geometric and topological interpretation


This article defines the Hopf Fibration (HF), the concept of splitting the sphere onto the twisted cartesian product of spheres and . Basic HF applications are: 1) HF is a Fiber Bundle structure of Dirac Monopole; 2) HF is a map from the in H to the Bloch sphere; 3) If HF is a vector field in then there exists a solution to compressible non-viscous Navier-Stokes equations. It was figured out that there are only 4 dimensions of fibers with Hopf invariant 1, namely , , , .

This article consists of two parts: 1) geometric visualization of projection of to (frontend); 2) formal topological version of HF in cubical type theory (backend). Consider this a basic intro and a summary of results or companion guide to the chapter 8.5 from HoTT.


Let’s imagine as smooth differentiable manifold and build a projection onto the display as if demoscene is still alive.


Definition (Sphere ). Like a little baby in :after math classes in quaternions :

Definition (Locus). The is realized as a disjoint union of circular fibers in Hopf coordinates , where and :

Definition (Mapping on ). A mapping of the Locus to the has points on the circles parametrized by :

Code in three.js:

var fiber = new THREE.Curve(), color = sphericalCoords.color; fiber.getPoint = function(t) { var eta = sphericalCoords.eta, phi = sphericalCoords.phi, theta = 2 * Math.PI * t; var x1 = Math.cos(phi+theta) * Math.sin(eta/2), x2 = Math.sin(phi+theta) * Math.sin(eta/2), x3 = Math.cos(phi-theta) * Math.cos(eta/2), x4 = Math.sin(phi-theta) * Math.cos(eta/2); var m = mag([x1,x2,x3]), r = Math.sqrt((1-x4)/(1+x4)); return new THREE.Vector3(r*x1/m,r*x2/m, r*x3/m); };


Can we reason about spheres without a metric? Yes! But can we do this in a constructive way? Also yes.


Definition (Fiber). The fiber of the map in a point is all points such that .

fiber (E B: U) (p: E -> B) (y: B): U = (x: E) * Path B y (p x)

Fiber Bundle

Definition (Fiber Bundle). The fiber bundle on a total space with fiber layer and base is a structure where is a surjective map with following property: for any point exists a neighborhood for which a homeomorphism making the following diagram commute.

Trivial Fiber Bundle

Definition (Trivial Fiber Bundle). When total space is cartesian product and then such bundle is called trivial .

Family (B: U): U = B -> U total (B: U) (F: Family B): U = Sigma B F trivial (B: U) (F: Family B): total B F -> B = \ (x: total B F) -> x.1

Theorem (Fiber Bundle is a Type Family). Inverse image (fiber) of fiber bundle in point equals .

FiberPi (B: U) (F: B -> U) (y: B) : Path U (fiber (total B F) B (trivial B F) y) (F y)

Definition (Structure Group). The structure group of an -fiber bundle is just Aut(F), the loop space of BAut(F).

Higher Spheres

Definition (2-points, Bool, Sphere ).

data bool = false | true

Definition (Suspension).

data susp (A: U) = north | south | merid (a: A) <i> [ (i = 0) -> north, (i = 1) -> south ]

Definition (Sphere ). Direct definition.

data S1 = base | loop <i> [ (i = 0) -> base, (i = 1) -> base ]

Definition (Sphere ). Recursive definition.

S: nat -> U = split zero -> bool succ x -> susp (S x) S2: U = susp S1 S3: U = susp S2 S4: U = susp S3

Hopf Fibrations

Theorem (Hopf Fibrations). There are fiber bundles:

Definition (H-space). H-space over a carrier is a tuple.

Example ( Hopf Fiber ). Mobius fiber. In cubicaltt type checker.

moebius : S1 -> U = split base -> bool loop @ i -> ua bool bool negBoolEquiv @ i H0 : U = (c : S1) * moebius c

Example ( Hopf Fiber ). Guillaume Brunerie. In cubicaltt type checker.

rot: (x : S1) -> Path S1 x x = split base -> loop1 loop @ i -> constSquare S1 base loop1 @ i mu : S1 -> equiv S1 S1 = split base -> idEquiv S1 loop @ i -> equivPath S1 S1 (idEquiv S1) (idEquiv S1) ( \(x : S1) -> rot x @ j) @ i H : S2 -> U = split north -> S1 south -> S1 merid x @ i -> ua S1 S1 (mu x) @ i total : U = (c : S2) * H c

Example ( Hopf Fiber ). By Egbert Rijke and Ulrik Buchholtz. In Lean prover.

definition pfiber_quaternionic_phopf : pfiber quaternionic_phopf ≃* S* 3 := begin fapply pequiv_of_equiv, { esimp, unfold [quaternionic_hopf], refine fiber.equiv_precompose (sigma.pr1 ◦ (hopf.total (S 3))−1e) (join.spheres (of_nat 3) (of_nat 3)) − 1 e _ ·e _, refine fiber.equiv_precompose _ (hopf.total (S 3))− 1 e _ ·e _, apply fiber_pr1 }, { reflexivity } end

Definition (Hopf Invariant). Let a continuous map. Then homotopy pushout (cofiber) of is has ordinary cohomologyHence for generators of the cohomology groups in degree and , respectively, there exists an integer that expresses the cup product square of as a multiple of . This integer is called Hopf invariant of .

Theorem (Adams, Atiyah). Hopf Fibrations are only maps that have Hopf invariant .


[1]. Ulrik Buchholtz, Egbert Rijke. The Cayley-Dickson Construction in Homotopy Type Theory