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.