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)$ .
随便看	HighlyAbundantNumber highly abundant number HighlycomplexSystemDiagrams highly-complex system diagrams HighlyCompositeNumber highly composite number HighSchoolMathematics high school mathematics HilbCategoryOfHilbertSpaces HilbertBasisTheorem Hilbert basis theorem HilbertMatrix Hilbert matrix HilbertModule Hilbert module HilbertParallelotope Hilbert parallelotope Hilberts16thProblemForQuadraticVectorFields HilbertsHotel HilbertsIrreducibilityTheorem HilbertsNullstellensatz HilbertSpace Hilbert space HilbertSpacesAreUniformlyConvexSpaces Hilbert spaces are uniformly convex spaces