EM: add functorial action and equivalence of 1-Type*[0] and Group

n-Type*[k] is new notation for n-truncated k-connected pointed types. All 'subnotations' are also defined

homotopy/EM.hlean

@@ -14,6 +14,46 @@ open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra
 
 namespace EM
 
+  /- Functorial action of Eilenberg-Maclane spaces -/
+
+  definition pEM1_functor [constructor] {G H : Group} (φ : G →g H) : pEM1 G →* pEM1 H :=
+  begin
+    fconstructor,
+    { intro g, induction g,
+      { exact base },
+      { exact pth (φ g) },
+      { exact ap pth (respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }},
+    { reflexivity }
+  end
+
+  definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) :
+    EMadd1 G n →* EMadd1 H n :=
+  begin
+    apply ptrunc_functor,
+    apply iterate_psusp_functor,
+    apply pEM1_functor,
+    exact φ
+  end
+
+  definition EM_functor {G H : CommGroup} (φ : G →g H) (n : ℕ) :
+    K G n →* K H n :=
+  begin
+    cases n with n,
+    { exact pmap_of_homomorphism φ },
+    { exact EMadd1_functor φ n }
+  end
+
+  /- Equivalence of Groups and pointed connected 1-truncated types -/
+
+  definition pEM1_pequiv_ptruncconntype (X : 1-Type*[0]) : pEM1 (π₁ X) ≃* X :=
+  pEM1_pequiv_type
+
+  definition Group_equiv_ptruncconntype [constructor] : Group ≃ 1-Type*[0] :=
+  equiv.MK (λG, ptruncconntype.mk (pEM1 G) _ pt !is_conn_pEM1)
+           (λX, π₁ X)
+           begin intro X, apply ptruncconntype_eq, esimp, exact pEM1_pequiv_type end
+           begin intro G, apply eq_of_isomorphism, apply fundamental_group_pEM1 end
+
   /- Higher EM-spaces -/
 
   /- K(G, 2) is unique (see below for general case) -/

move_to_lib.hlean

@@ -3,6 +3,7 @@
 import homotopy.sphere2
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
+     is_trunc
 
 attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in isomorphism_of_eq [constructor]
 attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
@@ -236,3 +237,95 @@ namespace eq --algebra.homotopy_group
   ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid
 
 end eq
+
+namespace susp
+
+  definition iterate_psusp_functor (n : ℕ) {A B : Type*} (f : A →* B) :
+    iterate_psusp n A →* iterate_psusp n B :=
+  begin
+    induction n with n g,
+    { exact f },
+    { exact psusp_functor g }
+  end
+
+end susp
+
+namespace is_conn -- homotopy.connectedness
+
+  structure conntype (n : ℕ₋₂) : Type :=
+    (carrier : Type)
+    (struct : is_conn n carrier)
+
+  notation `Type[`:95  n:0 `]`:0 := conntype n
+
+  attribute conntype.carrier [coercion]
+  attribute conntype.struct [instance] [priority 1300]
+
+  section
+    universe variable u
+    structure pconntype (n : ℕ₋₂) extends conntype.{u} n, pType.{u}
+
+    notation `Type*[`:95  n:0 `]`:0 := pconntype n
+
+    /-
+      There are multiple coercions from pconntype to Type. Type class inference doesn't recognize
+      that all of them are definitionally equal (for performance reasons). One instance is
+      automatically generated, and we manually add the missing instances.
+    -/
+
+    definition is_conn_pconntype [instance] {n : ℕ₋₂} (X : Type*[n]) : is_conn n X :=
+    conntype.struct X
+
+    /- Now all the instances work -/
+    example {n : ℕ₋₂} (X : Type*[n]) : is_conn n X := _
+    example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_pType X) := _
+    example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype.to_conntype X) := _
+    example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_pType X) := _
+    example {n : ℕ₋₂} (X : Type*[n]) : is_conn n (pconntype._trans_of_to_conntype X) := _
+
+    structure truncconntype (n k : ℕ₋₂) extends trunctype.{u} n,
+                                                conntype.{u} k renaming struct→conn_struct
+
+    notation n `-Type[`:95  k:0 `]`:0 := truncconntype n k
+
+    definition is_conn_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) :
+      is_conn k (truncconntype._trans_of_to_trunctype X) :=
+    conntype.struct X
+
+    definition is_trunc_truncconntype [instance] {n k : ℕ₋₂} (X : n-Type[k]) : is_trunc n X :=
+    trunctype.struct X
+
+    structure ptruncconntype (n k : ℕ₋₂) extends ptrunctype.{u} n,
+                                                 pconntype.{u} k renaming struct→conn_struct
+
+    notation n `-Type*[`:95  k:0 `]`:0 := ptruncconntype n k
+
+    attribute ptruncconntype._trans_of_to_pconntype ptruncconntype._trans_of_to_ptrunctype
+              ptruncconntype._trans_of_to_pconntype_1 ptruncconntype._trans_of_to_ptrunctype_1
+              ptruncconntype._trans_of_to_pconntype_2 ptruncconntype._trans_of_to_ptrunctype_2
+              ptruncconntype.to_pconntype ptruncconntype.to_ptrunctype
+              truncconntype._trans_of_to_conntype truncconntype._trans_of_to_trunctype
+              truncconntype.to_conntype truncconntype.to_trunctype [unfold 3]
+    attribute pconntype._trans_of_to_conntype pconntype._trans_of_to_pType
+              pconntype.to_pType pconntype.to_conntype [unfold 2]
+
+    definition is_conn_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) :
+      is_conn k (ptruncconntype._trans_of_to_ptrunctype X) :=
+    conntype.struct X
+
+    definition is_trunc_ptruncconntype [instance] {n k : ℕ₋₂} (X : n-Type*[k]) :
+      is_trunc n (ptruncconntype._trans_of_to_pconntype X) :=
+    trunctype.struct X
+
+    definition ptruncconntype_eq {n k : ℕ₋₂} {X Y : n-Type*[k]} (p : X ≃* Y) : X = Y :=
+    begin
+      induction X with X Xt Xp Xc, induction Y with Y Yt Yp Yc,
+      note q := pType_eq_elim (eq_of_pequiv p),
+      cases q with r s, esimp at *, induction r,
+      exact ap0111 (ptruncconntype.mk X) !is_prop.elim (eq_of_pathover_idp s) !is_prop.elim
+    end
+
+  end
+
+
+end is_conn