Equivalence of Definitions of Contractible Space

From ProofWiki
Jump to navigation Jump to search





Theorem

The following definitions of the concept of Contractible Space are equivalent:

Definition 1

$X$ is called contractible if and only if the identity map $\operatorname{id}_X$ is homotopic to a constant map $X \to X$.

Definition 2

$X$ is called contractible if and only if it is homotopy equivalent to a point.


Lemma



When the category of topological spaces $\bf Top$ is endowed with the cartesian monoidal structure, the terminal object $*$ (that is, any singleton set, endowed with the discrete topology) acts as monoidal unit.

$\Box$


Remark

By the lemma above, there is a bijection of sets $\hom(*,X)\cong X$ between the set of functions $* \to X$ and this bijection can be promoted to a homeomorphism transporting to $\hom(*,X)$ the topology on $X$.

Note that the Lemma above and the subsequent remark hold in full generality, even when we do not restrict to a cartesian closed subcategory of $\bf Top$.


Proof of the equivalence

Assume that $X$ is contractible according to definition 1.

Then every $x_0 \in X$ is represented by a unique $\ceiling {x_0}: *\to X$ such that the composition $X \overset {t_X}\to * \overset {\ceiling {x_0} }\to X$ is the constant mapping $X \to X : x \mapsto x_0$.

By assumption, there exists an $x_0$ such that the constant mapping is homotopic to the identity mapping on $X$, which means that $t_X$ and $\ceiling {x_0}$ are mutually inverse homotopy equivalences (the composition $*\to X\to *$ is evidently the identity of $\set {x_0}$).

Similarly, assume that $X$ is contractible according to definition 2.

This means that the terminal map $t_X : X \to *$ has an homotopy inverse $p : *\to X$ such that $X\to *\to X$ is homotopic to the identity of $X$.

But according to the lemma above, there is a unique $x_0\in X$ such that $p = \ceiling {x_0}$.

So again the composition $X \overset {t_X} \to * \overset {\ceiling {x_0} }\to X$ is the constant mapping at $x_0$.

$\blacksquare$