seq_colim universal property

algebra/quotient_group.hlean

@@ -644,7 +644,7 @@ definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g
     end
 
     definition gqg_elim_compute (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
-      : gqg_elim f H ∘g gqg_map ~ f :=
+      : gqg_elim f H ∘ gqg_map ~ f :=
     begin
       intro g, reflexivity
     end

algebra/seq_colim.hlean

@@ -1,4 +1,4 @@
-import .direct_sum .quotient_group
+import .direct_sum .quotient_group ..move_to_lib
 
 open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops nat
 
@@ -16,15 +16,17 @@ namespace group
     definition seq_colim : AbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥)
 
     definition seq_colim_incl [constructor] (i : ℕ) : A i →g seq_colim :=
-      qg_map _ ∘g dirsum_incl A i
+      gqg_map _ _ ∘g dirsum_incl A i
 
     definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (succ i) (f i a))
                                   (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 :=
       begin
         induction r with r, induction r, 
         refine !to_respect_mul ⬝ _,
-        refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ) (!to_respect_inv)⁻¹ ⬝ _,
-        refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹)) !dirsum_elim_compute ⬝ _,
+        refine ap (λγ, group_fun (dirsum_elim h) (group_fun (dirsum_incl A i) a) * group_fun (dirsum_elim h) γ) 
+                  (!to_respect_inv)⁻¹ ⬝ _,
+        refine ap (λγ, γ * group_fun (dirsum_elim h) (group_fun (dirsum_incl A (succ i)) (f i a)⁻¹)) 
+                  !dirsum_elim_compute ⬝ _,
         refine ap (λγ, (h i a) * γ) !dirsum_elim_compute ⬝ _,
         refine ap (λγ, γ * group_fun (h (succ i)) (f i a)⁻¹) !k ⬝ _,
         refine ap (λγ, group_fun (h (succ i)) (f i a) * γ) (!to_respect_inv) ⬝ _,
@@ -35,6 +37,36 @@ namespace group
                                             (k : Πi a, h i a = h (succ i) (f i a)) : seq_colim →g A' :=
       gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
 
+    definition seq_colim_compute (h : Πi, A i →g A')
+                                 (k : Πi a, h i a = h (succ i) (f i a)) (i : ℕ) (a : A i) : 
+               (seq_colim_elim h k) (seq_colim_incl i a) = h i a :=
+      begin
+        refine gqg_elim_compute (λa, ∥seq_colim_rel a∥) (dirsum_elim h) (seq_colim_quotient h k) (dirsum_incl A i a) ⬝ _,
+        exact !dirsum_elim_compute
+      end
+
+    definition seq_colim_glue {i : @trunctype.mk 0 ℕ _} {a : A i} : seq_colim_incl i a = seq_colim_incl (succ i) (f i a) :=
+   begin
+     refine !grp_comp_comp ⬝ _,
+     refine gqg_eq_of_rel _ _ ⬝ (!grp_comp_comp)⁻¹,
+     exact tr (seq_colim_rel.rmk _ _) 
+   end
+
+    section
+      local abbreviation h (m : seq_colim →g A') : Πi, A i →g A' := λi, m ∘g (seq_colim_incl i)
+      local abbreviation k (m : seq_colim →g A') : Πi a, h m i a = h m (succ i) (f i a) := 
+        λ i a, !grp_comp_comp ⬝ ap m (@seq_colim_glue i a) ⬝ !grp_comp_comp⁻¹
+
+      definition seq_colim_unique (m : seq_colim →g A') : 
+        Πv, seq_colim_elim (h m) (k m) v = m v :=
+      begin
+        intro v, refine (gqg_elim_unique _ (dirsum_elim (h m)) _ m _ _)⁻¹ ⬝ _,
+        apply dirsum_elim_unique, rotate 1, reflexivity,
+        intro i a, reflexivity
+      end
+
+    end
+
   end
 
 end group

move_to_lib.hlean

@@ -187,6 +187,11 @@ namespace group
                      ... = a * (c * (b * d)) : by exact ap (λ bcd, a * bcd) (mul.assoc c b d)
                      ... = (a * c) * (b * d) : by exact (mul.assoc a c (b * d))⁻¹
 
+  definition grp_comp_comp {G H K : Group} (g : H →g K) (f : G →g H) (x : G) : (g ∘g f) x = g (f x) :=
+  begin
+    reflexivity
+  end
+
 end group open group
 
 namespace function