Finish the universal property of the direct sum

algebra/direct_sum.hlean

@@ -23,7 +23,7 @@ namespace group
     variables {A' : CommGroup}
 
     definition dirsum_carrier : CommGroup := free_comm_group (trunctype.mk (Σi, Y i) _)
-    local abbreviation ι := @free_comm_group_inclusion
+    local abbreviation ι [constructor] := @free_comm_group_inclusion
     inductive dirsum_rel : dirsum_carrier → Type :=
     | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)
 
@@ -35,26 +35,30 @@ namespace group
     homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
       begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end
 
-    definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
+    definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
+      (r : ∥dirsum_rel g∥) : free_comm_group_elim (λv, f v.1 v.2) g = 1 :=
     begin
-      refine homomorphism.mk (gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) _) _,
+      induction r with r, induction r,
-      { intro g r, induction r with r, induction r,
+      rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul,
-        rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul,
+      rewrite [one_mul, to_respect_mul, ▸*, ↑foldl, +one_mul, to_respect_mul]
-        rewrite [one_mul], apply ap (free_comm_group_elim (λ v, group_fun (f v.1) v.2)),
-        exact sorry
-        },
-      { exact sorry }
     end
 
+    definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
+    gqg_elim _ (free_comm_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
+
     definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
       dirsum_elim f ∘g dirsum_incl i ~ f i :=
     begin
-      intro g, exact sorry
+      intro g, apply one_mul
     end
 
     definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
       (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
-    sorry
+    begin
+      apply gqg_elim_unique,
+      apply free_comm_group_elim_unique,
+      intro x, induction x with i y, exact H i y
+    end
 
 
   end

algebra/free_commutative_group.hlean

@@ -174,20 +174,27 @@ namespace group
   definition fn_of_free_comm_group_elim [unfold_full] (φ : free_comm_group X →g A) : X → A :=
   φ ∘ free_comm_group_inclusion
 
+  definition free_comm_group_elim_unique [constructor] (f : X → A) (k : free_comm_group X →g A)
+    (H : k ∘ free_comm_group_inclusion ~ f) : k ~ free_comm_group_elim f :=
+  begin
+    refine set_quotient.rec_prop _, intro l, esimp,
+      induction l with s l IH,
+      { esimp [foldl], exact to_respect_one k},
+      { rewrite [foldl_cons, fgh_helper_mul],
+        refine to_respect_mul k (class_of [s]) (class_of l) ⬝ _,
+        rewrite [IH], apply ap (λx, x * _), induction s: rewrite [▸*, one_mul, -H a],
+        apply to_respect_inv }
+  end
+
   variables (X A)
-  definition free_comm_group_elim_equiv_fn : (free_comm_group X →g A) ≃ (X → A) :=
+  definition free_comm_group_elim_equiv_fn [constructor] : (free_comm_group X →g A) ≃ (X → A) :=
   begin
     fapply equiv.MK,
     { exact fn_of_free_comm_group_elim},
     { exact free_comm_group_elim},
     { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
-    { intro φ, apply homomorphism_eq, refine set_quotient.rec_prop _, intro l, esimp,
+    { intro k, symmetry, apply homomorphism_eq, apply free_comm_group_elim_unique,
-      induction l with s l IH,
+      reflexivity }
-      { esimp [foldl], symmetry, exact to_respect_one φ},
-      { rewrite [foldl_cons, fgh_helper_mul],
-        refine _ ⬝ (to_respect_mul φ (class_of [s]) (class_of l))⁻¹,
-        rewrite [▸*,IH], induction s: rewrite [▸*, one_mul], apply ap (λx, x * _),
-        exact !to_respect_inv⁻¹}}
   end
 
 end group

algebra/quotient_group.hlean

@@ -37,7 +37,7 @@ namespace group
   have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc
     (g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)]
                       ... = g * k⁻¹               : by rewrite inv_mul_cancel_right,
-  show N (g * k⁻¹), from H2 ▸ H1
+  show N (g * k⁻¹), by rewrite [-H2]; exact H1
 
   theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) :=
   is_equivalence.mk quotient_rel_refl
@@ -53,7 +53,7 @@ namespace group
     g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc
                     ... = g⁻¹ * h           : inv_mul_cancel_right
                     ... = g⁻¹ * h⁻¹⁻¹       : by rewrite algebra.inv_inv,
-  show N (g⁻¹ * h⁻¹⁻¹), from H2 ▸ H1
+  show N (g⁻¹ * h⁻¹⁻¹), by rewrite [-H2]; exact H1
 
   theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h')
     : quotient_rel N (g * g') (h * h') :=
@@ -187,26 +187,33 @@ namespace group
     apply rel_of_eq _ H
   end
 
-  definition quotient_group_elim (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' :=
+  definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)
+    (g : quotient_group N) : G' :=
+  begin
+    refine set_quotient.elim f _ g,
+    intro g h K,
+    apply eq_of_mul_inv_eq_one,
+    have e : f (g * h⁻¹) = f g * (f h)⁻¹,
+    from calc
+      f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
+             ...  = f g * (f h)⁻¹ : to_respect_inv,
+    rewrite (inverse e),
+    apply H, exact K
+  end
+
+  definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group N →g G' :=
   begin
     fapply homomorphism.mk,
       -- define function
-    { apply set_quotient.elim f,
+    { exact quotient_group_elim_fun f H },
-      intro g h K,
-      apply eq_of_mul_inv_eq_one,
-      have e : f (g * h⁻¹) = f g * (f h)⁻¹,
-      from calc
-        f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
-               ...  = f g * (f h)⁻¹ : to_respect_inv,
-      rewrite (inverse e),
-      apply H, exact K},
     { intro g h, induction g using set_quotient.rec_prop with g,
       induction h using set_quotient.rec_prop with h,
       krewrite (inverse (to_respect_mul (qg_map N) g h)),
       unfold qg_map, esimp, exact to_respect_mul f g h }
   end
 
-  definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) : quotient_group_elim f H ∘g qg_map N ~ f :=
+  definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) :
+    quotient_group_elim f H ∘g qg_map N ~ f :=
   begin
     intro g, reflexivity
   end
@@ -215,7 +222,6 @@ namespace group
     : ( k ∘g qg_map N ~ f ) → k ~ quotient_group_elim f H :=
   begin
     intro K cg, induction cg using set_quotient.rec_prop with g,
-    krewrite (quotient_group_compute f),
     exact K g
   end
 
@@ -340,7 +346,7 @@ print iff.mpr
     definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h :=
     eq_of_rel (tr (rincl H))
 
-    definition gqg_elim (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
+    definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
       : quotient_comm_group_gen →g A₂ :=
     begin
       apply quotient_group_elim f,