# HOPF

This article defines the Hopf Fibration (HF), the concept
of splitting the

This article consists of two parts:
1) geometric visualization of projection of

# Geometry

Let’s imagine

## Equations

**Definition** (Sphere

**Definition** (Locus). The

**Definition** (Mapping on

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

```
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

## Trivial Fiber Bundle

**Definition** (Trivial Fiber Bundle).
When total space

```
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

```
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

## 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

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

**Definition** (Sphere

```
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

**Example** (

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

**Example** (

```
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** (

```
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 **cup product** square 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