Prove stabilization and work on equivalence of categories

higher_groups.hlean

@@ -6,9 +6,9 @@ Authors: Ulrik Buchholtz, Egbert Rijke, Floris van Doorn
 Formalization of the higher groups paper
 -/
 
-import .pointed_pi
+import .homotopy.EM
 open eq is_conn pointed is_trunc trunc equiv is_equiv trunc_index susp nat algebra
-     prod.ops sigma sigma.ops
+     prod.ops sigma sigma.ops category EM
 namespace higher_group
 set_option pp.binder_types true
 universe variable u
@@ -120,7 +120,7 @@ definition InfGrp_eq {k : ℕ} {G H : [∞;k]Grp} (e : iB G ≃* iB H) : G = H :
 
 -- maybe to do: ωGrp ≃ Σ(X : spectrum), is_sconn n X
 
-/- Constructions -/
+/- Constructions on higher groups -/
 definition Decat (G : [n+1;k]Grp) : [n;k]Grp :=
 Grp.mk (ptrunctype.mk (ptrunc n G) _ pt) (pconntype.mk (ptrunc (n + k) (B G)) _ pt)
   abstract begin
@@ -182,11 +182,11 @@ definition Deloop_adjoint_Loop (G : [n;k+1]Grp) (H : [n+1;k]Grp) :
   ppmap (B (Deloop G)) (B H) ≃* ppmap (B G) (B (Loop H)) :=
 (connect_intro_pequiv _ !is_conn_pconntype)⁻¹ᵉ* /- still a sorry here -/
 
+/- to do: naturality -/
+
 definition Loop_Deloop (G : [n;k+1]Grp) : Loop (Deloop G) = G :=
 Grp_eq (connect_pequiv (is_conn_pconntype (B G)))
 
-/- to do: adjunction, and Loop ∘ Deloop = id -/
-
 definition Forget (G : [n;k+1]Grp) : [n;k]Grp :=
 have is_conn k (B G), from !is_conn_pconntype,
 Grp.mk G (pconntype.mk (Ω (B G)) !is_conn_loop pt)
@@ -217,11 +217,36 @@ begin
   induction H with l H IH, exact G, exact Stabilize IH
 end
 
-lemma Stabilize_pequiv (H : k ≥ n + 2) (G : [n;k]Grp) : B G ≃* Ω (B (Stabilize G)) :=
+definition Forget_Stabilize (H : k ≥ n + 2) (G : [n;k]Grp) : B (Forget (Stabilize G)) ≃* B G :=
-sorry
+loop_ptrunc_pequiv _ _ ⬝e*
+begin
+  cases k with k,
+  { cases H },
+  { have k ≥ succ n, from le_of_succ_le_succ H,
+    assert this : n + succ k ≤ 2 * k,
+    { rewrite [two_mul, add_succ, -succ_add], exact nat.add_le_add_right this k },
+    exact freudenthal_pequiv (B G) this }
+end⁻¹ᵉ* ⬝e*
+ptrunc_pequiv (n + k) _
+
+definition Stabilize_Forget (H : k ≥ n + 1) (G : [n;k+1]Grp) : B (Stabilize (Forget G)) ≃* B G :=
+begin
+  assert lem1 : n + succ k ≤ 2 * k,
+  { rewrite [two_mul, add_succ, -succ_add], exact nat.add_le_add_right H k },
+  have is_conn k (B G), from !is_conn_pconntype,
+  have Π(G' : [n;k+1]Grp), is_trunc (n + k + 1) (B G'), from is_trunc_B,
+  note z := is_conn_fun_loop_susp_counit (B G) (nat.le_refl (2 * k)),
+  refine ptrunc_pequiv_ptrunc_of_le (of_nat_le_of_nat lem1) (@(ptrunc_pequiv_ptrunc_of_is_conn_fun _ _) z) ⬝e*
+    !ptrunc_pequiv,
+end
 
 theorem stabilization (H : k ≥ n + 2) : is_equiv (@Stabilize n k) :=
-sorry
+begin
+  fapply adjointify,
+  { exact Forget },
+  { intro G, apply Grp_eq, exact Stabilize_Forget (le.trans !self_le_succ H) _ },
+  { intro G, apply Grp_eq, exact Forget_Stabilize H G }
+end
 
 definition ωGrp.mk_le {n : ℕ} (k₀ : ℕ)
   (B : Π⦃k : ℕ⦄, k₀ ≤ k → (n+k)-Type*[k.-1])
@@ -233,7 +258,7 @@ sorry
 
 definition ωStabilize_of_le (H : k ≥ n + 2) (G : [n;k]Grp) : [n;ω]Grp :=
 ωGrp.mk_le k (λl H', Grp_equiv n l (nStabilize H' G))
-             (λl H', Stabilize_pequiv (le.trans H H') (nStabilize H' G))
+             (λl H', (Forget_Stabilize (le.trans H H') (nStabilize H' G))⁻¹ᵉ*)
 
 definition ωStabilize (G : [n;k]Grp) : [n;ω]Grp :=
 ωStabilize_of_le !le_max_left (nStabilize !le_max_right G)
@@ -252,4 +277,48 @@ begin
   { exact _ }
 end
 
+definition Grp_hom (G H : [n;k]Grp) : Type :=
+B G →* B H
+
+definition is_set_Grp_hom (G H : [0;k]Grp) : is_set (Grp_hom G H) :=
+is_trunc_pmap_of_is_conn _ (k.-2) _ k _ (le_of_eq (sub_one_add_plus_two_sub_one k 0)⁻¹)
+  (is_trunc_B' H)
+
+local attribute [instance] is_set_Grp_hom
+
+definition Grp_precategory [constructor] (k : ℕ) : precategory [0;k]Grp :=
+precategory.mk (λG H, Grp_hom G H) (λX Y Z g f, g ∘* f) (λX, pid (B X))
+  begin intros, apply eq_of_phomotopy, exact !passoc⁻¹* end
+  begin intros, apply eq_of_phomotopy, apply pid_pcompose end
+  begin intros, apply eq_of_phomotopy, apply pcompose_pid end
+
+definition cGrp [constructor] (k : ℕ) : Precategory :=
+Precategory.mk _ (Grp_precategory k)
+
+definition cGrp_equivalence_cType [constructor] (k : ℕ) : cGrp k ≃c cType*[k.-1] :=
+sorry
+
+-- print category.Grp
+-- set_option pp.universes true
+-- print equivalence.symm
+-- print equivalence.trans
+
+-- set_option pp.all true
+-- definition cGrp_equivalence_Grp [constructor] : cGrp 1 ≃c category.Grp :=
+-- equivalence.trans
+--   _
+--   (equivalence.symm Grp_equivalence_cptruncconntype')
+-- begin
+--   transitivity cptruncconntype'.{u} 0,
+--   exact sorry,
+--   symmetry, exact Grp_equivalence_cptruncconntype'
+-- end
+-- category.equivalence.{u+1 u u+1 u} (category.Category.to_Precategory.{u+1 u} category.Grp.{u})
+--   (EM.cptruncconntype'.{u} (@zero.{0} trunc_index has_zero_trunc_index))
+-- equivalence.trans
+--   _
+--   (equivalence.symm Grp_equivalence_cptruncconntype')
+
+
+
 end higher_group

homotopy/susp.hlean

@@ -78,6 +78,7 @@ sorry
     -- we end up not using this, because to prove that the
     -- composition with the first projection is loop_susp_counit A
     -- is hideous without HIT computations on path constructors
+    parameter (A)
     definition pullback_diagonal_prod_of_wedge : susp (Ω A)
       ≃ Σ (a : A) (w : wedge A A), prod_of_wedge w = (a, a) :=
     begin
@@ -116,6 +117,7 @@ sorry
         induction z with p q, reflexivity }
     end
 
+    parameter {A}
     -- instead we directly compare the fibers, using flattening twice
     definition fiber_loop_susp_counit_equiv (a : A)
       : fiber (loop_susp_counit A) a ≃ fiber prod_of_wedge (a, a) :=
@@ -166,6 +168,7 @@ sorry
 
     open is_conn trunc_index
 
+    parameter (A)
     -- connectivity of loop_susp_counit
     definition is_conn_fun_loop_susp_counit {k : ℕ} (H : k ≤ 2 * n)
       : is_conn_fun k (loop_susp_counit A) :=

move_to_lib.hlean

@@ -1209,6 +1209,11 @@ namespace is_conn
 
 open unit trunc_index nat is_trunc pointed.ops sigma.ops prod.ops
 
+-- todo: make trunc_equiv_trunc_of_is_conn_fun a def.
+definition ptrunc_pequiv_ptrunc_of_is_conn_fun {A B : Type*} (n : ℕ₋₂) (f : A →* B)
+  [H : is_conn_fun n f] : ptrunc n A ≃* ptrunc n B :=
+pequiv_of_pmap (ptrunc_functor n f) (is_equiv_trunc_functor_of_is_conn_fun n f)
+
 definition is_conn_zero {A : Type} (a₀ : trunc 0 A) (p : Πa a' : A, ∥ a = a' ∥) : is_conn 0 A :=
 is_conn_succ_intro a₀ (λa a', is_conn_minus_one _ (p a a'))
 
@@ -1753,6 +1758,23 @@ end
 
 end list
 
+
+namespace susp
+open trunc_index
+/- move to freudenthal -/
+definition freudenthal_pequiv_trunc_index' (A : Type*) (n : ℕ) (k : ℕ₋₂) [HA : is_conn n A]
+  (H : k ≤ of_nat (2 * n)) : ptrunc k A ≃* ptrunc k (Ω (susp A)) :=
+begin
+  assert lem : Π(l : ℕ₋₂), l ≤ 0 → ptrunc l A ≃* ptrunc l (Ω (susp A)),
+  { intro l H', exact ptrunc_pequiv_ptrunc_of_le H' (freudenthal_pequiv A (zero_le (2 * n))) },
+  cases k with k, { exact lem -2 (minus_two_le 0) },
+  cases k with k, { exact lem -1 (succ_le_succ (minus_two_le -1)) },
+  rewrite [-of_nat_add_two at *, add_two_sub_two at HA],
+  exact freudenthal_pequiv A (le_of_of_nat_le_of_nat H)
+end
+
+end susp
+
 /- namespace logic? -/
 namespace decidable
 definition double_neg_elim {A : Type} (H : decidable A) (p : ¬ ¬ A) : A :=