fix free_abelian_group and direct_sum

algebra/direct_sum.hlean

@@ -17,8 +17,11 @@ namespace group
     parameters {I : Type} [is_set I] (Y : I → AbGroup)
     variables {A' : AbGroup} {Y' : I → AbGroup}
 
-    definition dirsum_carrier : AbGroup := free_ab_group (Σi, Y i)
+    open option pointed
-    local abbreviation ι [constructor] := @free_ab_group_inclusion
+
+    definition dirsum_carrier : AbGroup := free_ab_group (Σi, Y i)₊
+
+    local abbreviation ι [constructor] := (@free_ab_group_inclusion (Σi, Y i)₊ _ ∘ some)
     inductive dirsum_rel : dirsum_carrier → Type :=
     | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ *  (ι ⟨i, y₁ * y₂⟩)⁻¹)
 
@@ -38,19 +41,24 @@ namespace group
       refine @set_quotient.rec_prop _ _ _ H _,
       refine @set_quotient.rec_prop _ _ _ (λx, !H) _,
       esimp, intro l, induction l with s l ih,
-        exact h₂,
+      { exact h₂ },
-      induction s with v v,
+      { induction s with z z,
-        induction v with i y,
+        { induction z with v,
-        exact h₃ _ _ (h₁ i y) ih,
+          { refine transport P _ ih, apply ap class_of, symmetry,
-      induction v with i y,
+            exact eq_of_rel (tr (free_ab_group.fcg_rel.resp_append !free_ab_group.fcg_rel.cancelpt1 (free_ab_group.fcg_rel.rrefl l))) },
-      refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
+          { induction v with i y, exact h₃ _ _ (h₁ i y) ih } },
-      refine transport P _ (h₁ i y⁻¹),
+        { induction z with v,
-      refine _ ⬝ !one_mul,
+          { refine transport P _ ih, apply ap class_of, symmetry,
-      refine _ ⬝ ap (λx, mul x _) (to_respect_zero (dirsum_incl i)),
+            exact eq_of_rel (tr (free_ab_group.fcg_rel.resp_append !free_ab_group.fcg_rel.cancelpt2 (free_ab_group.fcg_rel.rrefl l))) },
-      apply gqg_eq_of_rel',
+          { induction v with i y,
-      apply tr, esimp,
+            refine h₃ (gqg_map _ _ (class_of [inr (some ⟨i, y⟩)])) _ _ ih,
-      refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
+            refine transport P _ (h₁ i y⁻¹),
-      rewrite [mul.left_inv, mul.assoc],
+            refine _ ⬝ !one_mul,
+            refine _ ⬝ ap (λx, mul x _) (to_respect_zero (dirsum_incl i)),
+            apply gqg_eq_of_rel',
+            apply tr, esimp,
+            refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
+            rewrite [mul.left_inv, mul.assoc]} } }
     end
 
     definition dirsum_homotopy {φ ψ : dirsum →g A'}
@@ -63,15 +71,16 @@ namespace group
     end
 
     definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
-      (r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
+      (r : ∥dirsum_rel g∥) : free_ab_group_elim ((pmap_equiv_left (Σi, Y i) A')⁻¹ (λv, f v.1 v.2)) g = 1 :=
     begin
       induction r with r, induction r,
-      rewrite [to_respect_mul, to_respect_inv, to_respect_mul, ▸*, ↑foldl, *one_mul,
+      rewrite [to_respect_mul, to_respect_inv, to_respect_mul, ▸*, ↑foldl, *one_mul],
-        to_respect_mul], apply mul.right_inv
+      rewrite [↑pmap_equiv_left], esimp,
+      rewrite [-to_respect_mul], apply mul.right_inv
     end
 
     definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
-    gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
+    gqg_elim _ (free_ab_group_elim ((pmap_equiv_left (Σi, Y i) A')⁻¹ (λv, f v.1 v.2))) (dirsum_elim_resp_quotient f)
 
     definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) (y : Y i) :
       dirsum_elim f (dirsum_incl i y) = f i y :=
@@ -84,7 +93,10 @@ namespace group
     begin
       apply gqg_elim_unique,
       apply free_ab_group_elim_unique,
-      intro x, induction x with i y, exact H i y
+      intro x, induction x with z,
+      { esimp, refine _ ⬝ to_respect_zero k, apply ap k, apply ap class_of,
+        exact eq_of_rel (tr !free_ab_group.fcg_rel.cancelpt1) },
+      { induction z with i y, exact H i y }
     end
 
   end

algebra/free_abelian_group.hlean

@@ -9,22 +9,24 @@ Constructions with groups
 import algebra.group_theory hit.set_quotient types.list types.sum .free_group
 
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list trunc function equiv trunc_index
-     group
+     group pointed
 
 namespace group
 
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
-  variables (X : Type) {Y : Type} [is_set X] [is_set Y] {l l' : list (X ⊎ X)}
+  variables (X : Type*) {Y : Type*} [is_set X] [is_set Y] {l l' : list (X ⊎ X)}
 
-  /- Free Abelian Group of a set -/
+  /- Free Abelian Group on a pointed set -/
   namespace free_ab_group
 
   inductive fcg_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
-  | rrefl   : Πl, fcg_rel l l
+  | rrefl     : Πl, fcg_rel l l
-  | cancel1 : Πx, fcg_rel [inl x, inr x] []
+  | cancel1   : Πx, fcg_rel [inl x, inr x] []
-  | cancel2 : Πx, fcg_rel [inr x, inl x] []
+  | cancel2   : Πx, fcg_rel [inr x, inl x] []
-  | rflip   : Πx y, fcg_rel [x, y] [y, x]
+  | cancelpt1 : fcg_rel [inl pt] []
+  | cancelpt2 : fcg_rel [inr pt] []
+  | rflip     : Πx y, fcg_rel [x, y] [y, x]
   | resp_append : Π{l₁ l₂ l₃ l₄}, fcg_rel l₁ l₂ → fcg_rel l₃ l₄ →
                              fcg_rel (l₁ ++ l₃) (l₂ ++ l₄)
   | rtrans : Π{l₁ l₂ l₃}, fcg_rel l₁ l₂ → fcg_rel l₂ l₃ →
@@ -49,6 +51,8 @@ namespace group
     { reflexivity},
     { repeat esimp [map], exact cancel2 x},
     { repeat esimp [map], exact cancel1 x},
+    { exact cancelpt2 X },
+    { exact cancelpt1 X },
     { repeat esimp [map], apply fcg_rel.rflip},
     { rewrite [+map_append], exact resp_append IH₁ IH₂},
     { exact rtrans IH₁ IH₂}
@@ -60,6 +64,8 @@ namespace group
     { reflexivity},
     { repeat esimp [map], exact cancel2 x},
     { repeat esimp [map], exact cancel1 x},
+    { exact cancelpt1 X },
+    { exact cancelpt2 X },
     { repeat esimp [map], apply fcg_rel.rflip},
     { rewrite [+reverse_append], exact resp_append IH₂ IH₁},
     { exact rtrans IH₁ IH₂}
@@ -146,22 +152,24 @@ namespace group
 
   /- The universal property of the free commutative group -/
   variables {X A}
-  definition free_ab_group_inclusion [constructor] (x : X) : free_ab_group X :=
+  definition free_ab_group_inclusion [constructor] : X →* free_ab_group X :=
-  class_of [inl x]
+  ppi.mk (λ x, class_of [inl x]) (eq_of_rel (tr (fcg_rel.cancelpt1 X)))
 
-  theorem fgh_helper_respect_fcg_rel (f : X → A) (r : fcg_rel X l l')
+  theorem fgh_helper_respect_fcg_rel (f : X →* A) (r : fcg_rel X l l')
     : Π(g : A), foldl (fgh_helper f) g l = foldl (fgh_helper f) g l' :=
   begin
     induction r with l x x x y l₁ l₂ l₃ l₄ r₁ r₂ IH₁ IH₂ l₁ l₂ l₃ r₁ r₂ IH₁ IH₂: intro g,
     { reflexivity},
     { unfold [foldl], apply mul_inv_cancel_right},
     { unfold [foldl], apply inv_mul_cancel_right},
+    { unfold [foldl], rewrite (respect_pt f), apply mul_one },
+    { unfold [foldl], rewrite [respect_pt f, one_inv], apply mul_one },
     { unfold [foldl, fgh_helper], apply mul.right_comm},
     { rewrite [+foldl_append, IH₁, IH₂]},
     { exact !IH₁ ⬝ !IH₂}
   end
 
-  definition free_ab_group_elim [constructor] (f : X → A) : free_ab_group X →g A :=
+  definition free_ab_group_elim [constructor] (f : X →* A) : free_ab_group X →g A :=
   begin
     fapply homomorphism.mk,
     { intro g, refine set_quotient.elim _ _ g,
@@ -172,10 +180,15 @@ namespace group
       esimp, refine !foldl_append ⬝ _, esimp, apply fgh_helper_mul}
   end
 
-  definition fn_of_free_ab_group_elim [unfold_full] (φ : free_ab_group X →g A) : X → A :=
+  definition fn_of_free_ab_group_elim [unfold_full] (φ : free_ab_group X →g A) : X →* A :=
-  φ ∘ free_ab_group_inclusion
+  ppi.mk (φ ∘ free_ab_group_inclusion)
+  begin
+    refine (_ ⬝ @respect_one _ _ _ _ φ (homomorphism.p φ)),
+    apply ap φ, apply eq_of_rel, apply tr,
+    exact (fcg_rel.cancelpt1 X)
+  end
 
-  definition free_ab_group_elim_unique [constructor] (f : X → A) (k : free_ab_group X →g A)
+  definition free_ab_group_elim_unique [constructor] (f : X →* A) (k : free_ab_group X →g A)
     (H : k ∘ free_ab_group_inclusion ~ f) : k ~ free_ab_group_elim f :=
   begin
     refine set_quotient.rec_prop _, intro l, esimp,
@@ -188,18 +201,20 @@ namespace group
   end
 
   variables (X A)
-  definition free_ab_group_elim_equiv_fn [constructor] : (free_ab_group X →g A) ≃ (X → A) :=
+  definition free_ab_group_elim_equiv_fn [constructor] : (free_ab_group X →g A) ≃ (X →* A) :=
   begin
     fapply equiv.MK,
     { exact fn_of_free_ab_group_elim},
     { exact free_ab_group_elim},
-    { intro f, apply eq_of_homotopy, intro x, esimp, unfold [foldl], apply one_mul},
+    { intro f, apply eq_of_phomotopy, fapply phomotopy.mk,
+      { intro x, esimp, unfold [foldl], apply one_mul },
+      { apply is_prop.elim } },
     { intro k, symmetry, apply homomorphism_eq, apply free_ab_group_elim_unique,
       reflexivity }
   end
 
-  definition free_ab_group_functor (f : X → Y) : free_ab_group X →g free_ab_group Y :=
+  definition free_ab_group_functor (f : X →* Y) : free_ab_group X →g free_ab_group Y :=
-  free_ab_group_elim (free_ab_group_inclusion ∘ f)
+  free_ab_group_elim (free_ab_group_inclusion ∘* f)
 
 -- set_option pp.all true
 --   definition free_ab_group.rec {P : free_ab_group X → Type} [H : Πg, is_prop (P g)]

algebra/free_group.hlean

@@ -129,8 +129,8 @@ namespace group
 
   /- The universal property of the free group -/
   variables {X G}
-  definition free_group_inclusion [constructor] (x : X) : free_group X :=
+  definition free_group_inclusion [constructor] : X →* free_group X :=
-  class_of [inl x]
+  ppi.mk (λ x, class_of [inl x]) (eq_of_rel (tr (free_group_rel.cancelpt1 X)))
 
   definition fgh_helper [unfold 6] (f : X → G) (g : G) (x : X ⊎ X) : G :=
   g * sum.rec (λz, f z) (λz, (f z)⁻¹) x