add stuff about Postnikov towers, EM-spaces and components

homotopy/EM.hlean

@@ -499,6 +499,65 @@ namespace EM
   equivalence.mk (EM_cfunctor (n+2)) (is_equivalence_EM_cfunctor n)
   end category
 
+  /- move -/
+  -- switch arguments in homotopy_group_trunc_of_le
+  lemma ghomotopy_group_trunc_of_le (k n : ℕ) (A : Type*) [Hk : is_succ k] (H : k ≤[ℕ] n)
+    : πg[k] (ptrunc n A) ≃g πg[k] A :=
+  begin
+    exact sorry
+  end
+
+  lemma homotopy_group_isomorphism_of_ptrunc_pequiv {A B : Type*}
+    (n k : ℕ) (H : n+1 ≤[ℕ] k) (f : ptrunc k A ≃* ptrunc k B) : πg[n+1] A ≃g πg[n+1] B :=
+  (ghomotopy_group_trunc_of_le _ k A H)⁻¹ᵍ ⬝g
+  homotopy_group_isomorphism_of_pequiv n f ⬝g
+  ghomotopy_group_trunc_of_le _ k B H
+
+  open trunc_index
+  lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n :=
+  by induction n with n p; reflexivity; exact ap succ p
+
+  definition is_trunc_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
+    (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
+  begin
+    apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
+    refine is_conn.elim -1 _ _, exact H
+  end
+
+  lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
+    (H2 : is_conn m A) : is_trunc (m + n) A :=
+  begin
+    revert A H H2; induction m with m IH: intro A H H2,
+    { rewrite [nat.zero_add], exact H },
+    rewrite [succ_add],
+    apply is_trunc_succ_of_is_trunc_loop,
+    { apply IH,
+      { apply is_trunc_equiv_closed _ !loopn_succ_in },
+      apply is_conn_loop },
+    exact is_conn_of_le _ (zero_le_of_nat (succ m))
+  end
+
+  lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
+    (H2 : is_conn m A) : is_trunc m A :=
+  is_trunc_of_is_trunc_loopn m 0 A H H2
+
+  definition pequiv_EMadd1_of_loopn_pequiv_EM1 {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[n] X ≃* EM1 G)
+    [H1 : is_conn n X] : X ≃* EMadd1 G n :=
+  begin
+    symmetry, apply EMadd1_pequiv,
+    refine isomorphism_of_eq (ap (λx, πg[x+1] X) !zero_add⁻¹) ⬝g homotopy_group_add X 0 n ⬝g _ ⬝g
+      !fundamental_group_EM1,
+    exact homotopy_group_isomorphism_of_pequiv 0 e,
+    refine is_trunc_of_is_trunc_loopn n 1 X _ _,
+    apply is_trunc_equiv_closed_rev 1 e
+  end
+
+  definition EM1_pequiv_EM1 {G H : Group} (φ : G ≃g H) : EM1 G ≃* EM1 H :=
+  sorry
+
+  definition EMadd1_pequiv_EMadd1 (n : ℕ) {G H : AbGroup} (φ : G ≃g H) : EMadd1 G n ≃* EMadd1 H n :=
+  sorry
+
   /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
 
   definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
@@ -507,30 +566,40 @@ namespace EM
   open fiber EM.ops
 
   definition loopn_succ_pfiber_postnikov_map (A : Type*) (k : ℕ) (n : ℕ₋₂) :
-    Ω[k+1] (pfiber (postnikov_map A (n.+1))) ≃* Ω[k] (pfiber (postnikov_map A n)) :=
+    Ω[k+1] (pfiber (postnikov_map A (n.+1))) ≃* Ω[k] (pfiber (postnikov_map (Ω A) n)) :=
   begin
     exact sorry
   end
 
-  definition loopn_pfiber_postnikov_map (A : Type*) (n : ℕ) :
+  definition pfiber_postnikov_map_zero (A : Type*) :
-    Ω[n+1] (pfiber (postnikov_map A n)) ≃* ptrunc 0 A :=
+    pfiber (postnikov_map A 0) ≃* EM1 (πg[1] A) :=
   begin
-    induction n with n IH,
+    symmetry, apply EM1_pequiv,
-    { exact loopn_succ_pfiber_postnikov_map A 0 -1 ⬝e* !pfiber_pequiv_of_is_prop },
+    { refine !homotopy_group_component⁻¹ᵍ ⬝g _,
-    exact loopn_succ_pfiber_postnikov_map A (n+1) n ⬝e* IH
+      apply homotopy_group_isomorphism_of_ptrunc_pequiv, exact le.refl 1, symmetry,
+      refine !ptrunc_pequiv ⬝e* _,
+      exact sorry
+      },
+    { apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr }
+  end
+
+
+  definition loopn_pfiber_postnikov_map (A : Type*) (n : ℕ) :
+    Ω[n] (pfiber (postnikov_map A n)) ≃* EM1 (πg[n+1] A) :=
+  begin
+    revert A, induction n with n IH: intro A,
+    { apply pfiber_postnikov_map_zero },
+    exact loopn_succ_pfiber_postnikov_map A n n ⬝e* IH (Ω A) ⬝e*
+          EM1_pequiv_EM1 !ghomotopy_group_succ_in⁻¹ᵍ
   end
 
   definition pfiber_postnikov_map_succ (A : Type*) (n : ℕ) :
     pfiber (postnikov_map A (n+1)) ≃* EMadd1 (πag[n+2] A) (n+1) :=
   begin
-    symmetry, apply EMadd1_pequiv,
+    apply pequiv_EMadd1_of_loopn_pequiv_EM1,
-    { },
+    { exact sorry },
-    { apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr }
+    { apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr }
   end
 
-  definition pfiber_postnikov_map_zero (A : Type*) : pfiber (postnikov_map A 0) ≃* EM1 (πg[1] A) :=
-  begin
-    exact sorry
-  end
 
 end EM

move_to_lib.hlean

@@ -954,6 +954,7 @@ namespace fiber
     Ω→ (ppoint f) ∘* (loop_pfiber f)⁻¹ᵉ* ~* ppoint (Ω→ f) :=
   (phomotopy_pinv_right_of_phomotopy (ppoint_loop_pfiber f))⁻¹*
 
+  -- rename to pfiber_pequiv_...
   lemma pfiber_equiv_of_phomotopy_ppoint {A B : Type*} {f g : A →* B} (h : f ~* g)
     : ppoint g ∘* pfiber_equiv_of_phomotopy h ~* ppoint f :=
   begin
@@ -1005,19 +1006,13 @@ namespace fiber
     [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (pfiber f) :=
   is_trunc_fiber n f pt
 
-  definition fiber_equiv_of_is_prop [constructor] {A B : Type} (f : A → B) (b : B) [is_prop B] :
+  definition fiber_equiv_of_is_contr [constructor] {A B : Type} (f : A → B) (b : B) [is_contr B] :
     fiber f b ≃ A :=
-  begin
+  !fiber.sigma_char ⬝e !sigma_equiv_of_is_contr_right
-    fapply equiv.MK,
-    { intro f, cases f with a H, exact a },
-    { intro a, apply fiber.mk a, apply is_prop.elim },
-    { intro a, reflexivity },
-    { intro f, cases f with a H, apply ap (fiber.mk a) !is_prop.elim }
-  end
 
-  definition pfiber_pequiv_of_is_prop [constructor] {A B : Type*} (f : A →* B) [is_prop B] :
+  definition pfiber_pequiv_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B] :
     pfiber f ≃* A :=
-  pequiv_of_equiv (fiber_equiv_of_is_prop f pt) idp
+  pequiv_of_equiv (fiber_equiv_of_is_contr f pt) idp
 
 end fiber
 
@@ -1181,6 +1176,103 @@ namespace is_conn
     cases A with A a, exact H k H2
   end
 
+  /- move! -/
+  open sigma.ops pointed
+  definition merely_constant {A B : Type} (f : A → B) : Type :=
+  Σb, Πa, merely (f a = b)
+
+  definition merely_constant_pmap {A B : Type*} {f : A →* B} (H : merely_constant f) (a : A) :
+    merely (f a = pt) :=
+  tconcat (tconcat (H.2 a) (tinverse (H.2 pt))) (tr (respect_pt f))
+
+  definition merely_constant_of_is_conn {A B : Type*} (f : A →* B) [is_conn 0 A] : merely_constant f :=
+  ⟨pt, is_conn.elim -1 _ (tr (respect_pt f))⟩
+
+  open sigma
+  definition component [constructor] (A : Type*) : Type* :=
+  pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩
+
+  lemma is_conn_component [instance] (A : Type*) : is_conn 0 (component A) :=
+  is_contr.mk (tr pt)
+    begin
+      intro x, induction x with x, induction x with a p, induction p with p, induction p, reflexivity
+    end
+
+  definition component_incl [constructor] (A : Type*) : component A →* A :=
+  pmap.mk pr1 idp
+
+  definition component_intro [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) :
+    A →* component B :=
+  begin
+    fapply pmap.mk,
+    { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) },
+    exact subtype_eq !respect_pt
+  end
+
+  definition component_functor [constructor] {A B : Type*} (f : A →* B) : component A →* component B :=
+  component_intro (f ∘* component_incl A) !merely_constant_of_is_conn
+
+  -- definition component_elim [constructor] {A B : Type*} (f : A →* B) (H : merely_constant f) :
+  --   A →* component B :=
+  -- begin
+  --   fapply pmap.mk,
+  --   { intro a, refine ⟨f a, _⟩, exact tinverse (merely_constant_pmap H a) },
+  --   exact subtype_eq !respect_pt
+  -- end
+
+  /- move!-/
+  lemma is_equiv_ap1_of_is_embedding {A B : Type*} (f : A →* B) [is_embedding f] :
+    is_equiv (Ω→ f) :=
+  sorry
+
+  definition loop_pequiv_loop_of_is_embedding [constructor] {A B : Type*} (f : A →* B) [is_embedding f] :
+    Ω A ≃* Ω B :=
+  pequiv_of_pmap (Ω→ f) (is_equiv_ap1_of_is_embedding f)
+
+  definition loop_component (A : Type*) : Ω (component A) ≃* Ω A :=
+  have is_embedding (component_incl A), from is_embedding_pr1 _,
+  loop_pequiv_loop_of_is_embedding (component_incl A)
+
+  lemma loopn_component (n : ℕ) (A : Type*) : Ω[n+1] (component A) ≃* Ω[n+1] A :=
+  !loopn_succ_in ⬝e* loopn_pequiv_loopn n (loop_component A) ⬝e* !loopn_succ_in⁻¹ᵉ*
+
+  -- lemma fundamental_group_component (A : Type*) : π₁ (component A) ≃g π₁ A :=
+  -- isomorphism_of_equiv (trunc_equiv_trunc 0 (loop_component A)) _
+
+  lemma homotopy_group_component (n : ℕ) (A : Type*) : πg[n+1] (component A) ≃g πg[n+1] A :=
+  sorry
+
+  definition is_trunc_component [instance] (n : ℕ₋₂) (A : Type*) [is_trunc n A] : is_trunc n (component A) :=
+  begin
+    apply @is_trunc_sigma, intro a, cases n with n,
+    { apply is_contr_of_inhabited_prop, exact tr !is_prop.elim },
+    { apply is_trunc_succ_of_is_prop },
+  end
+
+  definition ptrunc_component' (n : ℕ₋₂) (A : Type*) :
+    ptrunc (n.+2) (component A) ≃* component (ptrunc (n.+2) A) :=
+  begin
+    fapply pequiv.MK,
+    { exact ptrunc.elim (n.+2) (component_functor !ptr) },
+    { intro x, cases x with x p, induction x with a,
+      refine tr ⟨a, _⟩,
+      note q := trunc_functor -1 !tr_eq_tr_equiv p,
+      exact trunc_trunc_equiv_left _ !minus_one_le_succ q },
+    { exact sorry },
+    { exact sorry }
+  end
+
+  definition ptrunc_component (n : ℕ₋₂) (A : Type*) : ptrunc n (component A) ≃* component (ptrunc n A) :=
+  begin
+    cases n with n, exact sorry,
+    cases n with n, exact sorry,
+    exact ptrunc_component' n A
+  end
+
+  definition pfiber_pequiv_component_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B]
+    /- extra condition, something like trunc_functor 0 f is an embedding -/ : pfiber f ≃* component A :=
+  sorry
+
 end is_conn
 
 namespace circle