\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{homotopy group} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{homotopy_theory}{}\paragraph*{{Homotopy theory}}\label{homotopy_theory} [[!include homotopy - contents]] \hypertarget{algebraic_topology}{}\paragraph*{{Algebraic topology}}\label{algebraic_topology} [[!include algebraic topology - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{Definition}{Definition}\dotfill \pageref*{Definition} \linebreak \noindent\hyperlink{ForTopologicalSpaces}{For topological spaces}\dotfill \pageref*{ForTopologicalSpaces} \linebreak \noindent\hyperlink{for_simplicial_sets}{For simplicial sets}\dotfill \pageref*{for_simplicial_sets} \linebreak \noindent\hyperlink{for_lie_groupoids}{For Lie groupoids}\dotfill \pageref*{for_lie_groupoids} \linebreak \noindent\hyperlink{for_objects_in_a_general_stack_topos}{For objects in a general $\infty$-stack $(\infty,1)$-topos}\dotfill \pageref*{for_objects_in_a_general_stack_topos} \linebreak \noindent\hyperlink{truncconn}{Truncated and connected spaces}\dotfill \pageref*{truncconn} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{in_low_dimensions}{In low dimensions}\dotfill \pageref*{in_low_dimensions} \linebreak \noindent\hyperlink{of_the_circle}{Of the circle}\dotfill \pageref*{of_the_circle} \linebreak \noindent\hyperlink{of_spheres}{Of spheres}\dotfill \pageref*{of_spheres} \linebreak \noindent\hyperlink{history}{History}\dotfill \pageref*{history} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{some_general_nonsense}{Some general nonsense}\dotfill \pageref*{some_general_nonsense} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak \noindent\hyperlink{formalization_in_hott}{Formalization in HoTT}\dotfill \pageref*{formalization_in_hott} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} The \emph{homotopy groups} $\pi_n(X,x)$ of a [[pointed object|pointed]] [[topological space]] $(X,x)$ are a sequence of [[groups]] that generalise the [[fundamental group]] $\pi_1(X,x)$ to higher [[homotopy (as a transformation)|homotopies]]. The $n$th homotopy group $\pi_n(X,x)$ has as elements [[equivalence classes]] of [[spheres]] $\gamma : S_*^n \to X_*$ in $X$ where two such are regarded as equivalent if there is a [[left homotopy]] $\gamma \Rightarrow \gamma'$ between them, fixing the base point. The group operation is given by gluing of two spheres at their basepoint. In degree 0, $\pi_0(X,x)$ is not a group but merely a [[pointed set]]. In degree $n \geq 2$ all homotopy groups are [[abelian groups]]. Only $\pi_1(X,x)$ may be an arbitrary group. In general, $\pi_n(X,x)$ is an $n$-[[k-tuply groupal n-groupoid|tuply groupal]] set. Lower homotopy groups [[action|act]] on higher homotopy groups; the nonabelian group cohomology of this gives the Postnikov invariants of the space. All of this data put together allows one to reconstruct the original space, at least up to weak [[homotopy type]], through its [[Postnikov system]]. These definitions only depend on the [[homotopy type]] of $X$, by definition: a [[weak homotopy equivalence]] between topological spaces is a [[continuous map]] that induces an [[isomorphism]] on all homotopy groups. Accordingly, homotopy groups are defined for all other models of [[homotopy types]], notably for [[simplicial sets]]. See at \emph{[[simplicial homotopy group]]} for more. There are generalizations of the concept to [[stable homotopy groups]] of [[spectra]] and to [[equivariant homotopy groups]] for [[topological G-spaces]] and [[equivariant spectra]]. \hypertarget{Definition}{}\subsection*{{Definition}}\label{Definition} \hypertarget{ForTopologicalSpaces}{}\subsubsection*{{For topological spaces}}\label{ForTopologicalSpaces} Let $X$ be a [[topological space]], let $x : * \to X$ be a point, to be called the \emph{base point}. For $n \in \mathbb{N}$, let $S^n$ be the pointed $n$-[[sphere]]. \begin{defn} \label{}\hypertarget{}{} The underlying set of $\pi_n(X,x)$ is the set of [[equivalence classes]] of basepoint-preserving [[continuous functions]] \begin{displaymath} \gamma : S^n \to X \end{displaymath} where two such are regarded as equivalent if there is a basepoint-preserving [[left homotopy]] between them. \end{defn} Now we will put some structure on that set. \begin{defn} \label{}\hypertarget{}{} There are $n$ independent equators through the basepoint of $S^n$. Given two maps $f, g: S^n \to (X,x)$, form their [[coproduct|copairing]] in the category of pointed spaces to get a map \begin{displaymath} S^n \vee S^n \to (X,x) \end{displaymath} (where $\vee$ indicates the [[wedge sum]]); then combine this with a map $S^n \to S^n \vee S^n$ that maps the $i$th equator to the basepoint and each hemisphere to one copy of the sphere. The result is a map $S^n \to (X,x)$, called the $i$th \textbf{concatenation} of $f$ and $g$: \begin{displaymath} S^n \to_i S^n \vee S^n \stackrel{[f,g]}{\to} (X,x) \,. \end{displaymath} One can check that each of these operations respects homotopy equivalence and hence equips $\pi_n(X,x)$ with the structure of a [[magma]]. \end{defn} \begin{prop} \label{}\hypertarget{}{} These magmas are in fact [[groups]]; in particular: \begin{itemize}% \item the [[constant function]] that maps all of $S^n$ to $x$ represents the \textbf{null element} of $\pi_n(X,x)$, which is an identity for every concatenation. \end{itemize} \end{prop} \begin{remark} \label{}\hypertarget{}{} This is closely related to the statement that the [[positive dimension spheres are H-cogroup objects]] (see there) in the [[homotopy category]] of [[pointed topological spaces]]. \end{remark} \begin{defn} \label{}\hypertarget{}{} This may seem like quite a complicated kind of structure, but it is actually quite simple up to homotopy. First of all, all $n$ concatenations of given maps $f$ and $g$ are homotopic, so we speak of simply a single \textbf{concatenation} for $n \geq 1$ (and none for $n = 0$). By the [[Eckmann-Hilton argument]], this concatenation will be commutative up to homotopy for $n \geq 2$. In any case, it is [[associativity|associative]] and [[inverse|invertible]] up to homotopy, and the null element is an identity up to homotopy. \end{defn} \begin{prop} \label{}\hypertarget{}{} The result is that the set $\pi_n(X,x)$ of equivalence classes is an abelian group for $n \geq 2$, a group for $n = 1$, and a pointed set for $n = 0$ (when the null element is the only structure). \end{prop} \begin{prop} \label{}\hypertarget{}{} If $X$ is [[connected space|path-connected]], then all of the $\pi_n(X,a)$ are [[isomorphism|isomorphic]]. Accordingly, it's traditional to just write $\pi_n(X)$ in that case. (This is why we must use $\Pi_n(X)$ for the homotopy $n$-groupoid.) However, there may be many different isomorphisms between $\pi_n(X,a)$ and $\pi_n(X,b)$ (given by $\pi_{n+1}(X)$), so a more careful treatment requires keeping track of the basepoint even in the connected case. \end{prop} \hypertarget{for_simplicial_sets}{}\subsubsection*{{For simplicial sets}}\label{for_simplicial_sets} See [[simplicial homotopy group]]. \hypertarget{for_lie_groupoids}{}\subsubsection*{{For Lie groupoids}}\label{for_lie_groupoids} \begin{itemize}% \item [[homotopy groups of a Lie groupoid]] \end{itemize} \hypertarget{for_objects_in_a_general_stack_topos}{}\subsubsection*{{For objects in a general $\infty$-stack $(\infty,1)$-topos}}\label{for_objects_in_a_general_stack_topos} [[Top]] is the archetypical [[(∞,1)-topos]]. The definition of homotopy groups for objects in [[Top]] is just a special case of a general definition of homotopy groups of objects of [[∞-stack]] [[(∞,1)-topos]]es. This is described in detail at \begin{itemize}% \item [[homotopy groups in an (∞,1)-topos]]. \end{itemize} \hypertarget{truncconn}{}\subsection*{{Truncated and connected spaces}}\label{truncconn} Often it is useful to talk about spaces whose homotopy groups are all trivial above or below a certain degree, for instance in the context of [[Postnikov towers]] and [[Whitehead towers]]. For $n = -1, 0, 1, 2, \ldots, \infty$: \begin{itemize}% \item a space is \textbf{$n$-[[truncated space|truncated]]} if all homotopy groups \emph{above} degree $n$ are trivial. \item a space is \textbf{$n$-[[n-connected space|connected]]} (or \textbf{$n$-simply connected}) if it is [[inhabited space|inhabited]] and all homotopy groups \emph{at or below} degree $n$ are trivial. \end{itemize} Vacuously, every space is $\infty$-truncated, and precisely the inhabited spaces are $(-1)$-connected. On the other end, precisely the weakly [[contractible spaces]] are $\infty$-connected, and a space is $(-1)$-truncated iff it is weakly contractible if inhabited. (So [[classical mathematics|classically]], using [[excluded middle]], a space is $(-1)$-truncated iff it is either [[empty space|empty]] or weakly contractible.) To extend one step further in [[negative thinking]], every space (even the empty space) is $(-2)$-connected, and precisely a weakly contractible space (but not the empty space) is $(-2)$-truncated. \begin{itemize}% \item A [[pointed space]] is a \textbf{degree-$n$ [[Eilenberg?MacLane space]]} if it is both $n$-truncated as well as $(n-1)$-connected, i.e. if its only nontrivial homotopy group is in degree $n$. \end{itemize} A weakly contractible space is an Eilenberg--MacLane space in every degree, and these are the only Eilenberg--MacLane spaces in degree $\infty$ or $-1$. In degree $0$, they are the pointed [[discrete space]]s (and those weakly homotopy equivalent to such). In degree $1$, they are (up to weak homotopy equivalence) precisely the [[classifying spaces]] of [[groups]]. And so on. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \hypertarget{in_low_dimensions}{}\subsubsection*{{In low dimensions}}\label{in_low_dimensions} The $0$th homotopy `group' $\pi_0(X,a)$ can be identified with the set of all [[path component]]s of $X$, with the component containing $a$ as the basepoint. Similarly, the [[fundamental infinity-groupoid|fundamental 0-groupoid]] $\Pi_0(X)$ is the set of all path components without a chosen basepoint. Note that $\Pi_0(X)$ is traditionally written $\pi_0(X)$, even without a basepoint. The $1$st homotopy group $\pi_1(X,a)$ is precisely the [[fundamental group]] of $X$ at $a$. This is the original example from which all others derived. It was once written simply $\pi(X,a)$ with the $\pi$ standing for Poincar\'e{}, who invented it. At least, that's where I \emph{think} that it comes from \ldots{} ---Toby \hypertarget{of_the_circle}{}\subsubsection*{{Of the circle}}\label{of_the_circle} The first homotopy group of the [[circle]] $S^1$ is the group of [[integer]]s. \begin{displaymath} \pi_1(S^1) \simeq \mathbb{Z} \,. \end{displaymath} A formalization of a proof of this in [[homotopy type theory]] is in (\hyperlink{ShulmanPi1S1}{Shulman}). \hypertarget{of_spheres}{}\subsubsection*{{Of spheres}}\label{of_spheres} See [[homotopy groups of spheres]]. \hypertarget{history}{}\subsection*{{History}}\label{history} In the early years of the 20th century it was known that the nonabelian fundamental group $\pi_1(X,a)$ of a space $X$ with base point $a$ was useful in geometry and complex analysis. It was also known that the abelian [[homology group]]s $H_n(X)$ existed for all $n \geq 0$ and that if $X$ is connected then $H_1(X)$ is isomorphic to the abelianisation of any $\pi_1(X,a)$. Consequently it was hoped to generalise the fundamental group to higher dimensions, producing nonabelian groups whose abelianisations would be the homology groups. In 1932, E. ech proposed a definition of higher homotopy groups using maps of spheres, but the paper was rejected for the Zurich ICM since it was found that these groups $\pi_n(X,a)$ were abelian for $n \geq 2$, and so do not generalise the fundamental group in the way that was originally desired. Nonetheless, they have proved to be extremely important in homotopy theory, although more difficult to compute in general than homology groups. See [[weak homotopy equivalence]]. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} It was early realised that the fundamental groupoid $\Pi_1(X)$ operates on the family of groups $\{\pi_n(X,a) | a \in X\}$ which should thus together be regarded as a module over $\pi_1(X,a)$. A key property of homotopy groups is the \emph{Whitehead theorem}: if $f:X \to Y$ is a map of connected [[m-cofibrant spaces]] (spaces each of the homotopy type of a [[CW complex]]), and $f$ induces isomorphisms $\pi_n(X,a) \to \pi_n(Y,f(a))$ for some $a$ and all $n \geq 1$, then $f$ is a [[homotopy equivalence]]. However, the homotopy groups by themselves, even considering the operations of $\pi_1$, do not characterise homotopy types. See also [[algebraic homotopy|algebraic homotopy theory]]. See also the \emph{[[Freudenthal suspension theorem]]}. \hypertarget{some_general_nonsense}{}\subsection*{{Some general nonsense}}\label{some_general_nonsense} Using the [[Eckmann-Hilton duality]] between [[cohomology]] and [[homotopy (as an operation)]] one may discuss homotopy groups along the same lines as the discussion of [[cohomology groups]] (see there). From that perspective we might say that: for $B, X$ any two objects in an [[(∞,1)-topos]] $\mathbf{H}$, the ``homotopy of $X$ with co-coefficients $B$'' is the [[hom-set]] \begin{displaymath} \pi_H(X,B) := H(B,X) := \pi_0 \mathbf{H}(B,X) \,, \end{displaymath} where $\pi_H$ denotes the [[homotopy category of an (infinity,1)-category|homotopy category]] of $\mathbf{H}$. For the special case that the object $B$ here is a [[co-group object]], this \emph{homotopy set} $\pi(X,B)$ naturally inherits the structure of a [[group]]. The standard example is that where $B = S^n$ is the $n$-[[sphere]]. This naturally comes with an co-group structure up to homotopy, which is precisely the structure underlying the co-category structure of the [[interval object]] and more generally that underlying the mechanism of the [[Trimble n-category]]. As opposed to [[cohomology]] where people are used to talking about [[generalized cohomology]], ``homotopy'' usually just means this ordinary homotopy for $B = S^n$. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[homotopy group of a spectrum]] \item [[weak homotopy equivalence]] \item [[p-localization]] \item [[Goodwillie calculus]] \item [[homotopy groups in an (infinity,1)-topos]] \item [[finite homotopy type]], [[nilpotent homotopy type]], [[p-local homotopy type]], [[p-complete homotopy type]] \item [[equivariant homotopy group]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \hypertarget{general}{}\subsubsection*{{General}}\label{general} \begin{itemize}% \item [[Paul Goerss]], [[Rick Jardine]], section I.7 of \emph{[[Simplicial homotopy theory]]}, Progress in Mathematics, Birkh\"a{}user (1996) \item Marcelo Aguilar, [[Samuel Gitler]], Carlos Prieto, section 3.4 of \emph{Algebraic topology from a homotopical viewpoint}, Springer (2002) (\href{http://tocs.ulb.tu-darmstadt.de/106999419.pdf}{toc pdf}) \item [[Michael Hutchings]], \emph{Introduction to higher homotopy groups and obstruction theory} (\href{http://math.berkeley.edu/~hutching/teach/215b-2011/homotopy.pdf}{pdf}) \end{itemize} \hypertarget{formalization_in_hott}{}\subsubsection*{{Formalization in HoTT}}\label{formalization_in_hott} Homotopy groups and their properties can naturally be formalized in [[homotopy type theory]]. In this context a proof that $\pi_1(S^1)\simeq \mathbb{Z}$ is in \begin{itemize}% \item [[Mike Shulman]], \emph{\href{https://github.com/HoTT/HoTT/blob/master/Coq/HIT/Pi1S1.v}{P1S1.v}} \item [[Dan Licata]], [[Mike Shulman]], \emph{Calculating the fundamental group of the circle in homotopy type theory} (\href{http://www.cs.cmu.edu/~drl/pubs/ls13pi1s1/ls13pi1s1.pdf}{pdf}) \end{itemize} and a proof that $\pi_k(S^n) \simeq \left\{ \itexarray{ 0 & for \;k \lt n \\ \mathbb{Z} & for\; k = n} \right.$ is in \begin{itemize}% \item [[Dan Licata]], [[Guillaume Brunerie]], \emph{\href{https://github.com/dlicata335/hott-agda/blob/master/homotopy/PiNSN.agda}{PiNSN.agda}} \end{itemize} [[!redirects homotopy group]] [[!redirects homotopy groups]] [[!redirects homotopy n-tuply groupal set]] [[!redirects homotopy n-tuply groupal sets]] [[!redirects homotopy groupal set]] [[!redirects homotopy groupal sets]] [[!redirects homotopy pointed set]] [[!redirects homotopy pointed sets]] [[!redirects homotopy abelian group]] [[!redirects homotopy abelian groups]] \end{document}