HOPF

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.

Geometry

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

Equations

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);
};

Topology

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

Fiber

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 .

Literature

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