michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(hott) update book.md

Browse source
This commit is contained in:
Jakob von Raumer 2016-07-18 17:25:59 +02:00 committed by Leonardo de Moura
parent 548671ce1b
commit 3416430cfa
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
hott/book.md
View file

@ -149,11 +149,11 @@ Every file is in the folder [homotopy](homotopy/homotopy.md)
- 8.2 (Connectedness of suspensions): [susp](homotopy/susp.hlean) (different proof of Theorem 8.2.1) - 8.2 (Connectedness of suspensions): [susp](homotopy/susp.hlean) (different proof of Theorem 8.2.1)
- 8.3 (πk≤n of an n-connected space and π_{k<n}(S^n)): [homotopy_group](homotopy/homotopy_group.hlean) - 8.3 (πk≤n of an n-connected space and π_{k<n}(S^n)): [homotopy_group](homotopy/homotopy_group.hlean)
- 8.4 (Fiber sequences and the long exact sequence): Mostly in [homotopy.chain_complex](homotopy/chain_complex.hlean), [homotopy.LES_of_homotopy_groups](homotopy/LES_of_homotopy_groups.hlean). Definitions 8.4.1 and 8.4.2 in [types.pointed](types/pointed.hlean), Corollary 8.4.8 in [homotopy.homotopy_group](homotopy/homotopy_group.hlean). - 8.4 (Fiber sequences and the long exact sequence): Mostly in [homotopy.chain_complex](homotopy/chain_complex.hlean), [homotopy.LES_of_homotopy_groups](homotopy/LES_of_homotopy_groups.hlean). Definitions 8.4.1 and 8.4.2 in [types.pointed](types/pointed.hlean), Corollary 8.4.8 in [homotopy.homotopy_group](homotopy/homotopy_group.hlean).
- 8.5 (The Hopf fibration): [circle](homotopy/circle.hlean) (multiplication on the circle, Lemma 8.5.8), [join](homotopy/join.hlean) (join is associative, Lemma 8.5.9), [hopf](homotopy/hopf.hlean) (The Hopf construction, Lemmas 8.5.5 and 8.5.7), [complex_hopf](homotopy/complex_hopf.hlean) (the H-space structure on the circle and the complex Hopf fibration) - 8.5 (The Hopf fibration): [hit.pushout](hit/pushout.hlean) (Lemma 8.5.3), [hopf](homotopy/hopf.hlean) (The Hopf construction, Lemmas 8.5.5 and 8.5.7), [susp](homotopy/susp.hlean) (Definition 8.5.6), [circle](homotopy/circle.hlean) (multiplication on the circle, Lemma 8.5.8), [join](homotopy/join.hlean) (join is associative, Lemma 8.5.9), [complex_hopf](homotopy/complex_hopf.hlean) (the H-space structure on the circle and the complex Hopf fibration, i.e. Theorem 8.5.1), [sphere2](homotopy/sphere2.hlean) (Corollary 8.5.2)
- 8.6 (The Freudenthal suspension theorem): [connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2). Corollary 8.6.14 is proven directly in [homotopy.freudenthal](homotopy/freudenthal.hlean), however, we don't prove it as a Corollary of Theorem 8.6.4, which is not proven. Stability of iterated suspensions is also in [homotopy.freudenthal](homotopy/freudenthal.hlean). The homotopy groups of spheres in this section are computed in [homotopy.sphere2](homotopy/sphere2.hlean). - 8.6 (The Freudenthal suspension theorem): [connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2). Corollary 8.6.14 is proven directly in [freudenthal](homotopy/freudenthal.hlean), however, we don't prove Theorem 8.6.4. Stability of iterated suspensions is also in [freudenthal](homotopy/freudenthal.hlean). The homotopy groups of spheres in this section are computed in [sphere2](homotopy/sphere2.hlean).
- 8.7 (The van Kampen theorem): not formalized - 8.7 (The van Kampen theorem): [vankampen](homotopy/vankampen.hlean) (the pushout of Groupoids is formalized in [algebra.category.constructions.pushout](algebra/category/constructions/pushout.hlean) with some definitions in [algebra.graph](algebra/graph.hlean))
- 8.8 (Whitehead’s theorem and Whitehead’s principle): 8.8.1 and 8.8.2 at the bottom of [types.trunc](types/trunc.hlean), 8.8.3 in [homotopy.homotopy_group](homotopy/homotopy_group.hlean). - 8.8 (Whitehead’s theorem and Whitehead’s principle): 8.8.1 and 8.8.2 at the bottom of [types.trunc](types/trunc.hlean), 8.8.3 in [homotopy_group](homotopy/homotopy_group.hlean). [Rest to be moved]
- 8.9 (A general statement of the encode-decode method): One variation of the encode-decode method is in [types.eq](types/eq.hlean). - 8.9 (A general statement of the encode-decode method): [types.eq](types/eq.hlean).
- 8.10 (Additional Results): Theorem 8.10.3 is formalized in [homotopy.EM](homotopy/EM.hlean). - 8.10 (Additional Results): Theorem 8.10.3 is formalized in [homotopy.EM](homotopy/EM.hlean).
Chapter 9: Category theory Chapter 9: Category theory
@ -169,7 +169,7 @@ Every file is in the folder [algebra.category](algebra/category/category.md)
- 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition) - 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition)
- 9.7 (†-categories): not formalized - 9.7 (†-categories): not formalized
- 9.8 (The structure identity principle): not formalized - 9.8 (The structure identity principle): not formalized
- 9.9 (The Rezk completion): not formalized - 9.9 (The Rezk completion): [constructions.rezk](algebra/category/constructions/rezk.hlean], 9.9.1 and 9.9.2 in [constructions.functor](algebra/category/constructions/functor.hlean]
Chapter 10: Set theory Chapter 10: Set theory
---------- ----------