From 93126a9c2b5a76eb96bd988b7e13031133a9075b Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 13 Apr 2017 14:54:48 -0400
Subject: [PATCH] checkpoint, submodules

---
 algebra/direct_sum.hlean |  4 ++--
 algebra/graded.hlean     | 12 ++++++++----
 move_to_lib.hlean        |  9 +++++++--
 3 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index db2df16..5c84a57 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -64,7 +64,7 @@ namespace group
       refine dirsum.rec _ _ _,
           exact h,
         refine !to_respect_zero ⬝ !to_respect_zero⁻¹,
-      intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_add, h₁, h₂]
+      intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_add', h₁, h₂]
     end
 
     definition dirsum_elim_resp_quotient (f : Πi, Y i →a A') (g : dirsum_carrier)
@@ -72,7 +72,7 @@ namespace group
     begin
       induction r with r, induction r,
       rewrite [to_respect_add, to_respect_neg], apply add_neg_eq_of_eq_add,
-      rewrite [zero_add, to_respect_add, ▸*, ↑foldl, +one_mul, to_respect_add]
+      rewrite [zero_add, to_respect_add, ▸*, ↑foldl, +one_mul, to_respect_add']
     end
 
     definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' :=
diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index 591690c..119ece2 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -155,7 +155,7 @@ variables {J : Set} (N : graded_module R J)
 definition dirsum' : AddAbGroup :=
 group.dirsum (λj, AddAbGroup_of_LeftModule (N j))
 variable {N}
-definition dirsum_smul [constructor] (r : R) : dirsum' N →g dirsum' N :=
+definition dirsum_smul [constructor] (r : R) : dirsum' N →a dirsum' N :=
 dirsum_functor (λi, smul_homomorphism (N i) r)
 
 definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) :
@@ -165,13 +165,17 @@ begin
   intro i ni, exact to_smul_right_distrib r s ni
 end
 
-definition dirsum_mul_smul (r s : R) (n : dirsum' N) :
-  dirsum_smul (r * s) n = dirsum_smul r (dirsum_smul s n) :=
+definition dirsum_mul_smul' (r s : R) (n : dirsum' N) :
+  dirsum_smul (r * s) n = (dirsum_smul r ∘a dirsum_smul s) n :=
 begin
-  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_compose⁻¹,
+  refine dirsum_functor_homotopy _ n ⬝ (dirsum_functor_compose _ _ n)⁻¹ᵖ,
   intro i ni, exact to_mul_smul r s ni
 end
 
+definition dirsum_mul_smul (r s : R) (n : dirsum' N) :
+  dirsum_smul (r * s) n = dirsum_smul r (dirsum_smul s n) :=
+proof dirsum_mul_smul' r s n qed
+
 definition dirsum_one_smul (n : dirsum' N) : dirsum_smul 1 n = n :=
 begin
   refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_gid,
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index f9f53a0..b79d422 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -43,6 +43,11 @@ namespace algebra
   definition Set_of_AddGroup [reducible] [constructor] : AddGroup → Set :=
   algebra._trans_of_pSet_of_AddGroup_2
 
+  -- --
+  -- definition Group_of_AddAbGroup [coercion] [constructor] (G : AddAbGroup) : Group :=
+  -- AddGroup.mk G _
+  -- --
+
   definition AddGroup_of_AddAbGroup [coercion] [constructor] (G : AddAbGroup) : AddGroup :=
   AddGroup.mk G _
 
@@ -515,13 +520,13 @@ namespace group
   definition add_homomorphism (G H : AddGroup) : Type := homomorphism G H
   infix ` →a `:55 := add_homomorphism
 
-  definition agroup_fun [coercion] {G H : AddGroup} (φ : G →a H) : G → H :=
+  definition agroup_fun [coercion] [unfold 3] [reducible] {G H : AddGroup} (φ : G →a H) : G → H :=
   φ
 
   definition add_homomorphism.struct [instance] {G H : AddGroup} (φ : G →a H) : is_add_hom φ :=
   homomorphism.addstruct φ
 
-  definition add_homomorphism.mk [constructor] {G H : AddGroup} (φ : G → H) (h : is_add_hom φ) : G →a H :=
+  definition add_homomorphism.mk [constructor] {G H : AddGroup} (φ : G → H) (h : is_add_hom φ) : G →g H :=
   homomorphism.mk φ h
 
   definition add_homomorphism_compose [constructor] [trans] {G₁ G₂ G₃ : AddGroup}