8.10 Additional Results

Though we do not present the proofs in this chapter, following results have also been established in homotopy type theory.

Theorem 8.10.1.

There exists a $k$ such that for all $n\\geq 3$ , $\\pi_{n+1}(\\mathbb{S}^{n})=\\mathbb{Z}_{k}$ .

Notes on the proof..

The proof consists of a calculation of $\\pi_{4}(\\mathbb{S}^{3})$ , together with anappeal to stability (\\crefcor:stability-spheres). In the classicalstatement of this result, $k$ is $2$ . While we have not yet checked that $k$ is in fact $2$ , our calcluation of $\\pi_{4}(\\mathbb{S}^{3})$ is constructive,like all the rest of the proofs in this chapter.(More precisely, it doesn’t use any additional axioms such as $\\mathsf{LEM}$ or $\\mathsf{AC}$ , making it as constructive asunivalence and higher inductive types are.) Thus, given acomputational interpretation of homotopy type theory, we could run theproof on a computer to verify that $k$ is $2$ . This example is quiteintriguing, because it is the first calculation of a homotopy groupfor which we have not needed to know the answer in advance.∎

Theorem 8.10.2 (Blakers–Massey theorem).

Suppose we are given maps $f:C\\rightarrow X$ , and $g:C\\rightarrow Y$ . Taking first the pushout $X\\sqcup^{C}Y$ of $f$ and $g$ and then the pullback of its inclusions ${\\mathsf{inl}}:X\\rightarrow X\\sqcup^{C}Y\\leftarrow Y:{\\mathsf{inr}}$ , we have an induced map $C\\to X\\times_{(X\\sqcup^{C}Y)}Y$ .

If $f$ is $i$ -connected and $g$ is $j$ -connected, then this induced map is $(i+j)$ -connected. In other words, for any points $x : X$ , $y : Y$ , the corresponding fiber $C_{x,y}$ of $(f,g):C\\to X\\times Y$ gives an approximation to the path space ${\\mathsf{inl}}(x)=_{X\\sqcup^{C}Y}{\\mathsf{inr}}(y)$ in the pushout.

It should be noted that in classical algebraic topology, the Blakers–Massey theorem is often stated in a somewhat different form, where the maps $f$ and $g$ are replaced by inclusions of subcomplexes of CW complexes, and the homotopy pushout and homotopy pullback by a union and intersection, respectively.In order to express the theorem in homotopy type theory, we have to replace notions of this sort with ones that are homotopy-invariant.We have seen another example of this in the van Kampen theorem (\\autorefsec:van-kampen), where we had to replace a union of open subsets by a homotopy pushout.

Theorem 8.10.3 (Eilenberg–Mac Lane Spaces).

For any abelian group $G$ and positive integer $n$ , there is an $n$ -type $K(G,n)$ such that $\\pi_{n}(K(G,n))=G$ , and $\\pi_{k}(K(G,n))=0$ for $k\eq n$ .

Theorem 8.10.4 (Covering spaces).

For a connected space $A$ , there is an equivalence between covering spaces over $A$ and sets with an action of $\\pi_{1}(A)$ .

单词	810AdditionalResults
释义	8.10 Additional Results Though we do not present the proofs in this chapter, following results have also been established in homotopy type theory. Theorem 8.10.1. There exists a $k$ such that for all $n\\geq 3$ , $\\pi_{n+1}(\\mathbb{S}^{n})=\\mathbb{Z}_{k}$ . Notes on the proof.. The proof consists of a calculation of $\\pi_{4}(\\mathbb{S}^{3})$ , together with anappeal to stability (\\crefcor:stability-spheres). In the classicalstatement of this result, $k$ is $2$ . While we have not yet checked that $k$ is in fact $2$ , our calcluation of $\\pi_{4}(\\mathbb{S}^{3})$ is constructive,like all the rest of the proofs in this chapter.(More precisely, it doesn’t use any additional axioms such as $\\mathsf{LEM}$ or $\\mathsf{AC}$ , making it as constructive asunivalence and higher inductive types are.) Thus, given acomputational interpretation of homotopy type theory, we could run theproof on a computer to verify that $k$ is $2$ . This example is quiteintriguing, because it is the first calculation of a homotopy groupfor which we have not needed to know the answer in advance.∎ Theorem 8.10.2 (Blakers–Massey theorem). Suppose we are given maps $f:C\\rightarrow X$ , and $g:C\\rightarrow Y$ . Taking first the pushout $X\\sqcup^{C}Y$ of $f$ and $g$ and then the pullback of its inclusions ${\\mathsf{inl}}:X\\rightarrow X\\sqcup^{C}Y\\leftarrow Y:{\\mathsf{inr}}$ , we have an induced map $C\\to X\\times_{(X\\sqcup^{C}Y)}Y$ . If $f$ is $i$ -connected and $g$ is $j$ -connected, then this induced map is $(i+j)$ -connected. In other words, for any points $x : X$ , $y : Y$ , the corresponding fiber $C_{x,y}$ of $(f,g):C\\to X\\times Y$ gives an approximation to the path space ${\\mathsf{inl}}(x)=_{X\\sqcup^{C}Y}{\\mathsf{inr}}(y)$ in the pushout. It should be noted that in classical algebraic topology, the Blakers–Massey theorem is often stated in a somewhat different form, where the maps $f$ and $g$ are replaced by inclusions of subcomplexes of CW complexes, and the homotopy pushout and homotopy pullback by a union and intersection, respectively.In order to express the theorem in homotopy type theory, we have to replace notions of this sort with ones that are homotopy-invariant.We have seen another example of this in the van Kampen theorem (\\autorefsec:van-kampen), where we had to replace a union of open subsets by a homotopy pushout. Theorem 8.10.3 (Eilenberg–Mac Lane Spaces). For any abelian group $G$ and positive integer $n$ , there is an $n$ -type $K(G,n)$ such that $\\pi_{n}(K(G,n))=G$ , and $\\pi_{k}(K(G,n))=0$ for $k\eq n$ . Theorem 8.10.4 (Covering spaces). For a connected space $A$ , there is an equivalence between covering spaces over $A$ and sets with an action of $\\pi_{1}(A)$ .
随便看	asymptote AsymptoteOfAnArctangent asymptote of an arctangent AsymptotesOfGraphOfRationalFunction asymptotes of graph of rational function AsymptoticallyStable asymptotically stable AsymptoticBasis asymptotic basis AsymptoticBoundsForFactorial asymptotic bounds for factorial AsymptoticDensity asymptotic density AsymptoticEstimate asymptotic estimate AsymptoticEstimatesForRealvaluedNonnegativeMultiplicativeFunctions asymptotic estimates for real-valued nonnegative multiplicative functions AsymptoticsOfCentralBinomialCoefficient asymptotics of central binomial coefficient Atom atom AtomicFormula atomic formula AtommeasureTheory atom (measure theory)