feat(hott/homotopy): general connectivity elimination and the wedge connectivity lemma

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 | - | - | - | - | - | - |   |   |   |    |    |    |    |    |    |
@@ -145,8 +145,8 @@ Unless otherwise noted, the files are in the folder [homotopy](homotopy/homotopy
 - 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.4 (Fiber sequences and the long exact sequence): not formalized
-- 8.5 (The Hopf fibration): 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): 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
 - 8.7 (The van Kampen theorem): not formalized
 - 8.8 (Whitehead’s theorem and Whitehead’s principle): not formalized
 - 8.9 (A general statement of the encode-decode method): not formalized

hott/homotopy/circle.hlean

@@ -269,4 +269,30 @@ namespace circle
       induction H', reflexivity}
   end
 
+  definition circle_mul [reducible] (x y : S¹) : S¹ :=
+  begin
+    induction x,
+    { induction y,
+      { exact base },
+      { exact loop } },
+    { induction y,
+      { exact loop },
+      { apply eq_pathover, rewrite elim_loop,
+        apply square_of_eq, reflexivity } }
+  end
+
+  definition circle_mul_base (x : S¹) : circle_mul x base = x :=
+  begin
+    induction x,
+    { reflexivity },
+    { apply eq_pathover, krewrite [elim_loop,ap_id], apply hrefl }
+  end
+
+  definition circle_base_mul (x : S¹) : circle_mul base x = x :=
+  begin
+    induction x,
+    { reflexivity },
+    { apply eq_pathover, krewrite [elim_loop,ap_id], apply hrefl }
+  end
+
 end circle

hott/homotopy/connectedness.hlean

@@ -3,9 +3,9 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ulrik Buchholtz
 -/
-import types.trunc types.arrow_2 types.fiber .susp
+import types.trunc types.eq types.arrow_2 types.fiber .susp
 
-open eq is_trunc is_equiv nat equiv trunc function fiber
+open eq is_trunc is_equiv nat equiv trunc function fiber funext
 
 namespace homotopy
 
@@ -29,33 +29,73 @@ namespace homotopy
     parameters {n : trunc_index} {A B : Type} {h : A → B}
                (H : is_conn_map n h) (P : B → n -Type)
 
-    private definition helper : (Πa : A, P (h a)) → Πb : B, trunc n (fiber h b) → P b :=
+    private definition rec.helper : (Πa : A, P (h a)) → Πb : B, trunc n (fiber h b) → P b :=
     λt b, trunc.rec (λx, point_eq x ▸ t (point x))
 
-    private definition g : (Πa : A, P (h a)) → (Πb : B, P b) :=
+    private definition rec.g : (Πa : A, P (h a)) → (Πb : B, P b) :=
-    λt b, helper t b (@center (trunc n (fiber h b)) (H b))
+    λt b, rec.helper t b (@center (trunc n (fiber h b)) (H b))
 
     -- induction principle for n-connected maps (Lemma 7.5.7)
-    definition rec : is_equiv (λs : Πb : B, P b, λa : A, s (h a)) :=
+    protected definition rec : is_equiv (λs : Πb : B, P b, λa : A, s (h a)) :=
-    adjointify (λs a, s (h a)) g
+    adjointify (λs a, s (h a)) rec.g
     begin
-      intro t, apply eq_of_homotopy, intro a, unfold g, unfold helper,
+      intro t, apply eq_of_homotopy, intro a, unfold rec.g, unfold rec.helper,
       rewrite [@center_eq _ (H (h a)) (tr (fiber.mk a idp))],
     end
     begin
-      intro k, apply eq_of_homotopy, intro b, unfold g,
+      intro k, apply eq_of_homotopy, intro b, unfold rec.g,
       generalize (@center _ (H b)), apply trunc.rec, apply fiber.rec,
       intros a p, induction p, reflexivity
     end
 
-    definition elim : (Πa : A, P (h a)) → (Πb : B, P b) :=
+    protected definition elim : (Πa : A, P (h a)) → (Πb : B, P b) :=
     @is_equiv.inv _ _ (λs a, s (h a)) rec
 
-    definition elim_β : Πf : (Πa : A, P (h a)), Πa : A, elim f (h a) = f a :=
+    protected definition elim_β : Πf : (Πa : A, P (h a)), Πa : A, elim f (h a) = f a :=
     λf, apd10 (@is_equiv.right_inv _ _ (λs a, s (h a)) rec f)
 
   end
 
+  section
+    parameters {n k : trunc_index} {A B : Type} {f : A → B}
+               (H : is_conn_map n f) (P : B → (n +2+ k)-Type)
+
+    include H
+    -- Lemma 8.6.1
+    proposition elim_general (t : Πa : A, P (f a))
+      : is_trunc k (fiber (λs : (Πb : B, P b), (λa, s (f a))) t) :=
+    begin
+      induction k with k IH,
+      { apply is_contr_fiber_of_is_equiv, apply is_conn_map.rec, exact H },
+      { apply is_trunc_succ_intro,
+        intros x y, cases x with g p, cases y with h q,
+        assert e : fiber (λr : g ~ h, (λa, r (f a))) (apd10 (p ⬝ q⁻¹))
+                 ≃ (fiber.mk g p = fiber.mk h q
+                     :> fiber (λs : (Πb, P b), (λa, s (f a))) t),
+        { apply equiv.trans !fiber.sigma_char,
+          assert e' : Πr : g ~ h,
+                 ((λa, r (f a)) = apd10 (p ⬝ q⁻¹))
+               ≃ (ap (λv, (λa, v (f a))) (eq_of_homotopy r) ⬝ q = p),
+          { intro r,
+            refine equiv.trans _ (eq_con_inv_equiv_con_eq q p
+                                   (ap (λv a, v (f a)) (eq_of_homotopy r))),
+            rewrite [-(ap (λv a, v (f a)) (apd10_eq_of_homotopy r))],
+            rewrite [-(apd10_ap_precompose_dependent f (eq_of_homotopy r))],
+            apply equiv.symm,
+            apply eq_equiv_fn_eq (@apd10 A (λa, P (f a)) (λa, g (f a)) (λa, h (f a))) },
+          apply equiv.trans (sigma.sigma_equiv_sigma_id e'), clear e',
+          apply equiv.trans (equiv.symm (sigma.sigma_equiv_sigma_left
+                                           eq_equiv_homotopy)),
+          apply equiv.symm, apply equiv.trans !fiber_eq_equiv,
+          apply sigma.sigma_equiv_sigma_id, intro r,
+          apply eq_equiv_eq_symm },
+        apply @is_trunc_equiv_closed _ _ k e, clear e,
+        apply IH (λb : B, trunctype.mk (g b = h b)
+                           (@is_trunc_eq (P b) (n +2+ k) (trunctype.struct (P b))
+                           (g b) (h b))) }
+    end
+  end
+
   section
     universe variables u v
     parameters {n : trunc_index} {A : Type.{u}} {B : Type.{v}} {h : A → B}
@@ -113,6 +153,44 @@ namespace homotopy
 
   end
 
+  -- as special case we get elimination principles for pointed connected types
+  namespace is_conn
+    open pointed Pointed unit
+    section
+      parameters {n : trunc_index} {A : Type*}
+                 [H : is_conn n .+1 A] (P : A → n -Type)
+
+      include H
+      protected definition rec : is_equiv (λs : Πa : A, P a, s (Point A)) :=
+      @is_equiv_compose
+        (Πa : A, P a) (unit → P (Point A)) (P (Point A))
+        (λs x, s (Point A)) (λf, f unit.star)
+        (is_conn_map.rec (is_conn_map_from_unit n A (Point A)) P)
+        (to_is_equiv (unit.unit_imp_equiv (P (Point A))))
+
+      protected definition elim : P (Point A) → (Πa : A, P a) :=
+      @is_equiv.inv _ _ (λs, s (Point A)) rec
+
+      protected definition elim_β (p : P (Point A)) : elim p (Point A) = p :=
+      @is_equiv.right_inv _ _ (λs, s (Point A)) rec p
+    end
+
+    section
+      parameters {n k : trunc_index} {A : Type*}
+                 [H : is_conn n .+1 A] (P : A → (n +2+ k)-Type)
+
+      include H
+      proposition elim_general (p : P (Point A))
+        : is_trunc k (fiber (λs : (Πa : A, P a), s (Point A)) p) :=
+      @is_trunc_equiv_closed
+        (fiber (λs x, s (Point A)) (λx, p))
+        (fiber (λs, s (Point A)) p)
+        k
+        (equiv.symm (fiber.equiv_postcompose (to_fun (unit.unit_imp_equiv (P (Point A))))))
+        (is_conn_map.elim_general (is_conn_map_from_unit n A (Point A)) P (λx, p))
+    end
+  end is_conn
+
   -- Lemma 7.5.2
   definition minus_one_conn_of_surjective {A B : Type} (f : A → B)
     : is_surjective f → is_conn_map -1 f :=

hott/homotopy/wedge.hlean

@@ -1,22 +1,19 @@
 /-
 Copyright (c) 2016 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jakob von Raumer
+Authors: Jakob von Raumer, Ulrik Buchholtz
 
 The Wedge Sum of Two Pointed Types
 -/
-import hit.pointed_pushout
+import hit.pointed_pushout .connectedness
 
 open eq pushout pointed Pointed
 
+definition Wedge (A B : Type*) : Type* := Pushout (pconst Unit A) (pconst Unit B)
+
 namespace wedge
-  section
-  variables (A B : Type*)
-
-  definition Wedge : Type* := Pushout (pconst Unit A) (pconst Unit B)
-
   -- TODO maybe find a cleaner proof
-  protected definition unit : A ≃* Wedge Unit A :=
+  protected definition unit (A : Type*) : A ≃* Wedge Unit A :=
   begin
     fconstructor,
     { fapply pmap.mk, intro a, apply pinr a, apply respect_pt },
@@ -30,6 +27,52 @@ namespace wedge
       apply con.left_inv, 
       intro a, reflexivity },
   end
-
-  end
 end wedge
+
+open trunc is_trunc function homotopy
+namespace wedge_extension
+section
+  -- The wedge connectivity lemma (Lemma 8.6.2)
+  parameters {A B : Type*} (n m : trunc_index)
+             [cA : is_conn n .+2 A] [cB : is_conn m .+2 B]
+             (P : A → B → (m .+1 +2+ n .+1)-Type)
+             (f : Πa : A, P a (Point B))
+             (g : Πb : B, P (Point A) b)
+             (p : f (Point A) = g (Point B))
+
+  include cA cB
+  private definition Q (a : A) : (n .+1)-Type :=
+  trunctype.mk
+    (fiber (λs : (Πb : B, P a b), s (Point B)) (f a))
+    (is_conn.elim_general (P a) (f a))
+
+  private definition Q_sec : Πa : A, Q a :=
+  is_conn.elim Q (fiber.mk g p⁻¹)
+
+  protected definition ext : Π(a : A)(b : B), P a b :=
+  λa, fiber.point (Q_sec a)
+
+  protected definition β_left (a : A) : ext a (Point B) = f a :=
+  fiber.point_eq (Q_sec a)
+
+  private definition coh_aux : Σq : ext (Point A) = g,
+    β_left (Point A) = ap (λs : (Πb : B, P (Point A) b), s (Point B)) q ⬝ p⁻¹ :=
+  equiv.to_fun (fiber.fiber_eq_equiv (Q_sec (Point A)) (fiber.mk g p⁻¹))
+               (is_conn.elim_β Q (fiber.mk g p⁻¹))
+
+  protected definition β_right (b : B) : ext (Point A) b = g b :=
+  apd10 (sigma.pr1 coh_aux) b
+
+  private definition lem : β_left (Point A) = β_right (Point B) ⬝ p⁻¹ :=
+  begin
+    unfold β_right, unfold β_left,
+    krewrite (apd10_eq_ap_eval (sigma.pr1 coh_aux) (Point B)),
+    exact sigma.pr2 coh_aux,
+  end
+
+  protected definition coh
+    : (β_left (Point A))⁻¹ ⬝ β_right (Point B) = p :=
+  by rewrite [lem,con_inv,inv_inv,con.assoc,con.left_inv]
+
+end
+end wedge_extension

hott/init/path.hlean

@@ -233,6 +233,11 @@ namespace eq
   definition apd10' [unfold 6] {f g : Πx, P x} (a : A) (H : f = g) : f a = g a :=
   eq.rec_on H idp
 
+  --apd10 is also ap evaluation
+  definition apd10_eq_ap_eval {f g : Πx, P x} (H : f = g) (a : A)
+    : apd10 H a = ap (λs : Πx, P x, s a) H :=
+  eq.rec_on H idp
+
   definition ap10 [reducible] [unfold 5] {f g : A → B} (H : f = g) : f ~ g := apd10 H
 
   definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
@@ -525,12 +530,17 @@ namespace eq
     ap (λh, h ∘ f) p = transport (λh : B → C, g ∘ f = h ∘ f) p idp :=
   eq.rec_on p idp
 
-  definition apd10_ap_precompose (f : A → B) (g g' : B → C) (p : g = g') (a : A) :
+  definition apd10_ap_precompose (f : A → B) (g g' : B → C) (p : g = g') :
-    apd10 (ap (λh : B → C, h ∘ f) p) a = apd10 p (f a) :=
+    apd10 (ap (λh : B → C, h ∘ f) p) = λa, apd10 p (f a) :=
   eq.rec_on p idp
 
-  definition apd10_ap_postcompose (f : B → C) (g g' : A → B) (p : g = g') (a : A) :
+  definition apd10_ap_precompose_dependent {C : B → Type}
-    apd10 (ap (λh : A → B, f ∘ h) p) a = ap f (apd10 p a) :=
+    (f : A → B) {g g' : Πb : B, C b} (p : g = g')
+    : apd10 (ap (λ(h : (Πb : B, C b))(a : A), h (f a)) p) = λa, apd10 p (f a) :=
+  eq.rec_on p idp
+
+  definition apd10_ap_postcompose (f : B → C) (g g' : A → B) (p : g = g') :
+    apd10 (ap (λh : A → B, f ∘ h) p) = λa, ap f (apd10 p a) :=
   eq.rec_on p idp
 
   -- A special case of [tr_compose] which seems to come up a lot.

hott/types/fiber.hlean

@@ -68,8 +68,31 @@ namespace fiber
 
   definition is_trunc_fun [reducible] (n : trunc_index) (f : A → B) :=
   Π(b : B), is_trunc n (fiber f b)
+
   definition is_contr_fun [reducible] (f : A → B) := is_trunc_fun -2 f
 
+  -- pre and post composition with equivalences
+  open function
+  protected definition equiv_postcompose {B' : Type} (g : B → B') [H : is_equiv g]
+    : fiber (g ∘ f) (g b) ≃ fiber f b :=
+  calc
+    fiber (g ∘ f) (g b) ≃ Σa : A, g (f a) = g b : fiber.sigma_char
+                    ... ≃ Σa : A, f a = b       : begin
+                                                    apply sigma_equiv_sigma_id, intro a,
+                                                    apply equiv.symm, apply eq_equiv_fn_eq
+                                                  end
+                    ... ≃ fiber f b             : fiber.sigma_char
+
+  protected definition equiv_precompose {A' : Type} (g : A' → A) [H : is_equiv g]
+    : fiber (f ∘ g) b ≃ fiber f b :=
+  calc
+    fiber (f ∘ g) b ≃ Σa' : A', f (g a') = b   : fiber.sigma_char
+                ... ≃ Σa : A, f a = b          : begin
+                                                   apply sigma_equiv_sigma (equiv.mk g H),
+                                                   intro a', apply erfl
+                                                 end
+                ... ≃ fiber f b                : fiber.sigma_char
+
 end fiber
 
 open unit is_trunc