feat(homotopy/homotopy_group): add theorems in section 8.3 of the HoTT book

hott/book.md

@@ -22,7 +22,7 @@ The rows indicate the chapters, the columns the sections.
 | Ch 5  | - | . | ½ | - | - | . | . | ½ |   |    |    |    |    |    |    |
 | Ch 6  | . | + | + | + | + | ½ | ½ | + | ¾ | ¼  | ¾  | +  | .  |    |    |
 | Ch 7  | + | + | + | - | ¾ | - | - |   |   |    |    |    |    |    |    |
-| Ch 8  | + | + | - | - | ¼ | ¼ | - | - | - | -  |    |    |    |    |    |
+| Ch 8  | + | + | + | - | ¼ | ¼ | - | - | - | -  |    |    |    |    |    |
 | Ch 9  | ¾ | + | + | ½ | ¾ | ½ | - | - | - |    |    |    |    |    |    |
 | Ch 10 | - | - | - | - | - |   |   |   |   |    |    |    |    |    |    |
 | Ch 11 | - | - | - | - | - | - |   |   |   |    |    |    |    |    |    |
@@ -143,7 +143,7 @@ Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy
 
 - 8.1 (π_1(S^1)): [homotopy.circle](homotopy/circle.hlean) (only the encode-decode proof)
 - 8.2 (Connectedness of suspensions): [homotopy.connectedness](homotopy/connectedness.hlean) (different proof)
-- 8.3 (πk≤n of an n-connected space and π_{k<n}(S^n)): not formalized
+- 8.3 (πk≤n of an n-connected space and π_{k<n}(S^n)): [homotopy.homotopy_group](homotopy/homotopy_group.hlean)
 - 8.4 (Fiber sequences and the long exact sequence): not formalized
 - 8.5 (The Hopf fibration): [homotopy.circle](homotopy/circle.hlean) (H-space structure on the circle, Lemma 8.5.8), [homotopy.join](homotopy/join.hlean) (join is associative, Lemma 8.5.9), the rest is not formalized
 - 8.6 (The Freudenthal suspension theorem): [homotopy.connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [homotopy.wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2), the rest is not formalized

hott/homotopy/homotopy.md

@@ -16,3 +16,4 @@ folder (sorted such that files only import previous files).
 * [connectedness](connectedness.hlean)
 * [cofiber](cofiber.hlean)
 * [smash](smash.hlean)
+* [homotopy_group](homotopy_group.hlean) (theorems about homotopy groups. The definition and basic facts about homotopy groups is in [algebra/homotopy_group](../algebra/homotopy_group.hlean)).

hott/homotopy/homotopy_group.hlean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2016 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Clive Newstead
+
+-/
+
+import algebra.homotopy_group .connectedness
+
+open eq is_trunc trunc_index pointed algebra trunc nat homotopy
+
+namespace is_trunc
+  -- Lemma 8.3.1
+  theorem trivial_homotopy_group_of_is_trunc (A : Type*) (n k : ℕ) [is_trunc n A] (H : n ≤ k)
+    : is_contr (πg[k+1] A) :=
+  begin
+    apply is_trunc_trunc_of_is_trunc,
+    apply is_contr_loop_of_is_trunc,
+    apply @is_trunc_of_le A n _,
+    rewrite [succ_sub_two_succ k],
+    exact of_nat_le_of_nat H,
+  end
+
+  -- Lemma 8.3.2
+  theorem trivial_homotopy_group_of_is_conn (A : Type*) {k n : ℕ} (H : k ≤ n) [is_conn n A]
+    : is_contr (π[k] A) :=
+  begin
+      have H2 : of_nat k ≤ of_nat n, from of_nat_le_of_nat H,
+      have H3 : is_contr (ptrunc k A),
+      begin
+        fapply is_contr_equiv_closed,
+        { apply trunc_trunc_equiv_left _ k n H2}
+      end,
+      have H4 : is_contr (Ω[k](ptrunc k A)),
+        from !is_trunc_loop_of_is_trunc,
+      apply is_trunc_equiv_closed_rev,
+      { apply equiv_of_pequiv (phomotopy_group_pequiv_loop_ptrunc k A)}
+  end
+
+  -- Corollary 8.3.3
+  open sphere.ops sphere_index
+  theorem homotopy_group_sphere_le (n k : ℕ) (H : k < n) : is_contr (π[k] (S. n)) :=
+  begin
+    cases n with n,
+    { exfalso, apply not_lt_zero, exact H},
+    { have H2 : k ≤ n, from le_of_lt_succ H,
+      apply @(trivial_homotopy_group_of_is_conn _ H2),
+      rewrite [-trunc_index.of_sphere_index_of_nat, -trunc_index.succ_sub_one], apply is_conn_sphere}
+  end
+
+end is_trunc

hott/homotopy/sphere.hlean

@@ -8,7 +8,7 @@ Declaration of the n-spheres
 
 import .susp types.trunc
 
-open eq nat susp bool is_trunc unit pointed
+open eq nat susp bool is_trunc unit pointed algebra
 
 /-
   We can define spheres with the following possible indices:
@@ -27,6 +27,17 @@ inductive sphere_index : Type₀ :=
 
 notation `ℕ₋₁` := sphere_index
 
+namespace trunc_index
+  definition sub_one [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
+  sphere_index.rec_on n -2 (λ n k, k.+1)
+  postfix `..-1`:(max+1) := sub_one
+
+  definition of_sphere_index [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
+  n..-1.+1
+
+  -- we use a double dot to distinguish with the notation .-1 in trunc_index (of type ℕ → ℕ₋₂)
+end trunc_index
+
 namespace sphere_index
   /-
      notation for sphere_index is -1, 0, 1, ...
@@ -52,8 +63,9 @@ namespace sphere_index
     (sphere_index.cases_on n -1 id)
     (sphere_index.rec n (λn' r, succ r))
 
-  protected definition le (n m : ℕ₋₁) : Type₀ :=
-  sphere_index.rec_on n (λm, unit) (λ n p m, sphere_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
+  inductive le (a : ℕ₋₁) : ℕ₋₁ → Type :=
+  | sp_refl : le a a
+  | step : Π {b}, le a b → le a (b.+1)
 
   infix `+1+`:65 := sphere_index.add_plus_one
 
@@ -63,11 +75,6 @@ namespace sphere_index
   definition has_le_sphere_index [instance] : has_le ℕ₋₁ :=
   has_le.mk sphere_index.le
 
-  definition succ_le_succ {n m : ℕ₋₁} (H : n ≤ m) : n.+1 ≤ m.+1 := proof H qed
-  definition le_of_succ_le_succ {n m : ℕ₋₁} (H : n.+1 ≤ m.+1) : n ≤ m := proof H qed
-  definition minus_two_le (n : ℕ₋₁) : -1 ≤ n := star
-  definition empty_of_succ_le_minus_two {n : ℕ₋₁} (H : n .+1 ≤ -1) : empty := H
-
   definition of_nat [coercion] [reducible] (n : nat) : ℕ₋₁ :=
   (nat.rec_on n -1 (λ n k, k.+1)).+1
 
@@ -80,17 +87,71 @@ namespace sphere_index
   definition succ_sub_one (n : ℕ) : (nat.succ n)..-1 = n :> ℕ₋₁ :=
   idp
 
-end sphere_index
-open sphere_index
+  definition succ_le_succ {n m : ℕ₋₁} (H : n ≤ m) : n.+1 ≤[ℕ₋₁] m.+1 :=
+  by induction H with m H IH; apply le.sp_refl; exact le.step IH
+
+  definition minus_one_le (n : ℕ₋₁) : -1 ≤[ℕ₋₁] n :=
+  by induction n with n IH; apply le.sp_refl; exact le.step IH
+
+  open decidable
+  protected definition has_decidable_eq [instance] : Π(n m : ℕ₋₁), decidable (n = m)
+  | has_decidable_eq -1     -1     := inl rfl
+  | has_decidable_eq (n.+1) -1     := inr (by contradiction)
+  | has_decidable_eq -1     (m.+1) := inr (by contradiction)
+  | has_decidable_eq (n.+1) (m.+1) :=
+      match has_decidable_eq n m with
+      | inl xeqy := inl (by rewrite xeqy)
+      | inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney)
+      end
+
+  definition not_succ_le_minus_two {n : sphere_index} (H : n .+1 ≤[ℕ₋₁] -1) : empty :=
+  by cases H
+
+  protected definition le_trans {n m k : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m) (H2 : m ≤[ℕ₋₁] k) : n ≤[ℕ₋₁] k :=
+  begin
+    induction H2 with k H2 IH,
+    { exact H1},
+    { exact le.step IH}
+  end
+
+  definition le_of_succ_le_succ {n m : ℕ₋₁} (H : n.+1 ≤[ℕ₋₁] m.+1) : n ≤[ℕ₋₁] m :=
+  begin
+    cases H with m H',
+    { apply le.sp_refl},
+    { exact sphere_index.le_trans (le.step !le.sp_refl) H'}
+  end
+
+  theorem not_succ_le_self {n : ℕ₋₁} : ¬n.+1 ≤[ℕ₋₁] n :=
+  begin
+    induction n with n IH: intro H,
+    { exact not_succ_le_minus_two H},
+    { exact IH (le_of_succ_le_succ H)}
+  end
+
+  protected definition le_antisymm {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m) (H2 : m ≤[ℕ₋₁] n) : n = m :=
+  begin
+    induction H2 with n H2 IH,
+    { reflexivity},
+    { exfalso, apply @not_succ_le_self n, exact sphere_index.le_trans H1 H2}
+  end
+
+  protected definition le_succ {n m : ℕ₋₁} (H1 : n ≤[ℕ₋₁] m): n ≤[ℕ₋₁] m.+1 :=
+  le.step H1
+
+  /-
+    warning: if this coercion is available, the coercion ℕ → ℕ₋₂ is the composition of the coercions
+    ℕ → ℕ₋₁ → ℕ₋₂. We don't want this composition as coercion, because it has worse computational
+    properties. You can rewrite it with trans_to_of_sphere_index_eq defined below.
+  -/
+  attribute trunc_index.of_sphere_index [coercion]
+
+
+end sphere_index open sphere_index
+
+definition weak_order_sphere_index [trans_instance] [reducible] : weak_order sphere_index :=
+weak_order.mk le sphere_index.le.sp_refl @sphere_index.le_trans @sphere_index.le_antisymm
 
 namespace trunc_index
-  definition sub_one [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
-  sphere_index.rec_on n -2 (λ n k, k.+1)
-  postfix `..-1`:(max+1) := sub_one
-
-  definition of_sphere_index [coercion] [reducible] (n : ℕ₋₁) : ℕ₋₂ :=
-  n..-1.+1
-
   definition sub_two_eq_sub_one_sub_one (n : ℕ) : n.-2 = n..-1..-1 :=
   nat.rec_on n idp (λn p, ap trunc_index.succ p)
 
@@ -98,13 +159,17 @@ namespace trunc_index
   idp
 
   definition of_sphere_index_of_nat (n : ℕ)
-    : of_sphere_index (sphere_index.of_nat n) = trunc_index.of_nat n :> ℕ₋₂ :=
+    : of_sphere_index (sphere_index.of_nat n) = of_nat n :> ℕ₋₂ :=
   begin
     induction n with n IH,
     { reflexivity},
     { exact ap trunc_index.succ IH}
   end
 
+  definition trans_to_of_sphere_index_eq (n : ℕ)
+    : trunc_index._trans_to_of_sphere_index n = of_nat n :> ℕ₋₂ :=
+  of_sphere_index_of_nat n
+
 end trunc_index
 
 open sphere_index equiv

hott/init/trunc.hlean

@@ -90,8 +90,6 @@ namespace trunc_index
 
   definition minus_two_le (n : ℕ₋₂) : -2 ≤ n :=
   by induction n with n IH; apply le.tr_refl; exact le.step IH
-  protected definition le_refl (n : ℕ₋₂) : n ≤ n :=
-  le.tr_refl n
 
 end trunc_index open trunc_index
 

hott/types/trunc.hlean

@@ -15,7 +15,7 @@ open eq sigma sigma.ops pi function equiv trunctype
 
 namespace trunc_index
 
-  definition minus_one_le_succ (n : trunc_index) : -1 ≤ n.+1 :=
+  definition minus_one_le_succ (n : ℕ₋₂) : -1 ≤ n.+1 :=
   succ_le_succ (minus_two_le n)
 
   definition zero_le_of_nat (n : ℕ) : 0 ≤ of_nat n :=
@@ -32,7 +32,7 @@ namespace trunc_index
       | inr xney := inr (λ h : succ n = succ m, by injection h with xeqy; exact absurd xeqy xney)
       end
 
-  definition not_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty :=
+  definition not_succ_le_minus_two {n : ℕ₋₂} (H : n .+1 ≤ -2) : empty :=
   by cases H
 
   protected definition le_trans {n m k : ℕ₋₂} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
@@ -42,7 +42,7 @@ namespace trunc_index
     { exact le.step IH}
   end
 
-  definition le_of_succ_le_succ {n m : trunc_index} (H : n.+1 ≤ m.+1) : n ≤ m :=
+  definition le_of_succ_le_succ {n m : ℕ₋₂} (H : n.+1 ≤ m.+1) : n ≤ m :=
   begin
     cases H with m H',
     { apply le.tr_refl},
@@ -69,7 +69,7 @@ namespace trunc_index
 end trunc_index open trunc_index
 
 definition weak_order_trunc_index [trans_instance] [reducible] : weak_order trunc_index :=
-weak_order.mk le trunc_index.le_refl @trunc_index.le_trans @trunc_index.le_antisymm
+weak_order.mk le trunc_index.le.tr_refl @trunc_index.le_trans @trunc_index.le_antisymm
 
 namespace trunc_index