define Z-modules from abelian groups

algebra/is_short_exact.hlean

@@ -21,15 +21,29 @@ structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C)
   (ker_in_im : Π(b:B), (g b = pt) → fiber f b)
   (is_surj   : is_split_surjective g)
 
-definition is_short_exact_of_is_exact {X A B C Y : Type*}
-  (k : X → A) (f : A → B) (g : B → C) (l : C → Y)
+definition 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 :=
-sorry
+begin
+  constructor,
+  { apply to_is_embedding_homomorphism, intro a p,
+    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 },
+end
 
 definition is_short_exact_equiv {A B A' B' : Type} {C C' : Type*}
   {f' : A' → B'} {g' : B' → C'} (f : A → B) (g : B → C)
   (eA : A ≃ A') (eB : B ≃ B') (eC : C ≃* C')
   (h : hsquare f f' eA eB) (h : hsquare g g' eB eC)
   (H : is_short_exact f' g') : is_short_exact f g :=
-sorry
+begin
+  constructor,
+  { exact sorry },
+  { exact sorry },
+  { exact sorry },
+  { exact sorry }
+end

algebra/left_module.hlean

@@ -7,7 +7,7 @@ Modules prod vector spaces over a ring.
 
 (We use "left_module," which is more precise, because "module" is a keyword.)
 -/
-import algebra.field ..move_to_lib .is_short_exact
+import algebra.field ..move_to_lib .is_short_exact algebra.group_power
 open is_trunc pointed function sigma eq algebra prod is_equiv equiv group
 
 structure has_scalar [class] (F V : Type) :=
@@ -183,21 +183,17 @@ definition left_module_AddAbGroup_of_LeftModule [instance] {R : Ring} (M : LeftM
   left_module R (AddAbGroup_of_LeftModule M) :=
 LeftModule.struct M
 
-definition left_module_of_ab_group (G : Type) [gG : add_ab_group G] (R : Type) [ring R]
+definition left_module_of_ab_group {G : Type} [gG : add_ab_group G] {R : Type} [ring R]
   (smul : R → G → G)
   (h1 : Π (r : R) (x y : G), smul r (x + y) = (smul r x + smul r y))
   (h2 : Π (r s : R) (x : G), smul (r + s) x = (smul r x + smul s x))
   (h3 : Π r s x, smul (r * s) x = smul r (smul s x))
   (h4 : Π x, smul 1 x = x) : left_module R G  :=
-begin
-  cases gG with Gs Gm Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5,
-  exact left_module.mk smul Gs Gm Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5 h1 h2 h3 h4
-end
+left_module.mk smul _ add add.assoc 0 zero_add add_zero neg add.left_inv add.comm h1 h2 h3 h4
 
 definition LeftModule_of_AddAbGroup {R : Ring} (G : AddAbGroup) (smul : R → G → G)
   (h1 h2 h3 h4) : LeftModule R :=
-LeftModule.mk G (left_module_of_ab_group G R smul h1 h2 h3 h4)
-
+LeftModule.mk G (left_module_of_ab_group smul h1 h2 h3 h4)
 
 section
   variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R}
@@ -400,12 +396,14 @@ end
     (g : B →lm C)
     (h : @is_short_exact _ _ (pType.mk _ 0) f g)
 
+  local abbreviation g_of_lm := @group_homomorphism_of_lm_homomorphism
   definition short_exact_mod_of_is_exact {X A B C Y : LeftModule R}
     (k : X →lm A) (f : A →lm B) (g : B →lm C) (l : C →lm Y)
     (hX : is_contr X) (hY : is_contr Y)
     (kf : is_exact_mod k f) (fg : is_exact_mod f g) (gl : is_exact_mod g l) :
     short_exact_mod A B C :=
-  short_exact_mod.mk f g (is_short_exact_of_is_exact k f g l hX hY kf fg gl)
+  short_exact_mod.mk f g
+    (is_short_exact_of_is_exact (g_of_lm k) (g_of_lm f) (g_of_lm g) (g_of_lm l) hX hY kf fg gl)
 
   definition short_exact_mod_isomorphism {A B A' B' C C' : LeftModule R}
     (eA : A ≃lm A') (eB : B ≃lm B') (eC : C ≃lm C')
@@ -422,4 +420,17 @@ end
 
 end
 
+section int
+open int
+definition left_module_int_of_ab_group [constructor] (A : Type) [add_ab_group A] : left_module rℤ A :=
+left_module_of_ab_group imul imul_add add_imul mul_imul one_imul
+
+definition LeftModule_int_of_AbGroup [constructor] (A : AddAbGroup) : LeftModule rℤ :=
+LeftModule.mk A (left_module_int_of_ab_group A)
+
+definition lm_hom_int.mk [constructor] {A B : AbGroup} (φ : A →g B) :
+  LeftModule_int_of_AbGroup A →lm LeftModule_int_of_AbGroup B :=
+lm_homomorphism_of_group_homomorphism φ (to_respect_imul φ)
+end int
+
 end left_module

algebra/module_exact_couple.hlean

@@ -2,19 +2,13 @@
 
 -- Author: Floris van Doorn
 
-import .graded ..homotopy.spectrum .product_group --types.int.order
+import .graded ..homotopy.spectrum .product_group
 
 open algebra is_trunc left_module is_equiv equiv eq function nat
 
 -- move
 section
   open group int chain_complex pointed succ_str
-  definition LeftModule_int_of_AbGroup [constructor] (A : AbGroup) : LeftModule rℤ :=
-  LeftModule.mk A (left_module.mk sorry sorry sorry sorry 1 sorry sorry sorry sorry sorry sorry sorry sorry sorry)
-
-  definition lm_hom_int.mk [constructor] {A B : AbGroup} (φ : A →g B) :
-    LeftModule_int_of_AbGroup A →lm LeftModule_int_of_AbGroup B :=
- homomorphism.mk φ sorry
 
   definition is_exact_of_is_exact_at {N : succ_str} {A : chain_complex N} {n : N}
     (H : is_exact_at A n) : is_exact (cc_to_fn A (S n)) (cc_to_fn A n) :=