feat(EM): Prove some corollaries of Whitehead's principle, and prove that K(G,1) is unique.

Also reorder the arguments of is_equiv_compose

hott/algebra/homotopy_group.hlean

@@ -69,14 +69,19 @@ namespace eq
     exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end)
   end
 
+  open trunc_index
+  definition phomotopy_group_ptrunc_of_le [constructor] {k n : ℕ} (H : k ≤ n) (A : Type*) :
+    π*[k] (ptrunc n A) ≃* π*[k] A :=
+  calc
+    π*[k] (ptrunc n A) ≃* Ω[k] (ptrunc k (ptrunc n A))
+             : phomotopy_group_pequiv_loop_ptrunc k (ptrunc n A)
+      ... ≃* Ω[k] (ptrunc k A)
+             : loopn_pequiv_loopn k (ptrunc_ptrunc_pequiv_left A (of_nat_le_of_nat H))
+      ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
+
   definition phomotopy_group_ptrunc [constructor] (k : ℕ) (A : Type*) :
     π*[k] (ptrunc k A) ≃* π*[k] A :=
-  calc
-    π*[k] (ptrunc k A) ≃* Ω[k] (ptrunc k (ptrunc k A))
-             : phomotopy_group_pequiv_loop_ptrunc k (ptrunc k A)
-      ... ≃* Ω[k] (ptrunc k A)
-             : loopn_pequiv_loopn k (ptrunc_pequiv k (ptrunc k A) _)
-      ... ≃* π*[k] A : (phomotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
+  phomotopy_group_ptrunc_of_le (le.refl k) A
 
   theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 :=
   begin
@@ -149,7 +154,7 @@ namespace eq
   definition is_equiv_phomotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B)
     [is_equiv (π→*[n + 1] f)] : is_equiv (π→*[n] (Ω→ f)) :=
   have is_equiv (pcast (phomotopy_group_succ_in B n) ∘* π→*[n + 1] f),
-  begin apply @(is_equiv_compose (π→*[n + 1] f) _) end,
+  from is_equiv_compose _ (π→*[n + 1] f),
   have is_equiv (π→*[n] (Ω→ f) ∘ pcast (phomotopy_group_succ_in A n)),
   from is_equiv.homotopy_closed _ (phomotopy_group_functor_succ_phomotopy_in n f),
   is_equiv.cancel_right (pcast (phomotopy_group_succ_in A n)) _

hott/hit/groupoid_quotient.hlean

@@ -243,3 +243,5 @@ section
 end
 
 end groupoid_quotient
+
+export [unfold] groupoid_quotient

hott/homotopy/EM.hlean

@@ -9,6 +9,7 @@ Eilenberg MacLane spaces
 
 import hit.groupoid_quotient .hopf .freudenthal .homotopy_group
 open algebra pointed nat eq category group algebra is_trunc iso pointed unit trunc equiv is_conn
+     function is_equiv
 
 namespace EM
   open groupoid_quotient
@@ -150,7 +151,7 @@ namespace EM
       { exact abstract begin apply loop_pathover, apply square_of_eq,
           refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul,
           exact ap pth !mul.comm end end}},
-    { refine EM.prop_rec _ x', esimp, apply resp_mul},
+    { refine EM.prop_rec _ x', apply resp_mul}
   end
 
   definition EM1_mul_one (G : CommGroup) (x : EM1 G) : EM1_mul x base = x :=
@@ -235,6 +236,52 @@ namespace EM
     { apply is_trunc_EMadd1}
   end
 
+  /- Uniqueness of K(G, 1) -/
+  definition pEM1_pmap [constructor] {G : Group} {X : Type*} (e : Ω X ≃ G)
+    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G →* X :=
+  begin
+    apply pmap.mk (EM1_map e r),
+    reflexivity,
+  end
 
+  definition loop_pEM1 [constructor] (G : Group) : Ω (pEM1 G) ≃* pType_of_Group G :=
+  pequiv_of_equiv (base_eq_base_equiv G) idp
+
+  definition loop_pEM1_pmap {G : Group} {X : Type*} (e : Ω X ≃ G)
+    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] :
+    Ω→(pEM1_pmap e r) ~ e⁻¹ᵉ ∘ base_eq_base_equiv G :=
+  begin
+    apply homotopy_of_inv_homotopy_pre (base_eq_base_equiv G),
+    intro g, exact !idp_con ⬝ !elim_pth
+  end
+
+  open trunc_index
+  definition pEM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : Ω X ≃ G)
+    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
+  begin
+    apply pequiv_of_pmap (pEM1_pmap e r),
+    apply whitehead_principle_pointed 1,
+    intro k, cases k with k,
+    { apply @is_equiv_of_is_contr,
+      all_goals (esimp; exact _)},
+    { cases k with k,
+      { apply is_equiv_trunc_functor, esimp,
+        apply is_equiv.homotopy_closed, rotate 1,
+        { symmetry, exact loop_pEM1_pmap _ _},
+        apply is_equiv_compose, apply to_is_equiv},
+      { apply @is_equiv_of_is_contr,
+        do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}}
+  end
+
+  definition pEM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
+    [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
+  begin
+    apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
+    intro p q, esimp, exact respect_mul e (tr p) (tr q)
+  end
+
+  definition KG1_pequiv.{u} {X Y : pType.{u}} (e : π₁ X ≃g π₁ Y)
+    [is_conn 0 X] [is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] : X ≃* Y :=
+  (pEM1_pequiv e)⁻¹ᵉ* ⬝e* pEM1_pequiv !isomorphism.refl
 
 end EM

hott/homotopy/chain_complex.hlean

@@ -517,6 +517,19 @@ namespace chain_complex
     { apply is_surjective_of_trivial X, apply H1},
   end
 
+  definition is_contr_of_is_embedding_of_is_surjective {N : succ_str} (X : chain_complex N) {n : N}
+    (H : is_exact_at X (S n)) [is_embedding (cc_to_fn X n)]
+    [H2 : is_surjective (cc_to_fn X (S (S (S n))))] : is_contr (X (S (S n))) :=
+  begin
+    apply is_contr.mk pt, intro x,
+    have p : cc_to_fn X n (cc_to_fn X (S n) x) = cc_to_fn X n pt,
+      from !cc_is_chain_complex ⬝ !respect_pt⁻¹,
+    have q : cc_to_fn X (S n) x = pt, from is_injective_of_is_embedding p,
+    induction H x q with y r,
+    induction H2 y with z s,
+    exact (cc_is_chain_complex X _ z)⁻¹ ⬝ ap (cc_to_fn X _) s ⬝ r
+  end
+
   end
 
 end chain_complex

hott/homotopy/connectedness.hlean

@@ -145,6 +145,13 @@ namespace is_conn
       exact is_conn_equiv_closed n (fiber.fiber_star_equiv A) _,
     end
 
+    definition is_conn_fun_to_unit_of_is_conn [H : is_conn n A] :
+      is_conn_fun n (const A unit.star) :=
+    begin
+      intro u, induction u,
+      exact is_conn_equiv_closed n (fiber.fiber_star_equiv A)⁻¹ᵉ _,
+    end
+
     -- now maps from unit
     definition is_conn_of_map_from_unit (a₀ : A) (H : is_conn_fun n (const unit a₀))
       : is_conn n .+1 A :=
@@ -176,7 +183,7 @@ namespace is_conn
       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)
+        (λf, f unit.star) (λs x, s (Point A))
         (is_conn_fun.rec n (is_conn_fun_from_unit n A (Point A)) P)
         (to_is_equiv (arrow_unit_left (P (Point A))))
 

hott/homotopy/homotopy_group.hlean

@@ -7,20 +7,26 @@ Authors: Floris van Doorn, Clive Newstead
 
 import .LES_of_homotopy_groups .sphere .complex_hopf
 
-open eq is_trunc trunc_index pointed algebra trunc nat is_conn fiber pointed
+open eq is_trunc trunc_index pointed algebra trunc nat is_conn fiber pointed unit
 
 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) :=
+  theorem trivial_homotopy_group_of_is_trunc (A : Type*) {n k : ℕ} [is_trunc n A] (H : n < k)
+    : is_contr (π[k] A) :=
   begin
     apply is_trunc_trunc_of_is_trunc,
     apply is_contr_loop_of_is_trunc,
     apply @is_trunc_of_le A n _,
+    apply trunc_index.le_of_succ_le_succ,
     rewrite [succ_sub_two_succ k],
     exact of_nat_le_of_nat H,
   end
 
+  theorem trivial_ghomotopy_group_of_is_trunc (A : Type*) (n k : ℕ) [is_trunc n A] (H : n ≤ k)
+    : is_contr (πg[k+1] A) :=
+  trivial_homotopy_group_of_is_trunc A (lt_succ_of_le H)
+
   -- 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) :=
@@ -109,9 +115,9 @@ namespace is_trunc
     (@is_contr_HG_fiber_of_is_connected A B n n f H !le.refl)
 
   /-
-    Theorem 8.8.3: Whitehead's principle
+    Theorem 8.8.3: Whitehead's principle and its corollaries
   -/
-  definition whiteheads_principle (n : ℕ₋₂) {A B : Type}
+  definition whitehead_principle (n : ℕ₋₂) {A B : Type}
     [HA : is_trunc n A] [HB : is_trunc n B] (f : A → B) (H' : is_equiv (trunc_functor 0 f))
     (H : Πa k, is_equiv (π→*[k + 1] (pmap_of_map f a))) : is_equiv f :=
   begin
@@ -148,4 +154,93 @@ namespace is_trunc
     apply is_equiv_of_is_equiv_ap1_of_is_equiv_trunc
   end
 
+  definition whitehead_principle_pointed (n : ℕ₋₂) {A B : Type*}
+    [HA : is_trunc n A] [HB : is_trunc n B] [is_conn 0 A] (f : A →* B)
+    (H : Πk, is_equiv (π→*[k] f)) : is_equiv f :=
+  begin
+    apply whitehead_principle n, rexact H 0,
+    intro a k, revert a, apply is_conn.elim -1,
+    have is_equiv (π→*[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)
+           ∘* π→*[k + 1] f ∘* π→*[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
+    begin
+      apply is_equiv_compose
+              (π→*[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)),
+      apply is_equiv_compose (π→*[k + 1] f),
+      all_goals apply is_equiv_homotopy_group_functor,
+    end,
+    refine @(is_equiv.homotopy_closed _) _ this _,
+    apply to_homotopy,
+    refine pwhisker_left _ !phomotopy_group_functor_compose⁻¹* ⬝* _,
+    refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
+    apply phomotopy_group_functor_phomotopy, apply phomotopy_pmap_of_map
+  end
+
+  open pointed.ops
+  definition is_contr_of_trivial_homotopy (n : ℕ₋₂) (A : Type) [is_trunc n A] [is_conn 0 A]
+    (H : Πk a, is_contr (π[k] (pointed.MK A a))) : is_contr A :=
+  begin
+    fapply is_trunc_is_equiv_closed_rev, { exact λa, ⋆},
+    apply whitehead_principle n,
+    { apply is_equiv_trunc_functor_of_is_conn_fun, apply is_conn_fun_to_unit_of_is_conn},
+    intro a k,
+    apply @is_equiv_of_is_contr,
+    refine trivial_homotopy_group_of_is_trunc _ !zero_lt_succ,
+  end
+
+  definition is_contr_of_trivial_homotopy_nat (n : ℕ) (A : Type) [is_trunc n A] [is_conn 0 A]
+    (H : Πk a, k ≤ n → is_contr (π[k] (pointed.MK A a))) : is_contr A :=
+  begin
+    apply is_contr_of_trivial_homotopy n,
+    intro k a, apply @lt_ge_by_cases _ _ n k,
+    { intro H', exact trivial_homotopy_group_of_is_trunc _ H'},
+    { intro H', exact H k a H'}
+  end
+
+  definition is_contr_of_trivial_homotopy_pointed (n : ℕ₋₂) (A : Type*) [is_trunc n A]
+    (H : Πk, is_contr (π[k] A)) : is_contr A :=
+  begin
+    have is_conn 0 A, proof H 0 qed,
+    fapply is_contr_of_trivial_homotopy n A,
+    intro k, apply is_conn.elim -1,
+    cases A with A a, exact H k
+  end
+
+  definition is_contr_of_trivial_homotopy_nat_pointed (n : ℕ) (A : Type*) [is_trunc n A]
+    (H : Πk, k ≤ n → is_contr (π[k] A)) : is_contr A :=
+  begin
+    have is_conn 0 A, proof H 0 !zero_le qed,
+    fapply is_contr_of_trivial_homotopy_nat n A,
+    intro k a H', revert a, apply is_conn.elim -1,
+    cases A with A a, exact H k H'
+  end
+
+  definition is_conn_fun_of_equiv_on_homotopy_groups.{u} (n : ℕ) {A B : Type.{u}} (f : A → B)
+    [is_equiv (trunc_functor 0 f)]
+    (H1 : Πa k, k ≤ n → is_equiv (homotopy_group_functor k (pmap_of_map f a)))
+    (H2 : Πa, is_surjective (homotopy_group_functor (succ n) (pmap_of_map f a))) : is_conn_fun n f :=
+  have H2' : Πa k, k ≤ n → is_surjective (homotopy_group_functor (succ k) (pmap_of_map f a)),
+  begin
+    intro a k H, cases H with n' H',
+    { apply H2},
+    { apply is_surjective_of_is_equiv, apply H1, exact succ_le_succ H'}
+  end,
+  have H3 : Πa, is_contr (ptrunc n (pfiber (pmap_of_map f a))),
+  begin
+    intro a, apply is_contr_of_trivial_homotopy_nat_pointed n,
+    { intro k H, apply is_trunc_equiv_closed_rev, exact phomotopy_group_ptrunc_of_le H _,
+      rexact @is_contr_of_is_embedding_of_is_surjective +3ℕ
+               (LES_of_homotopy_groups (pmap_of_map f a)) (k, 0)
+               (is_exact_LES_of_homotopy_groups _ _)
+               proof @(is_embedding_of_is_equiv _)  (H1 a k H) qed
+               proof (H2' a k H) qed}
+  end,
+  show Πb, is_contr (trunc n (fiber f b)),
+  begin
+    intro b,
+    note p := right_inv (trunc_functor 0 f) (tr b), revert p,
+    induction (trunc_functor 0 f)⁻¹ (tr b), esimp, intro p,
+    induction !tr_eq_tr_equiv p with q,
+    rewrite -q, exact H3 a
+  end
+
 end is_trunc

hott/homotopy/sphere2.hlean

@@ -65,11 +65,11 @@ namespace sphere
         _,
         { rewrite [▸*, LES_of_homotopy_groups_2 _ (n +[ℕ] 2)],
           have H : 1 ≤[ℕ] n + 1, from !one_le_succ,
-          apply trivial_homotopy_group_of_is_trunc _ _ _ H},
+          apply trivial_ghomotopy_group_of_is_trunc _ _ _ H},
         { refine tr_rev (λx, is_contr (ptrunctype._trans_of_to_pType x))
                         (LES_of_homotopy_groups_2 complex_phopf _) _,
           have H : 1 ≤[ℕ] n + 2, from !one_le_succ,
-          apply trivial_homotopy_group_of_is_trunc _ _ _ H},
+          apply trivial_ghomotopy_group_of_is_trunc _ _ _ H},
         { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}}},
     { exact homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun _ (n+2, 0))}
   end
@@ -96,7 +96,7 @@ namespace sphere
   theorem not_is_trunc_sphere (n : ℕ) : ¬is_trunc n (S. (succ n)) :=
   begin
     intro H,
-    note H2 := trivial_homotopy_group_of_is_trunc (S. (succ n)) n n !le.refl,
+    note H2 := trivial_ghomotopy_group_of_is_trunc (S. (succ n)) n n !le.refl,
     have H3 : is_contr ℤ, from is_trunc_equiv_closed _ (equiv_of_isomorphism (πnSn n)),
     have H4 : (0 : ℤ) ≠ (1 : ℤ), from dec_star,
     apply H4,

hott/init/equiv.hlean

@@ -35,7 +35,7 @@ namespace is_equiv
   postfix [parsing_only] `⁻¹ᶠ`:std.prec.max_plus := inv
 
   section
-  variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
+  variables {A B C : Type} (g : B → C) (f : A → B) {f' : A → B}
 
   -- The variant of mk' where f is explicit.
   protected abbreviation mk [constructor] := @is_equiv.mk' A B f
@@ -134,11 +134,11 @@ namespace is_equiv
   -- The 2-out-of-3 properties
   definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
   have Hfinv : is_equiv f⁻¹, from is_equiv_inv f,
-  @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@right_inv _ _ f _ b))
+  @homotopy_closed _ _ _ _ (is_equiv_compose (g ∘ f) f⁻¹) (λb, ap g (@right_inv _ _ f _ b))
 
   definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) :=
   have Hfinv : is_equiv f⁻¹, from is_equiv_inv f,
-  @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, left_inv f (g a))
+  @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (f ∘ g)) (λa, left_inv f (g a))
 
   definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y :=
   (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y

hott/types/arrow_2.hlean

@@ -171,11 +171,9 @@ namespace arrow
     : is_equiv (inv_commute_of_commute f f' α β) :=
   begin
     unfold inv_commute_of_commute,
-    apply @is_equiv_compose _ _ _
-      (homotopy.symm ∘ (inv_homotopy_of_homotopy_pre f (f' ∘ α) β))
-      (inv_homotopy_of_homotopy_post f' (α ∘ f⁻¹) β),
-    { apply @is_equiv_compose _ _ _
-            (inv_homotopy_of_homotopy_pre f (f' ∘ α) β) homotopy.symm,
+    apply @is_equiv_compose _ _ _ (inv_homotopy_of_homotopy_post f' (α ∘ f⁻¹) β)
+      (homotopy.symm ∘ (inv_homotopy_of_homotopy_pre f (f' ∘ α) β)),
+    { apply @is_equiv_compose _ _ _ homotopy.symm (inv_homotopy_of_homotopy_pre f (f' ∘ α) β),
       { apply inv_homotopy_of_homotopy_pre.is_equiv },
       { apply pi.is_equiv_homotopy_symm }
     },

hott/types/pointed.hlean

@@ -29,6 +29,13 @@ namespace pointed
   notation `Ω` := ploop_space
   notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A
 
+  namespace ops
+    -- this is in a separate namespace because it caused type class inference to loop in some places
+    definition is_trunc_pointed_MK [instance] [priority 1100] (n : ℕ₋₂) {A : Type} (a : A)
+      [H : is_trunc n A] : is_trunc n (pointed.MK A a) :=
+    H
+  end ops
+
   definition is_trunc_loop [instance] [priority 1100] (A : Type*)
     (n : ℕ₋₂) [H : is_trunc (n.+1) A] : is_trunc n (Ω A) :=
   !is_trunc_eq
@@ -776,6 +783,21 @@ namespace pointed
     pointed.MK A a ≃* pointed.MK A a' :=
   pequiv_of_pmap (pmap_of_eq_pt p) !is_equiv_id
 
+  definition pointed_eta_pequiv [constructor] (A : Type*) : A ≃* pointed.MK A pt :=
+  pequiv.mk id !is_equiv_id idp
+
+  /- every pointed map is homotopic to one of the form `pmap_of_map _ _`, up to some
+     pointed equivalences -/
+  definition phomotopy_pmap_of_map {A B : Type*} (f : A →* B) :
+    (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*) ∘* f ∘*
+      (pointed_eta_pequiv A)⁻¹ᵉ* ~* pmap_of_map f pt :=
+  begin
+    fapply phomotopy.mk,
+    { reflexivity},
+    { esimp [pequiv.trans, pequiv.symm],
+      exact !con.right_inv⁻¹ ⬝ ((!idp_con⁻¹ ⬝ !ap_id⁻¹) ◾ (!ap_id⁻¹⁻² ⬝ !idp_con⁻¹)), }
+  end
+
 /- -- TODO
   definition pmap_pequiv_pmap {A A' B B' : Type*} (f : A ≃* A') (g : B ≃* B') :
     ppmap A B ≃* ppmap A' B' :=