move results to HoTT library, and start on uniqueness of K(G, n) for n>1

homotopy/EM.hlean

@@ -7,234 +7,160 @@ Authors: Floris van Doorn
 Eilenberg MacLane spaces
 -/
 
-import homotopy.EM
+import homotopy.EM .spectrum
 
 open eq is_equiv equiv is_conn is_trunc unit function pointed nat group algebra trunc trunc_index
-     fiber prod fin pointed
+     fiber prod fin pointed susp EM.ops
-
-namespace chain_complex
-  open succ_str
-
-  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 chain_complex open chain_complex
 
 namespace EM
 
-    -- MOVE to connectedness
+  /- Higher EM-spaces -/
-    definition is_conn_fun_to_unit_of_is_conn (n : ℕ₋₂) (A : Type) [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
 
-  /- Whitehead Corollaries -/
+  /- K(G, 2) is unique (see below for general case) -/
-
+  definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : Ω[succ n] (EMadd1 G n) ≃* pType_of_Group G :=
-  -- to pointed
-
-  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,
+    refine _ ⬝e* loop_pEM1 G,
-    { reflexivity},
+    cases n with n,
-    { esimp [pequiv.trans, pequiv.symm],
+    { refine !loop_ptrunc_pequiv ⬝e* _, refine ptrunc_pequiv _ _ _,
-      exact !con.right_inv⁻¹ ⬝ ((!idp_con⁻¹ ⬝ !ap_id⁻¹) ◾ (!ap_id⁻¹⁻² ⬝ !idp_con⁻¹)), }
+      apply is_trunc_eq, apply is_trunc_EM1},
+    induction n with n IH,
+    { exact loop_pequiv_loop (loop_EM2 G)},
+    refine _ ⬝e* IH,
+    refine !phomotopy_group_pequiv_loop_ptrunc⁻¹ᵉ* ⬝e* _ ⬝e* !phomotopy_group_pequiv_loop_ptrunc,
+    apply iterate_psusp_stability_pequiv,
+    rexact add_mul_le_mul_add n 1 1
   end
 
-  -- reorder arguments of is_equiv_compose
+  definition EM2_map [unfold 7] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
-  -- rename whiteheads_principle to whitehead_principle
+    (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
-  definition whitehead_principle_pointed (n : ℕ₋₂) {A B : Type*}
+    [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 → X :=
-    [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 whiteheads_principle n, rexact H 0,
+    change trunc 2 (susp (EM1 G)) → X, intro x,
-    intro a k, revert a, apply is_conn.elim -1,
+    induction x with x, induction x with x,
-    have is_equiv (π→*[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)
+    { exact pt},
-           ∘* π→*[k + 1] f ∘* π→*[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
+    { exact pt},
-    begin
+    { change carrier (Ω X), refine EM1_map e r x}
-      apply is_equiv_compose (π→*[k + 1] f ∘* π→*[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
-      apply is_equiv_compose (π→*[k + 1] (pointed_eta_pequiv A)⁻¹ᵉ*),
-      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
 
-  -- replace in homotopy_group?
+  definition pEM2_pmap [constructor] {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
-  theorem trivial_homotopy_group_of_is_trunc' (A : Type*) {n k : ℕ} [is_trunc n A] (H : n < k)
+    (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
-    : is_contr (π[k] A) :=
+    [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 →* X :=
+  pmap.mk (EM2_map e r) idp
+
+  definition loop_pEM2_pmap {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
+    (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
+    [is_conn 1 X] [is_trunc 2 X] :
+    Ω→[2](pEM2_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G 1 :=
   begin
-    apply is_trunc_trunc_of_is_trunc,
+    exact sorry
-    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
 
-  definition is_trunc_pointed_MK [instance] [priority 1100] (n : ℕ₋₂) {A : Type} (a : A)
+  -- TODO: make arguments in trivial_homotopy_group_of_is_trunc implicit
-    [H : is_trunc n A] : is_trunc n (pointed.MK A a) :=
+  attribute is_conn_EMadd1 is_trunc_EMadd1 [instance]
-  H
+  definition pEM2_pequiv' {G : CommGroup} {X : Type*} (e : Ω[2] X ≃ G)
-
+    (r : Π(p q : Ω[2] X), e (@concat (Ω X) idp idp idp p q) = e p * e q)
-  definition is_contr_of_trivial_homotopy (n : ℕ₋₂) (A : Type) [is_trunc n A] [is_conn 0 A]
+    [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X :=
-    (H : Πk a, is_contr (π[k] (pointed.MK A a))) : is_contr A :=
   begin
-    fapply is_trunc_is_equiv_closed_rev, { exact λa, ⋆},
+    apply pequiv_of_pmap (pEM2_pmap e r),
-    apply whiteheads_principle n,
+    have is_conn 0 (EMadd1 G 1), from !is_conn_of_is_conn_succ,
-    { apply is_equiv_trunc_functor_of_is_conn_fun, apply is_conn_fun_to_unit_of_is_conn},
+    have is_trunc 2 (EMadd1 G 1), from !is_trunc_EMadd1,
-    intro a k,
+    refine whitehead_principle_pointed 2 _ _,
-    apply @is_equiv_of_is_contr,
+    intro k, apply @nat.lt_by_cases k 2: intro H,
-    refine trivial_homotopy_group_of_is_trunc' _ !one_le_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
-
-  -- replace in homotopy_group
-  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 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
-
-  -- open sigma lift
-  -- definition flatten_univ.{u v} {A : Type.{u}} {B : Type.{v}} (f : A → B) :
-  --   Σ(A' B' : Type.{max u v}) (f' : A' → B') (g : A ≃ A') (h : B ≃ B'), h ∘ f ~ f' ∘ g :=
-  -- ⟨lift A, lift B, lift_functor f, proof equiv_lift A qed, proof equiv_lift B qed,
-  --   proof sorry qed⟩
-
-  definition is_conn_inf [reducible] (A : Type) : Type := Πn, is_conn n A
-  definition is_conn_fun_inf [reducible] {A B : Type} (f : A → B) : Type := Πn, is_conn_fun n f
-
-  /- applications to EM spaces -/
-
-  -- TODO
-
-  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
-
-  attribute base_eq_base_equiv [constructor]
-  export [unfold] groupoid_quotient
-
-  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),
-    esimp, intro g, exact !idp_con ⬝ !elim_pth
-  end
-
-  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 _)},
+      do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)},
-    { cases k with k,
+    { cases H, esimp, apply is_equiv_trunc_functor, esimp,
-      { apply is_equiv_trunc_functor, esimp,
+      apply is_equiv.homotopy_closed, rotate 1,
-        apply is_equiv.homotopy_closed, rotate 1,
+      { symmetry, exact loop_pEM2_pmap _ _},
-        { symmetry, exact loop_pEM1_pmap _ _},
+      apply is_equiv_compose, apply pequiv.to_is_equiv, apply to_is_equiv},
-        apply is_equiv_compose, apply to_is_equiv},
+    { apply @is_equiv_of_is_contr,
-      { apply @is_equiv_of_is_contr,
+      exact trivial_homotopy_group_of_is_trunc _ H,
-        do 2 apply trivial_homotopy_group_of_is_trunc _ _ _ !one_le_succ}}
+      apply @trivial_homotopy_group_of_is_trunc, rotate 1, exact H, exact _inst_2}
   end
 
-  definition pEM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
+  definition pEM2_pequiv {G : CommGroup} {X : Type*} (e : πg[1+1] X ≃g G)
-    [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
+    [is_conn 1 X] [is_trunc 2 X] : EMadd1 G 1 ≃* X :=
   begin
-    apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
+    have is_set (Ω[2] X), from !is_trunc_eq,
-    intro p q, esimp, exact respect_mul e (tr p) (tr q)
+    apply pEM2_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
+    intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
   end
 
-  definition KG1_pequiv.{u} {X Y : pType.{u}} (e : π₁ X ≃g π₁ Y)
+ -- general case
-    [is_conn 0 X] [is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] : X ≃* Y :=
+  definition EMadd1_map [unfold 8] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
-  (pEM1_pequiv e)⁻¹ᵉ* ⬝e* pEM1_pequiv !isomorphism.refl
+    (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n → X :=
+  begin
+    revert X e r H1 H2, induction n with n f: intro X e r H1 H2,
+    { change trunc 1 (EM1 G) → X, intro x, induction x with x, exact EM1_map e r x},
+    change trunc (n.+2) (susp (iterate_psusp n (pEM1 G))) → X, intro x,
+    induction x with x, induction x with x,
+    { exact pt},
+    { exact pt},
+    { change carrier (Ω X), refine f _ _ _ _ _ (tr x),
+      { refine _⁻¹ᵉ ⬝e e, apply equiv_of_pequiv, apply pequiv_of_eq, apply loop_space_succ_eq_in},
+      exact abstract begin
+        intro p q, refine _ ⬝ !r, apply ap e, esimp,
+        apply inv_tr_eq_of_eq_tr, symmetry,
+        rewrite [- + ap_inv, - + tr_compose],
+        refine !loop_space_succ_eq_in_concat ⬝ _, exact !tr_inv_tr ◾ !tr_inv_tr
+      end end}
+  end
 
+  definition pEMadd1_pmap [constructor] {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
+    (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X :=
+  pmap.mk (EMadd1_map e r) begin cases n with n: reflexivity end
+
+  definition loop_pEMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
+    (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] :
+    Ω→[succ n](pEMadd1_pmap e r) ~ e⁻¹ᵉ ∘ loopn_EMadd1 G n :=
+  begin
+    apply homotopy_of_inv_homotopy_pre (loopn_EMadd1 G n),
+    intro g, esimp at *,
+    revert X e r H1 H2, induction n with n IH: intro X e r H1 H2,
+    { refine !idp_con ⬝ _, refine !ap_compose'⁻¹ ⬝ _, esimp, apply elim_pth},
+    { replace (succ (succ n)) with ((succ n) + 1), rewrite [apn_succ],
+      unfold [ap1], exact sorry}
+    --exact !idp_con ⬝ !elim_pth
+  end
+
+  -- definition is_conn_of_le (n : ℕ₋₂) (A : Type) [is_conn (n.+1) A] :
+  --   is_conn n A :=
+  -- is_trunc_trunc_of_le A -2 (trunc_index.self_le_succ n)
+  -- attribute is_conn_EMadd1 is_trunc_EMadd1 [instance]
+
+  definition pEMadd1_pequiv' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃ G)
+    (r : Π(p q : Ω[succ n] X), e (@concat (Ω[n] X) pt pt pt p q) = e p * e q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
+  begin
+    apply pequiv_of_pmap (pEMadd1_pmap e r),
+    have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n),
+    have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1,
+    refine whitehead_principle_pointed (n.+1) _ _,
+    intro k, apply @nat.lt_by_cases k (succ n): intro H,
+    { apply @is_equiv_of_is_contr,
+      do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)},
+    { cases H, esimp, apply is_equiv_trunc_functor, esimp,
+      apply is_equiv.homotopy_closed, rotate 1,
+      { symmetry, exact loop_pEMadd1_pmap _ _},
+      apply is_equiv_compose, apply pequiv.to_is_equiv},
+    { apply @is_equiv_of_is_contr,
+      do 2 exact trivial_homotopy_group_of_is_trunc _ H}
+  end
+
+  definition pEMadd1_pequiv {G : CommGroup} {X : Type*} {n : ℕ} (e : πg[n+1] X ≃g G)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
+  begin
+    have is_set (Ω[succ n] X), from !is_set_loopn,
+    apply pEMadd1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
+    intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
+  end
+
+  definition EM_spectrum /-[constructor]-/ (G : CommGroup) : spectrum :=
+  spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)
 
 end EM
+-- cohomology ∥ X → K(G,n) ∥
+-- reduced cohomology ∥ X →* K(G,n) ∥
+-- but we probably want to do this for any spectrum