Nottingham FP Lab Blog

Homotopy tutorial 1

by Ambrus Kaposi on November 7, 2012.
Tagged as: Type theory meetings.

Notes from the homotopy tutorial given today by Nicolai Kraus.

From now on, space means topological space and function is continuous function.

Def. $$X$$, $$Y$$ spaces, $$f, g : X \rightarrow Y$$. A homotopy from $$f$$ to $$g$$ is an

$h : X \times [0,1] \rightarrow Y$

function such that

$h(x, 0) = f(x) \text{ and } h(x, 1) = g(x)$

Notation: $$h : f \simeq g$$

Exercise 1. Consider $$f, g : [0,1] \rightarrow X$$ with $$f(0) = g(0)$$. Show that $$f \simeq g$$.

Exercise 2 (later). What does exercise 1 have to do with J (eliminator)?

Exercise 3. What Thorsten said (prove that this is an equivalence relation).

Def. $$X$$, $$Y$$ spaces, $$f : X \rightarrow Y$$ is a homotopy equivalence iff there is a $$g : Y \rightarrow X$$ s.t. $$g \circ f \simeq id_X$$ and $$f \circ g \simeq id_Y$$.

Exercise 4. $$X$$, $$Y$$ spaces, $$X$$, $$Y$$ homeomorphic $$\Rightarrow X \simeq Y$$

Exercise 5 (later). This is a weak equivalence.

Def. $$h : f \simeq g$$, $$f, g : X \rightarrow Y$$, $$A \subseteq X$$. $$h$$ is a homotopy relative to $$A$$ if $$\forall a \in A \: . \: h(a,t)$$ independent of $$t$$.

Exercise 6. $$f, g : [0,1] \rightarrow X, f(0) = g(0), f(1) = g(1)$$. Show that $$f$$ and $$g$$ are not necessarily homotopic relative to $$\{0, 1\}$$.

Exercise 7 (later). What does this have to do with K?

Def. $$X$$ space. $$x_0 \in X$$. Loop space of $$X$$ and $$x_0$$:

$\Omega(X, x_0) = \left\{ f : [0,1] \rightarrow X \: | \: f(0) = f(1) = x_0 \right\} \\ \text{if } f, g \in \Omega(X, x_0) \\ f \bullet g \in \Omega(X, x_0) \\ f \bullet g (t) = \begin{cases} f(2t) & \text{if } t \leq \frac{1}{2} \\ g(2t-1) & \text{otherwise} \\ \end{cases} \\ f^{-1} \in \Omega(X, x_0), f^{-1}(t) = f (1-t) \\$

But this is not associative: $$(h \bullet g) \bullet f \neq h \bullet (g \bullet f)$$, the speed of $$f$$ on the left side is slower than that on the right side. So we define a better version:

Def. $$X$$ space, $$x_0 \in X$$. The fundamental group is:

\eqalign{ \pi_1(X, x_0) := \{ & [f] \: | \: f : [0,1] \rightarrow X, f(0)=f(1)=x_0, \\ & [f]=[g] \leftrightarrow f \simeq g \text{ relative to } \{0, 1\} \} \\ }

Exercise 8. This forms a group.