define deloopable types, define cup product

The cup product on Eilenberg Maclane spaces is now defined, but no properties are proven yet

algebra/arrow_group.hlean

@@ -38,6 +38,7 @@ namespace group
       { intro a, exact con.left_inv (f a) },
       { exact !con_left_inv_idp }},
   end
+  -- inf_pgroup_pequiv_closed (loop_pppi_pequiv B) _
 
   definition inf_group_ppi [constructor] {A : Type*} (B : A → Type*) : inf_group (Π*a, Ω (B a)) :=
   @inf_group_of_inf_pgroup _ (inf_pgroup_pppi B)
@@ -128,6 +129,10 @@ namespace group
     gtrunc (gloop (Π*(a : A), B a)) ≃g gtrunc (gppi_loop B) :=
   proof trunc_ppi_loop_isomorphism_gen (ppi_const B) qed
 
+  definition gppi_loop_homomorphism_right [constructor] {A : Type*} {B B' : A → Type*}
+    (g : Πa, B a →* B' a) : gppi_loop B →∞g gppi_loop B' :=
+  gloop_ppi_isomorphism B' ∘∞g Ωg→ (pppi_compose_left g) ∘∞g (gloop_ppi_isomorphism B)⁻¹ᵍ⁸
+
 
   /- We first define the group structure on A →* Ω B (except for truncatedness).
      Instead of Ω B, we could also choose any infinity group. However, we need various 2-coherences,
@@ -183,12 +188,30 @@ namespace group
   definition gpmap_loop [reducible] [constructor] (A B : Type*) : InfGroup :=
   InfGroup.mk (A →* Ω B) !inf_group_ppi
 
+  definition gpmap_loopn [constructor] (n : ℕ) [H : is_succ n] (A B : Type*) : InfGroup :=
+  InfGroup.mk (A →** Ω[n] B) (by induction H with n; exact inf_group_ppi (λa, Ω[n] B))
+
+  definition gloop_pmap_isomorphism (A B : Type*) : Ωg (A →** B) ≃∞g gpmap_loop A B :=
+  gloop_ppi_isomorphism _
+
+  definition gloopn_pmap_isomorphism (n : ℕ) [H : is_succ n] (A B : Type*) :
+    Ωg[n] (A →** B) ≃∞g gpmap_loopn n A B :=
+  begin
+    induction H with n, induction n with n IH,
+    { exact gloop_pmap_isomorphism A B },
+    { rexact Ωg≃ (pequiv_of_inf_isomorphism IH) ⬝∞g gloop_pmap_isomorphism A (Ω[succ n] B) }
+  end
+
   definition gpmap_loop' [reducible] [constructor] (A : Type*) {B C : Type*} (e : Ω C ≃* B) :
     InfGroup :=
   InfGroup.mk (A →* B)
     (@inf_group_of_inf_pgroup _ (inf_pgroup_pequiv_closed (ppmap_pequiv_ppmap_right e)
       !inf_pgroup_pppi))
 
+  definition gpmap_loop_homomorphism_right [constructor] (A : Type*) {B B' : Type*}
+    (g : B →* B') : gpmap_loop A B →∞g gpmap_loop A B' :=
+  gppi_loop_homomorphism_right (λa, g)
+
   definition Group_trunc_pmap [reducible] [constructor] (A B : Type*) : Group :=
   Group.mk (trunc 0 (A →* Ω B)) (@group_trunc _ !inf_group_ppi)
 

cohomology/serre.hlean

@@ -85,8 +85,6 @@ begin
   exact pfiber_postnikov_map A n
 end
 
-
-set_option formatter.hide_full_terms false
 definition pfiber_postnikov_map_pred' (A : spectrum) (n k l : ℤ) (p : n + k = l) :
   pfiber (postnikov_map_pred (A k) (maxm2 l)) ≃* EM_spectrum (πₛ[n] A) l :=
 begin

homotopy/EM.hlean

@@ -156,7 +156,7 @@ namespace EM
     (ptrunc_pequiv (n+1+1) (EMadd1 G (n+1)))⁻¹ᵉ* :=
   by reflexivity
 
-  definition ap1_EMadd1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+  definition loop_EMadd1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) :
     psquare (loop_EMadd1 G n) (loop_EMadd1 H n)
             (EMadd1_functor φ n) (Ω→ (EMadd1_functor φ (succ n))) :=
   begin
@@ -181,7 +181,7 @@ namespace EM
     { refine pwhisker_left _ !loopn_EMadd1_pequiv_EM1_succ ⬝* _,
       refine _ ⬝* pwhisker_right _ !loopn_EMadd1_pequiv_EM1_succ⁻¹*,
       refine _ ⬝h* !loopn_succ_in_inv_natural,
-      exact IH ⬝h* (apn_psquare n !ap1_EMadd1_natural) }
+      exact IH ⬝h* (apn_psquare n !loop_EMadd1_natural) }
   end
 
   definition homotopy_group_functor_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) :
@@ -301,15 +301,18 @@ namespace EM
     proof λa, idp qed
 
   definition EMadd1_pmap_equiv (n : ℕ) (X Y : Type*) [is_conn (n+1) X] [is_trunc (n+1+1) X]
-    [is_conn (n+1) Y] [is_trunc (n+1+1) Y] : (X →* Y) ≃ πag[n+2] X →g πag[n+2] Y :=
+    [H4 : is_trunc (n+1+1) Y] : (X →* Y) ≃ πag[n+2] X →g πag[n+2] Y :=
   begin
+    have H4' : is_trunc ((n+1).+1) Y, from H4,
+   have is_set (Ωg[succ (n+1)] Y), from is_set_loopn (n+1+1) Y,
     fapply equiv.MK,
     { exact π→g[n+2] },
-    { exact λφ, (EMadd1_pequiv_type Y n ∘* EMadd1_functor φ (n+1)) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ* },
+    { intro φ, refine (_ ∘* EMadd1_functor φ (n+1)) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ*,
+      exact EMadd1_pmap (n+1) (gtrunc_isomorphism (Ωg[succ (n+1)] Y)) },
     { intro φ, apply homomorphism_eq,
       refine homotopy_group_functor_pcompose (n+2) _ _ ⬝hty _, exact sorry }, -- easy but tedious
     { intro f, apply eq_of_phomotopy, refine (phomotopy_pinv_right_of_phomotopy _)⁻¹*,
-      apply EMadd1_pequiv_type_natural }
+      exact sorry /-apply EMadd1_pequiv_type_natural-/ }
   end
 
   definition EM1_functor_trivial_homomorphism [constructor] (G H : Group) :
@@ -343,19 +346,39 @@ namespace EM
     { refine !loopn_succ_in ⬝e* Ω≃[n] (loop_EMadd1 G (m + n))⁻¹ᵉ* ⬝e* e }
   end
 
+  definition loopn_EMadd1_add_of_eq (G : AbGroup) {n m k : ℕ} (p : m + n = k) : Ω[n] (EMadd1 G k) ≃* EMadd1 G m :=
+  by induction p; exact loopn_EMadd1_add G n m
+
+  definition EM1_phomotopy {G : Group} {X : Type*} [is_trunc 1 X] {f g : EM1 G →* X} (h : Ω→ f ~ Ω→ g) :
+    f ~* g :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x using EM.set_rec with a,
+      { exact respect_pt f ⬝ (respect_pt g)⁻¹ },
+      { apply eq_pathover, apply move_top_of_right, apply move_bot_of_right,
+        apply move_top_of_left', apply move_bot_of_left, apply hdeg_square, exact h (pth a) }},
+    { apply inv_con_cancel_right }
+  end
+
   /- properties about EM -/
 
+  definition deloopable_EM [instance] [constructor] (G : AbGroup) (n : ℕ) : deloopable (EM G n) :=
+  deloopable.mk (EMadd1 G n) (loop_EM G n)
+
   definition gEM (G : AbGroup) (n : ℕ) : InfGroup :=
-  InfGroup_equiv_closed (Ωg (EMadd1 G n)) (loop_EM G n)
+  InfGroup_of_deloopable (EM G n)
 
   definition gloop_EM1 [constructor] (G : Group) : Ωg (EM1 G) ≃∞g InfGroup_of_Group G :=
   inf_isomorphism_of_equiv (EM.base_eq_base_equiv G) groupoid_quotient.encode_con
 
+  definition gloop_EMadd1 [constructor] (G : AbGroup) (n : ℕ) : Ωg (EMadd1 G n) ≃∞g gEM G n :=
+  deloop_isomorphism (EM G n)
+
   definition gEM0_isomorphism (G : AbGroup) : gEM G 0 ≃∞g InfGroup_of_Group G :=
-  !InfGroup_equiv_closed_isomorphism⁻¹ᵍ⁸ ⬝∞g gloop_EM1 G
+  (gloop_EMadd1 G 0)⁻¹ᵍ⁸ ⬝∞g gloop_EM1 G
 
   definition gEM_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : gEM G n →∞g gEM H n :=
-  inf_homomorphism.mk (EM_functor φ n) sorry
+  gloop_EMadd1 H n ∘∞g Ωg→ (EMadd1_functor φ n) ∘∞g (gloop_EMadd1 G n)⁻¹ᵍ⁸
 
   definition EM_pmap [unfold 8] {G : AbGroup} (X : InfGroup) (n : ℕ)
     (e : AbInfGroup_of_AbGroup G →∞g Ωg'[n] X) [H : is_trunc n X] : EM G n →* X :=
@@ -366,9 +389,35 @@ namespace EM
   end
 
   definition EM_homomorphism_gloop [unfold 8] {G : AbGroup} (X : Type*) (n : ℕ)
-    (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g Ωg X :=
+    (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc (n+1) X] : gEM G n →∞g Ωg X :=
   Ωg→ (EMadd1_pmap n e) ∘∞g !InfGroup_equiv_closed_isomorphism⁻¹ᵍ⁸
 
+  definition gloopn_succ_in' (n : ℕ) (A : Type*) : Ωg[succ n] A ≃∞g Ωg'[n] (Ωg A) :=
+  inf_isomorphism_of_equiv (loopn_succ_in n A)
+                           (by cases n with n; apply is_mul_hom_id; exact loopn_succ_in_con)
+
+  definition EM_homomorphism_deloopable [unfold 8] {G : AbGroup} (X : Type*) (H : deloopable X) (n : ℕ)
+    (e : AbInfGroup_of_AbGroup G →∞g Ωg'[n] (InfGroup_of_deloopable X)) (H : is_trunc (n+1) (deloop X)) :
+    gEM G n →∞g InfGroup_of_deloopable X :=
+  deloop_isomorphism X ∘∞g
+  EM_homomorphism_gloop (deloop X) n
+    ((gloopn_succ_in' n (deloop X))⁻¹ᵍ⁸ ∘∞g Ωg'→[n] (deloop_isomorphism X)⁻¹ᵍ⁸ ∘∞g e)
+
+  definition is_mul_hom_EM_functor [constructor] (G H : AbGroup) (n : ℕ) :
+    is_mul_hom (λ(φ : G →gg H), EM_functor φ n) :=
+  begin
+    intro φ ψ,
+    apply eq_of_phomotopy,
+    exact sorry
+    -- exact sorry, exact sorry, exact sorry
+--    refine idpath (φ 0 * ψ 0) ⬝ _,
+  end
+
+  /- an enriched homomorphism -/
+  definition EM_ehomomorphism [constructor] (G H : AbGroup) (n : ℕ) :
+    InfGroup_of_Group (G →gg H) →∞g InfGroup_of_deloopable (EM G n →** EM H n) :=
+  inf_homomorphism.mk (λφ, EM_functor φ n) (is_mul_hom_EM_functor G H n)
+
   -- definition EM_homomorphism [unfold 8] {G : AbGroup} {X : Type*} (Y : Type*) (e : Ω Y ≃* X) (n : ℕ)
   --   (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g X :=
   -- _

homotopy/EMRing.hlean

@@ -2,9 +2,11 @@
 
 import .EM .smash_adjoint ..algebra.ring ..algebra.arrow_group
 
-open algebra eq EM is_equiv equiv is_trunc is_conn pointed trunc susp smash group nat
+open algebra eq EM is_equiv equiv is_trunc is_conn pointed trunc susp smash group nat function
+
 namespace EM
 
+
 definition EM1product_adj {R : Ring} :
   EM1 (AbGroup_of_Ring R) →* ppmap (EM1 (AbGroup_of_Ring R)) (EMadd1 (AbGroup_of_Ring R) 1) :=
 begin
@@ -25,6 +27,7 @@ definition EM0EMadd1product {A B C : AbGroup} (φ : A →g B →gg C) (n : ℕ)
   A →* EMadd1 B n →** EMadd1 C n :=
 EMadd1_pfunctor B C n ∘* pmap_of_homomorphism φ
 
+-- TODO: simplify
 definition EMadd1product {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) :
   EMadd1 A n →* EMadd1 B m →** EMadd1 C (m + succ n) :=
 begin
@@ -32,10 +35,12 @@ begin
   { refine is_trunc_pmap_of_is_conn _ (m.-1) !is_conn_EMadd1 _ _ _ _ !is_trunc_EMadd1,
     exact le_of_eq (trunc_index.of_nat_add_plus_two_of_nat m n)⁻¹ᵖ },
   apply EMadd1_pmap,
-  exact sorry
+  refine (gloopn_pmap_isomorphism (succ n) _ _)⁻¹ᵍ⁸ ∘∞g
-  /- the underlying pointed map is: -/
+    gpmap_loop_homomorphism_right (EMadd1 B m) (loopn_EMadd1_add_of_eq C !succ_add)⁻¹ᵉ* ∘∞g
-  -- refine (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* ∘* ppcompose_left !loopn_EMadd1_add⁻¹ᵉ* ∘*
+    gloop_pmap_isomorphism _ _ ∘∞g
-  --     EM0EMadd1product φ m
+    (deloop_isomorphism _)⁻¹ᵍ⁸ ∘∞g
+    EM_ehomomorphism B C (succ m) ∘∞g
+    inf_homomorphism_of_homomorphism φ
 end
 
 definition EMproduct1 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) :
@@ -51,8 +56,9 @@ begin
     { exact ppcompose_left (ptransport (EMadd1 C) !succ_add⁻¹) ∘* EMadd1product φ n m }}
 end
 
+
 definition EMproduct2 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) :
-  EM A n →* EM B m →** EM C (m + n) :=
+  EM A n →* (EM B m →** EM C (m + n)) :=
 begin
   assert H1 : is_trunc n (gpmap_loop' (EM B m) (loop_EM C (m + n))),
   { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM },
@@ -75,5 +81,43 @@ begin
  exact sorry
 end
 
+definition EMproduct4 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) :
+  gEM A n →∞g Ωg (EM B m →** EM C (m + n + 1)) :=
+begin
+  assert H1 : is_trunc (n+1) (EM B m →** EM C (m + n + 1)),
+  { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM },
+   apply EM_homomorphism_gloop,
+   refine (gloopn_pmap_isomorphism _ _ _)⁻¹ᵍ⁸ ∘∞g _ ∘∞g inf_homomorphism_of_homomorphism φ,
+
+--   exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g
+--        _ ∘∞g inf_homomorphism_of_homomorphism φ
+  exact sorry
+end
+
+definition EMproduct5 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) :
+  InfGroup_of_deloopable (EM A n) →∞g InfGroup_of_deloopable (EM B m →** EM C (m + n)) :=
+begin
+  assert H1 : is_trunc (n + 1) (deloop (EM B m →** EM C (m + n))),
+  { exact is_trunc_pmap_of_is_conn_nat _ m !is_conn_EM _ _ _ !le.refl !is_trunc_EM },
+  refine EM_homomorphism_deloopable _ _ _ _ _,
+
+  -- exact _ /- (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* -/ ∘∞g _ /-ppcompose_left !loopn_EMadd1_add⁻¹ᵉ*-/ ∘∞g
+  --      _ ∘∞g inf_homomorphism_of_homomorphism φ
+  exact sorry
+end
+
+definition EMadd1product2 {A B C : AbGroup} (φ : A →g B →gg C) (n m : ℕ) :
+  gEM A (n+1) →∞g Ωg[succ n] (EMadd1 B m →** EMadd1 C m) :=
+begin
+  assert H1 : is_trunc (n+1) (Ω[n] (EMadd1 B m →** EMadd1 C m)),
+  { apply is_trunc_loopn, exact sorry },
+--  refine EM_homomorphism_gloop (Ω[n] (EMadd1 B m →** EMadd1 C m)) _ _,
+  /- the underlying pointed map is: -/
+--  exact sorry
+  -- refine (loopn_ppmap_pequiv _ _ _)⁻¹ᵉ* ∘* ppcompose_left !loopn_EMadd1_add⁻¹ᵉ* ∘*
+  --     EM0EMadd1product φ m
+  exact sorry
+end
+
 
 end EM

pointed.hlean

@@ -611,5 +611,29 @@ begin
   fapply phomotopy.mk, exact homotopy.rfl, refine whisker_left idp (ap_id p)⁻¹
 end
 
+structure deloopable.{u} [class] (A : pType.{u}) : Type.{u+1} :=
+  (deloop : pType.{u})
+  (deloop_pequiv : Ω deloop ≃* A)
+
+abbreviation deloop [unfold 2] := deloopable.deloop
+abbreviation deloop_pequiv [unfold 2] := deloopable.deloop_pequiv
+
+definition deloopable_loop [instance] [constructor] (A : Type*) : deloopable (Ω A) :=
+deloopable.mk A pequiv.rfl
+
+definition deloopable_loopn [instance] [priority 500] (n : ℕ) [H : is_succ n] (A : Type*) :
+  deloopable (Ω[n] A) :=
+by induction H with n; exact deloopable.mk (Ω[n] A) pequiv.rfl
+
+definition inf_group_of_deloopable (A : Type*) [deloopable A] : inf_group A :=
+inf_group_equiv_closed (deloop_pequiv A) _
+
+definition InfGroup_of_deloopable (A : Type*) [deloopable A] : InfGroup :=
+InfGroup.mk A (inf_group_of_deloopable A)
+
+definition deloop_isomorphism [constructor] (A : Type*) [deloopable A] :
+  Ωg (deloop A) ≃∞g InfGroup_of_deloopable A :=
+InfGroup_equiv_closed_isomorphism (Ωg (deloop A)) (deloop_pequiv A)
+
 
 end pointed

pointed_pi.hlean

@@ -938,6 +938,15 @@ namespace pointed
     (Π*(a : A), Ω (B a)) ≃* Ω (Π*a, B a) :=
   (loop_pppi_pequiv B)⁻¹ᵉ*
 
+definition deloopable_pppi [instance] [constructor] {A : Type*} (B : A → Type*) [Πa, deloopable (B a)] :
+  deloopable (Π*a, B a) :=
+deloopable.mk (Π*a, deloop (B a))
+              (loop_pppi_pequiv (λa, deloop (B a)) ⬝e* ppi_pequiv_right (λa, deloop_pequiv (B a)))
+
+definition deloopable_ppmap [instance] [constructor] (A B : Type*) [deloopable B] :
+  deloopable (A →** B) :=
+deloopable_pppi (λa, B)
+
 
 /- below is an alternate proof strategy for the naturality of loop_pppi_pequiv_natural,
   where we define loop_pppi_pequiv as composite of pointed equivalences, and proved the