work of fiber of maps between EM-spaces

algebra/exactness.hlean

@@ -5,8 +5,8 @@ Authors: Jeremy Avigad
 
 Short exact sequences
 -/
-import homotopy.chain_complex eq2
+import homotopy.chain_complex eq2 .quotient_group
-open pointed is_trunc equiv is_equiv eq algebra group trunc function
+open pointed is_trunc equiv is_equiv eq algebra group trunc function fiber sigma
 
 structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
   ( im_in_ker : Π(a:A), g (f a) = pt)
@@ -34,7 +34,6 @@ begin
   induction h with a p, exact ap g p⁻¹ ⬝ is_exact.im_in_ker H a
 end
 
--- TO DO: give less univalency proof
 definition is_exact_homotopy {A B : Type} {C : Type*} {f f' : A → B} {g g' : B → C}
   (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' :=
 begin
@@ -54,8 +53,8 @@ begin
     exact image.mk (tr a) (ap tr r) }
 end
 
-definition is_contr_middle_of_is_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C} (H : is_exact f g)
+definition is_contr_middle_of_is_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C}
-  [is_contr A] [is_set B] [is_contr C] : is_contr B :=
+  (H : is_exact f g) [is_contr A] [is_set B] [is_contr C] : is_contr B :=
 begin
   apply is_contr.mk (f pt),
   intro b,
@@ -67,6 +66,99 @@ definition is_surjective_of_is_exact_of_is_contr {A B : Type} {C : Type*} {f : A
   (H : is_exact f g) [is_contr C] : is_surjective f :=
 λb, is_exact.ker_in_im H b !is_prop.elim
 
+definition is_embedding_of_is_exact_g {A B C : Group} {g : B →g C} {f : A →g B}
+  (gf : is_exact_g f g) [is_contr A] : is_embedding g :=
+begin
+  apply to_is_embedding_homomorphism, intro a p,
+  induction is_exact.ker_in_im gf a p with x q,
+  exact q⁻¹ ⬝ ap f !is_prop.elim ⬝ to_respect_one f
+end
+
+definition map_left_of_is_exact {G₃' G₃ G₂ : Type} {G₁ : Type*}
+  {g : G₃ → G₂} {g' : G₃' → G₂} {f : G₂ → G₁} (H1 : is_exact g f) (H2 : is_exact g' f)
+  (Hg' : is_embedding g') : G₃ → G₃' :=
+begin
+  intro a,
+  have fiber g' (g a),
+  begin
+    have is_prop (fiber g' (g a)), from !is_prop_fiber_of_is_embedding,
+    induction is_exact.ker_in_im H2 (g a) (is_exact.im_in_ker H1 a) with a' p,
+    exact fiber.mk a' p
+  end,
+  exact point this
+end
+
+definition map_left_of_is_exact_compute {G₃' G₃ G₂ : Type} {G₁ : Type*}
+  {g : G₃ → G₂} {g' : G₃' → G₂} {f : G₂ → G₁} (H1 : is_exact g f) (H2 : is_exact g' f)
+  (Hg' : is_embedding g') (a : G₃) : g' (map_left_of_is_exact H1 H2 Hg' a) = g a :=
+@point_eq _ _ g' _ _
+
+definition map_left_of_is_exact_compose {G₃'' G₃' G₃ G₂ : Type} {G₁ : Type*}
+  {g : G₃ → G₂} {g' : G₃' → G₂} {g'' : G₃'' → G₂} {f : G₂ → G₁}
+  (H1 : is_exact g f) (H2 : is_exact g' f) (H3 : is_exact g'' f)
+  (Hg' : is_embedding g') (Hg'' : is_embedding g'') (a : G₃) :
+  map_left_of_is_exact H2 H3 Hg'' (map_left_of_is_exact H1 H2 Hg' a) =
+  map_left_of_is_exact H1 H3 Hg'' a :=
+begin
+  refine @is_injective_of_is_embedding _ _ g'' _ _ _ _,
+  refine !map_left_of_is_exact_compute ⬝ _ ⬝ !map_left_of_is_exact_compute⁻¹,
+  exact map_left_of_is_exact_compute H1 H2 Hg' a
+end
+
+definition map_left_of_is_exact_id {G₃ G₂ : Type} {G₁ : Type*}
+  {g : G₃ → G₂} {f : G₂ → G₁} (H1 : is_exact g f) (Hg : is_embedding g) (a : G₃) :
+  map_left_of_is_exact H1 H1 Hg a = a :=
+begin
+  refine @is_injective_of_is_embedding _ _ g _ _ _ _,
+  exact map_left_of_is_exact_compute H1 H1 Hg a
+end
+
+definition map_left_of_is_exact_homotopy {G₃' G₃ G₂ : Type} {G₁ : Type*}
+  {g : G₃ → G₂} {g' g'' : G₃' → G₂} {f : G₂ → G₁} (H1 : is_exact g f) (H2 : is_exact g' f)
+  (H3 : is_exact g'' f) (Hg' : is_embedding g') (Hg'' : is_embedding g'') (p : g' ~ g'') :
+  map_left_of_is_exact H1 H2 Hg' ~ map_left_of_is_exact H1 H3 Hg'' :=
+begin
+  intro a,
+  refine @is_injective_of_is_embedding _ _ g' _ _ _ _,
+  exact !map_left_of_is_exact_compute ⬝ (!p ⬝ !map_left_of_is_exact_compute)⁻¹,
+end
+
+definition homomorphism_left_of_is_exact_g {G₃' G₃ G₂ G₁ : Group}
+  {g : G₃ →g G₂} {g' : G₃' →g G₂} {f : G₂ →g G₁} (H1 : is_exact_g g f) (H2 : is_exact_g g' f)
+  (Hg' : is_embedding g') : G₃ →g G₃' :=
+begin
+  apply homomorphism.mk (map_left_of_is_exact H1 H2 Hg'),
+  { intro a a', refine @is_injective_of_is_embedding _ _ g' _ _ _ _,
+    exact !point_eq ⬝ to_respect_mul g a a' ⬝
+      (to_respect_mul g' _ _ ⬝ ap011 mul !point_eq !point_eq)⁻¹ }
+end
+
+definition isomorphism_left_of_is_exact_g {G₃' G₃ G₂ G₁ : Group}
+  {g : G₃ →g G₂} {g' : G₃' →g G₂} {f : G₂ →g G₁} (H1 : is_exact g f) (H2 : is_exact g' f)
+  (Hg : is_embedding g) (Hg' : is_embedding g') : G₃ ≃g G₃' :=
+begin
+  fapply isomorphism.mk, exact homomorphism_left_of_is_exact_g H1 H2 Hg',
+  fapply adjointify, exact homomorphism_left_of_is_exact_g H2 H1 Hg,
+  { intro a, refine @is_injective_of_is_embedding _ _ g' _ _ _ _,
+    refine map_left_of_is_exact_compute H1 H2 Hg' _ ⬝ map_left_of_is_exact_compute H2 H1 Hg a },
+  { intro a, refine @is_injective_of_is_embedding _ _ g _ _ _ _,
+    refine map_left_of_is_exact_compute H2 H1 Hg _ ⬝ map_left_of_is_exact_compute H1 H2 Hg' a },
+end
+
+definition is_exact_incl_of_subgroup {G H : Group} (f : G →g H) :
+  is_exact (incl_of_subgroup (kernel_subgroup f)) f :=
+begin
+  apply is_exact.mk,
+  { intro x, cases x with x p, exact p },
+  { intro x p, exact image.mk ⟨x, p⟩ idp }
+end
+
+definition isomorphism_kernel_of_is_exact {G₄ G₃ G₂ G₁ : Group}
+  {h : G₄ →g G₃} {g : G₃ →g G₂} {f : G₂ →g G₁} (H1 : is_exact h g) (H2 : is_exact g f)
+  (HG : is_contr G₄) : G₃ ≃g kernel f :=
+isomorphism_left_of_is_exact_g H2 (is_exact_incl_of_subgroup f)
+  (is_embedding_of_is_exact_g H1) (is_embedding_incl_of_subgroup _)
+
 section chain_complex
 open succ_str chain_complex
 definition is_exact_of_is_exact_at {N : succ_str} {A : chain_complex N} {n : N}
@@ -89,12 +181,10 @@ structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C)
 lemma is_short_exact_of_is_exact {X A B C Y : Group}
   (k : X →g A) (f : A →g B) (g : B →g C) (l : C →g Y)
   (hX : is_contr X) (hY : is_contr Y)
-  (kf : is_exact k f) (fg : is_exact f g) (gl : is_exact g l) : is_short_exact f g :=
+  (kf : is_exact_g k f) (fg : is_exact_g f g) (gl : is_exact_g g l) : is_short_exact f g :=
 begin
   constructor,
-  { apply to_is_embedding_homomorphism, intro a p,
+  { exact is_embedding_of_is_exact_g kf },
-    induction is_exact.ker_in_im kf a p with x q,
-    exact q⁻¹ ⬝ ap k !is_prop.elim ⬝ to_respect_one k },
   { exact is_exact.im_in_ker fg },
   { exact is_exact.ker_in_im fg },
   { intro c, exact is_exact.ker_in_im gl c !is_prop.elim },
@@ -129,4 +219,46 @@ begin
   { exact is_short_exact.ker_in_im H }
 end
 
+/- TODO: move and remove other versions -/
+
+  definition is_surjective_qg_map {A : Group} (N : normal_subgroup_rel A) :
+    is_surjective (qg_map N) :=
+  begin
+    intro x, induction x,
+    fapply image.mk,
+    exact a, reflexivity,
+    apply is_prop.elimo
+  end
+
+  definition is_surjective_ab_qg_map {A : AbGroup} (N : subgroup_rel A) :
+    is_surjective (ab_qg_map N) :=
+  is_surjective_qg_map _
+
+  definition qg_map_eq_one {A : Group} {K : normal_subgroup_rel A} (g : A) (H : K g) :
+    qg_map K g = 1 :=
+  begin
+    apply set_quotient.eq_of_rel,
+    have e : g * 1⁻¹ = g,
+    from calc
+      g * 1⁻¹ = g * 1 : one_inv
+        ...   = g : mul_one,
+    exact transport (λx, K x) e⁻¹ H
+  end
+
+  definition ab_qg_map_eq_one {A : AbGroup} {K : subgroup_rel A} (g : A) (H : K g) :
+    ab_qg_map K g = 1 :=
+  qg_map_eq_one g H
+
+definition is_short_exact_normal_subgroup {G : Group} (S : normal_subgroup_rel G) :
+  is_short_exact (incl_of_subgroup S) (qg_map S) :=
+begin
+  fconstructor,
+  { exact is_embedding_incl_of_subgroup S },
+  { intro a, fapply qg_map_eq_one, induction a with b p, exact p },
+  { intro b p, fapply image.mk,
+    { apply sigma.mk b, fapply rel_of_qg_map_eq_one, exact p },
+    reflexivity },
+  { exact is_surjective_qg_map S },
+end
+
 end algebra

homotopy/EM.hlean

@@ -1,7 +1,7 @@
 -- Authors: Floris van Doorn
 
 import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed_pi ..pointed
-       ..move_to_lib .susp ..algebra.quotient_group
+       ..move_to_lib .susp ..algebra.exactness
 
 open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
 
@@ -620,31 +620,32 @@ namespace EM
     apply is_conn_fiber, apply is_conn_of_is_conn_succ
   end
 
-  section --move
+  section
-    open chain_complex succ_str
+    open chain_complex prod fin
-  -- definition isomorphism_kernel_of_trivial {N : succ_str} (X : chain_complex N) {n : N}
-  --   (H1 : is_exact_at X n) (H2 : is_exact_at X (S n))
-  --   (HX1 : is_contr (X n)) (HG2 : pgroup (X (S n)))
-  --   : Group_of_pgroup (X (S n)) ≃g kernel (homomorphism.mk (cc_to_fn X _) _) :=
-  -- _
 
+  /- TODO: other cases -/
+  definition LES_isomorphism_kernel_of_trivial.{u}
+    {X Y : pType.{u}} (f : X →* Y) (n : ℕ) [H : is_succ n]
+    (H1 : is_contr (πg[n+1] Y)) : πg[n] (pfiber f) ≃g kernel (π→g[n] f) :=
+  begin
+    induction H with n,
+    have H2 : is_exact (π→g[n+1] (ppoint f)) (π→g[n+1] f),
+    from is_exact_of_is_exact_at (is_exact_LES_of_homotopy_groups f (n+1, 0)),
+    have H3 : is_exact (π→g[n+1] (boundary_map f) ∘g ghomotopy_group_succ_in Y n)
+      (π→g[n+1] (ppoint f)),
+    from is_exact_of_is_exact_at (is_exact_LES_of_homotopy_groups f (n+1, 1)),
+    exact isomorphism_kernel_of_is_exact H3 H2 H1
+  end
 
   end
-  -- definition is_equiv_of_trivial (X : chain_complex N) {n : N}
-  --   (H1 : is_exact_at X n) (H2 : is_exact_at X (S n))
-  --   [HX1 : is_contr (X n)] [HX2 : is_contr (X (S (S (S n))))]
-  --   [pgroup (X (S n))] [pgroup (X (S (S n)))] [is_mul_hom (cc_to_fn X (S n))]
-  --   : is_equiv (cc_to_fn X (S n)) :=
-  -- begin
-  --   apply is_equiv_of_is_surjective_of_is_embedding,
-  --   { apply is_embedding_of_trivial X, apply H2},
-  --   { apply is_surjective_of_trivial X, apply H1},
-  -- end
 
-
+  open group algebra is_trunc
-  open group algebra
+  definition homotopy_group_fiber_EM1_functor.{u} {G H : Group.{u}} (φ : G →g H) :
-  definition homotopy_group_fiber_EM1_functor {G H : Group} (φ : G →g H) :
     π₁ (pfiber (EM1_functor φ)) ≃g kernel φ :=
+  have H1 : is_trunc 1 (EM1 H), from sorry,
+  have H2 : 1 <[ℕ] 1 + 1, from sorry,
+  LES_isomorphism_kernel_of_trivial (EM1_functor φ) 1
+    (@trivial_homotopy_group_of_is_trunc _ 1 2 H1 H2) ⬝g
   sorry
 
   definition homotopy_group_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) :