Merge branch 'master' of https://github.com/cmu-phil/Spectral

algebra/direct_sum.hlean

@@ -12,47 +12,79 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio
 
 namespace group
 
-  variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
+  variables {G G' : AddGroup} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
-            {A B : AbGroup}
+            {A B : AddAbGroup}
 
   variables (X : Set) {l l' : list (X ⊎ X)}
 
   section
 
-    parameters {I : Set} (Y : I → AbGroup)
+    parameters {I : Set} (Y : I → AddAbGroup)
-    variables {A' : AbGroup}
+    variables {A' : AddAbGroup} {Y' : I → AddAbGroup}
 
-    definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
+    definition dirsum_carrier : AddAbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
     local abbreviation ι [constructor] := @free_ab_group_inclusion
     inductive dirsum_rel : dirsum_carrier → Type :=
-    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)
+    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ + ι ⟨i, y₂⟩ +  -(ι ⟨i, y₁ + y₂⟩))
 
-    definition dirsum : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
+    definition dirsum : AddAbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
 
-    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier :=
+    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →a dirsum_carrier :=
 
-    definition dirsum_incl [constructor] (i : I) : Y i →g dirsum :=
+    definition dirsum_incl [constructor] (i : I) : Y i →a dirsum :=
-    homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
+    add_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_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
+    parameter {Y}
+    definition dirsum.rec {P : dirsum → Type} [H : Πg, is_prop (P g)]
+      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 0) (h₃ : Πg h, P g → P h → P (g + h)) :
+      Πg, P g :=
+    begin
+      refine @set_quotient.rec_prop _ _ _ H _,
+      refine @set_quotient.rec_prop _ _ _ (λx, !H) _,
+      esimp, intro l, induction l with s l ih,
+        exact h₂,
+      induction s with v v,
+        induction v with i y,
+        exact h₃ _ _ (h₁ i y) ih,
+      induction v with i y,
+      refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
+      refine transport P _ (h₁ i (-y)),
+      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 [add.left_inv, add.assoc],
+    end
+
+    definition dirsum_homotopy {φ ψ : dirsum →a A'}
+      (h : Πi (y : Y i), φ (dirsum_incl i y) = ψ (dirsum_incl i y)) : φ ~ ψ :=
+    begin
+      refine dirsum.rec _ _ _,
+          exact h,
+        refine !to_respect_zero ⬝ !to_respect_zero⁻¹,
+      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)
       (r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
     begin
       induction r with r, induction r,
-      rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul,
+      rewrite [to_respect_add, to_respect_neg], apply add_neg_eq_of_eq_add,
-      rewrite [one_mul, to_respect_mul, ▸*, ↑foldl, +one_mul, to_respect_mul]
+      rewrite [zero_add, to_respect_add, ▸*, ↑foldl, +one_mul, to_respect_add']
     end
 
-    definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
+    definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' :=
     gqg_elim _ (free_ab_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) :
+    definition dirsum_elim_compute (f : Πi, Y i →a A') (i : I) :
       dirsum_elim f ∘g dirsum_incl i ~ f i :=
     begin
-      intro g, apply one_mul
+      intro g, apply zero_add
     end
 
-    definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
+    definition dirsum_elim_unique (f : Πi, Y i →a A') (k : dirsum →a A')
       (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
     begin
       apply gqg_elim_unique,
@@ -60,7 +92,44 @@ namespace group
       intro x, induction x with i y, exact H i y
     end
 
-
   end
 
+  variables {I J : Set} {Y Y' Y'' : I → AddAbGroup}
+
+  definition dirsum_functor [constructor] (f : Πi, Y i →a Y' i) : dirsum Y →a dirsum Y' :=
+  dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
+
+  theorem dirsum_functor_compose (f' : Πi, Y' i →a Y'' i) (f : Πi, Y i →a Y' i) :
+    dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, reflexivity,
+  end
+
+  variable (Y)
+  definition dirsum_functor_gid : dirsum_functor (λi, aid (Y i)) ~ aid (dirsum Y) :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, reflexivity,
+  end
+  variable {Y}
+
+  definition dirsum_functor_add (f f' : Πi, Y i →a Y' i) :
+    homomorphism_add (dirsum_functor f) (dirsum_functor f') ~
+    dirsum_functor (λi, homomorphism_add (f i) (f' i)) :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, esimp, exact sorry
+  end
+
+  definition dirsum_functor_homotopy {f f' : Πi, Y i →a Y' i} (p : f ~2 f') :
+    dirsum_functor f ~ dirsum_functor f' :=
+  begin
+    apply dirsum_homotopy,
+    intro i y, exact sorry
+  end
+
+  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →a dirsum Y :=
+  dirsum_elim (λj, dirsum_incl Y (f j))
+
 end group

algebra/exact_couple.hlean

@@ -26,6 +26,14 @@ definition image_subgroup_of_diff {B : AbGroup} (d : B →g B) (H : is_different
 definition homology {B : AbGroup} (d : B →g B) (H : is_differential d) : AbGroup :=
   @quotient_ab_group (ab_kernel d) (image_subgroup_of_diff d H)
 
+definition SES_of_differential {B : AbGroup} (d : B →g B) (H : is_differential d) : SES (ab_image d) (ab_kernel d) (homology d H) :=
+  begin
+    fapply SES.mk,
+    sorry,
+-- use the more general fact that a subgroup inclusion is a group homomorphism
+-- maybe use SES_of_subgroup?
+  end
+
 structure exact_couple (A B : AbGroup) : Type :=
   ( i : A →g A) (j : A →g B) (k : B →g A)
   ( exact_ij : is_exact i j)

algebra/free_commutative_group.hlean

@@ -8,13 +8,14 @@ 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
+open eq algebra is_trunc set_quotient relation sigma sigma.ops prod sum list trunc function equiv trunc_index
+     group
 
 namespace group
 
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
-  variables (X : Set) {l l' : list (X ⊎ X)}
+  variables (X : Set) {Y : Set} {l l' : list (X ⊎ X)}
 
   /- Free Abelian Group of a set -/
   namespace free_ab_group
@@ -197,4 +198,36 @@ namespace group
       reflexivity }
   end
 
+  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)
+
+-- set_option pp.all true
+--   definition free_ab_group.rec {P : free_ab_group X → Type} [H : Πg, is_prop (P g)]
+--     (h₁ : Πx, P (free_ab_group_inclusion x))
+--     (h₂ : P 0)
+--     (h₃ : Πg h, P g → P h → P (g * h))
+--     (h₄ : Πg, P g → P g⁻¹) :
+--     Πg, P g :=
+--   begin
+--     refine @set_quotient.rec_prop _ _ _ H _,
+--     refine @set_quotient.rec_prop _ _ _ (λx, !H) _,
+--     esimp, intro l, induction l with s l ih,
+--       exact h₂,
+--     induction s with v v,
+--       induction v with i y,
+--       exact h₃ _ _ (h₁ i y) ih,
+--     induction v with i y,
+--     refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
+--     refine transport P _ (h₁ i y⁻¹),
+--     refine _ ⬝ !mul_one,
+--     refine _ ⬝ ap (mul _) (to_respect_one (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],
+--     apply ap (mul _),
+--     refine _ ⬝ (mul_inv (class_of [inr ⟨i, y⟩]) (ι ⟨i, 1⟩))⁻¹ᵖ,
+--     refine ap011 mul _ _,
+--   end
+
 end group

algebra/graded.hlean

@@ -2,14 +2,14 @@
 
 -- Author: Floris van Doorn
 
-import .left_module
+import .left_module .direct_sum
 
-open algebra eq left_module pointed function equiv is_equiv is_trunc prod
+open algebra eq left_module pointed function equiv is_equiv is_trunc prod group
 
 namespace left_module
 
-definition graded (str : Type) (I : Type) : Type := I → str
+definition graded [reducible] (str : Type) (I : Type) : Type := I → str
-definition graded_module (R : Ring) : Type → Type := graded (LeftModule R)
+definition graded_module [reducible] (R : Ring) : Type → Type := graded (LeftModule R)
 
 variables {R : Ring} {I : Type} {M M₁ M₂ M₃ : graded_module R I}
 
@@ -149,6 +149,46 @@ definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M
   : M₁ →gm M₂ :=
 graded_iso_of_eq p
 
+/- direct sum of graded R-modules -/
+
+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 →a dirsum' N :=
+dirsum_functor (λi, smul_homomorphism (N i) r)
+
+definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) :
+  dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n :=
+begin
+  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_add⁻¹,
+  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 ∘a dirsum_smul s) n :=
+begin
+  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,
+  intro i ni, exact to_one_smul ni
+end
+
+definition dirsum : LeftModule R :=
+LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n)
+  (λr, homomorphism.addstruct (dirsum_smul r))
+  dirsum_smul_right_distrib
+  dirsum_mul_smul
+  dirsum_one_smul
+
 /- exact couples -/
 
 definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=

algebra/left_module.hlean

@@ -8,7 +8,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
-open is_trunc pointed function sigma eq algebra prod is_equiv equiv
+open is_trunc pointed function sigma eq algebra prod is_equiv equiv group
 
 structure has_scalar [class] (F V : Type) :=
 (smul : F → V → V)
@@ -20,8 +20,8 @@ infixl ` • `:73 := has_scalar.smul
 namespace left_module
 
 structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming
-  mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
+  mul → add mul_assoc → add_assoc one → zero one_mul → zero_add mul_one → add_zero inv → neg
-  mul_left_inv→add_left_inv mul_comm→add_comm :=
+  mul_left_inv → add_left_inv mul_comm → add_comm :=
 (smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
 (smul_right_distrib : Π (r s : R) (x : M), smul (ring.add _ r s) x = (add (smul r x) (smul s x)))
 (mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x))
@@ -80,6 +80,7 @@ section left_module
 
   proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v :=
   by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul]
+
 end left_module
 
 /- vector spaces -/
@@ -145,18 +146,66 @@ end module_hom
 structure LeftModule (R : Ring) :=
 (carrier : Type) (struct : left_module R carrier)
 
-local attribute LeftModule.carrier [coercion]
 attribute LeftModule.struct [instance]
 
+section
+local attribute LeftModule.carrier [coercion]
+
+definition AddAbGroup_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : AddAbGroup :=
+AddAbGroup.mk M (LeftModule.struct M)
+end
+
+definition LeftModule.struct2 [instance] {R : Ring} (M : LeftModule R) : left_module R M :=
+LeftModule.struct M
+
+-- definition LeftModule.struct3 [instance] {R : Ring} (M : LeftModule R) :
+--   left_module R (AddAbGroup_of_LeftModule M) :=
+-- _
+
+
 definition pointed_LeftModule_carrier [instance] {R : Ring} (M : LeftModule R) :
   pointed (LeftModule.carrier M) :=
 pointed.mk zero
 
-definition pSet_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : Set* :=
+definition pSet_of_LeftModule {R : Ring} (M : LeftModule R) : Set* :=
 pSet.mk' (LeftModule.carrier M)
 
+definition left_module_AddAbGroup_of_LeftModule [instance] {R : Ring} (M : LeftModule R) :
+  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]
+  (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
+
+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)
+
+
 section
-  variable {R : Ring}
+  variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R}
+
+  definition smul_homomorphism [constructor] (M : LeftModule R) (r : R) : M →a M :=
+  add_homomorphism.mk (λg, r • g) (smul_left_distrib r)
+
+  proposition to_smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
+  !smul_left_distrib
+
+  proposition to_smul_right_distrib (a b : R) (u : M) : (a + b) • u = a • u + b • u :=
+  !smul_right_distrib
+
+  proposition to_mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
+  !mul_smul
+
+  proposition to_one_smul (u : M) : (1 : R) • u = u := !one_smul
 
   structure homomorphism (M₁ M₂ : LeftModule R) : Type :=
     (fn : LeftModule.carrier M₁ → LeftModule.carrier M₂)
@@ -171,7 +220,8 @@ section
   homomorphism.p φ
 
   section
-    variables {M₁ M₂ : LeftModule R} (φ : M₁ →lm M₂)
+
+    variable (φ : M₁ →lm M₂)
 
     definition to_respect_add (x y : M₁) : φ (x + y) = φ x + φ y :=
     respect_add φ x y
@@ -220,10 +270,6 @@ section
 end
 
   section
-  variables {M M₁ M₂ M₃ : LeftModule R}
-
-  definition LeftModule.struct2 [instance] (M : LeftModule R) : left_module R M :=
-  LeftModule.struct M
 
   definition homomorphism.mk' [constructor] (φ : M₁ → M₂)
     (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
@@ -256,8 +302,11 @@ end
   definition equiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃ M₂ :=
   equiv.mk φ !isomorphism.is_equiv_to_hom
 
+  section
+  local attribute pSet_of_LeftModule [coercion]
   definition pequiv_of_isomorphism [constructor] (φ : M₁ ≃lm M₂) : M₁ ≃* M₂ :=
   pequiv_of_equiv (equiv_of_isomorphism φ) (to_respect_zero φ)
+  end
 
   definition isomorphism_of_equiv [constructor] (φ : M₁ ≃ M₂)
     (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
@@ -320,8 +369,19 @@ end
     : M₁ →lm M₂ :=
   isomorphism_of_eq p
 
+  definition group_homomorphism_of_lm_homomorphism [constructor] {M₁ M₂ : LeftModule R}
+    (φ : M₁ →lm M₂) : M₁ →a M₂ :=
+  add_homomorphism.mk φ (to_respect_add φ)
+
+  definition lm_homomorphism_of_group_homomorphism [constructor] {M₁ M₂ : LeftModule R}
+    (φ : M₁ →a M₂) (h : Π(r : R) g, φ (r • g) = r • φ g) : M₁ →lm M₂ :=
+  homomorphism.mk' φ (group.to_respect_add φ) h
+
+  section
+  local attribute pSet_of_LeftModule [coercion]
   definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
   @is_exact M₁ M₂ M₃ (homomorphism_fn f) (homomorphism_fn f')
+  end
 
   end
 

algebra/module_chain_complex.hlean

@@ -10,7 +10,7 @@ open left_module
 
 structure module_chain_complex (R : Ring) (N : succ_str) : Type :=
 (mod : N → LeftModule R)
-(hom : Π (n : N), left_module.homomorphism (mod (S n)) (mod n))
+(hom : Π (n : N), mod (S n) →lm mod n)
 (is_chain_complex :
   Π (n : N) (x : mod (S (S n))), hom n (hom (S n) x) = 0)
 

algebra/quotient_group.hlean

@@ -13,6 +13,7 @@ open eq algebra is_trunc set_quotient relation sigma sigma.ops prod trunc functi
 namespace group
 
   variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
+            {N' : normal_subgroup_rel G'}
   variables {A B : AbGroup}
 
   /- Quotient Group -/
@@ -195,7 +196,7 @@ namespace group
     apply rel_of_eq _ H
   end
 
-  definition rel_of_ab_qg_map_eq_one {K : subgroup_rel A} (a :A) (H : ab_qg_map K a = 1) : K a := 
+  definition rel_of_ab_qg_map_eq_one {K : subgroup_rel A} (a :A) (H : ab_qg_map K a = 1) : K a :=
   begin
     have e : (a * 1⁻¹ = a),
     from calc
@@ -268,6 +269,14 @@ namespace group
     exact H
   end
 
+  definition quotient_group_functor [constructor] (φ : G →g G') (h : Πg, N g → N' (φ g)) :
+    quotient_group N →g quotient_group N' :=
+  begin
+    apply quotient_group_elim (qg_map N' ∘g φ),
+    intro g Ng, esimp,
+    refine qg_map_eq_one (φ g) (h g Ng)
+  end
+
 ------------------------------------------------
   -- FIRST ISOMORPHISM THEOREM
 ------------------------------------------------
@@ -402,7 +411,7 @@ definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
     exact is_embedding_kernel_quotient_extension f
   end
 
-definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B) 
+definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B)
            : quotient_ab_group (kernel_subgroup f) ≃g ab_image f :=
   begin
     fapply isomorphism.mk,
@@ -464,6 +473,10 @@ definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g
     definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h :=
     eq_of_rel (tr (rincl H))
 
+    -- this one might work if the previous one doesn't (maybe make this the default one?)
+    definition gqg_eq_of_rel' {g h : A₁} (H : S (g * h⁻¹)) : class_of g = class_of h :> quotient_ab_group_gen :=
+    gqg_eq_of_rel H
+
     definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
       : quotient_ab_group_gen →g A₂ :=
     begin

algebra/subgroup.hlean

@@ -113,7 +113,7 @@ namespace group
 
   /-- Next, we formalize some aspects of normal subgroups. Recall that a normal subgroup H of a group G is a subgroup which is invariant under all inner automorophisms on G. --/
 
-  definition is_normal [constructor] {G : Group} (R : G → Prop) : Prop :=
+  definition is_normal.{u v} [constructor] {G : Group.{u}} (R : G → Prop.{v}) : Prop.{max u v} :=
   trunctype.mk (Π{g} h, R g → R (h * g * h⁻¹)) _
 
   structure normal_subgroup_rel (G : Group) extends subgroup_rel G :=
@@ -244,7 +244,7 @@ namespace group
   definition is_embedding_incl_of_subgroup {G : Group} (H : subgroup_rel G) : is_embedding (incl_of_subgroup H) :=
   begin
     fapply function.is_embedding_of_is_injective,
-    intro h h', 
+    intro h h',
     fapply subtype_eq
   end
 
@@ -256,7 +256,7 @@ namespace group
   definition is_embedding_ab_kernel_incl {G H : AbGroup} (f : G →g H) : is_embedding (ab_kernel_incl f) :=
   begin
     fapply is_embedding_incl_of_subgroup,
-  end 
+  end
 
   definition subgroup_rel_of_subgroup {G : Group} (H1 H2 : subgroup_rel G) (hyp : Π (g : G), subgroup_rel.R H1 g → subgroup_rel.R H2 g) : subgroup_rel (subgroup H2) :=
   subgroup_rel.mk

algebra/submodule.hlean

@@ -0,0 +1,311 @@
+
+import .left_module .quotient_group
+
+open algebra eq group sigma is_trunc function trunc
+
+/- move to subgroup -/
+
+namespace group
+
+  variables {G H K : Group} {R : subgroup_rel G} {S : subgroup_rel H} {T : subgroup_rel K}
+
+  definition subgroup_functor_fun [unfold 7] (φ : G →g H) (h : Πg, R g → S (φ g)) (x : subgroup R) :
+    subgroup S :=
+  begin
+    induction x with g hg,
+    exact ⟨φ g, h g hg⟩
+  end
+
+  definition subgroup_functor [constructor] (φ : G →g H)
+    (h : Πg, R g → S (φ g)) : subgroup R →g subgroup S :=
+  begin
+    fapply homomorphism.mk,
+    { exact subgroup_functor_fun φ h },
+    { intro x₁ x₂, induction x₁ with g₁ hg₁, induction x₂ with g₂ hg₂,
+      exact sigma_eq !to_respect_mul !is_prop.elimo }
+  end
+
+  definition ab_subgroup_functor [constructor] {G H : AbGroup} {R : subgroup_rel G}
+    {S : subgroup_rel H} (φ : G →g H)
+    (h : Πg, R g → S (φ g)) : ab_subgroup R →g ab_subgroup S :=
+  subgroup_functor φ h
+
+  theorem subgroup_functor_compose (ψ : H →g K) (φ : G →g H)
+    (hψ : Πg, S g → T (ψ g)) (hφ : Πg, R g → S (φ g)) :
+    subgroup_functor ψ hψ ∘g subgroup_functor φ hφ ~
+    subgroup_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
+  begin
+    intro g, induction g with g hg, reflexivity
+  end
+
+  definition subgroup_functor_gid : subgroup_functor (gid G) (λg, id) ~ gid (subgroup R) :=
+  begin
+    intro g, induction g with g hg, reflexivity
+  end
+
+  definition subgroup_functor_mul {G H : AbGroup} {R : subgroup_rel G} {S : subgroup_rel H}
+    (ψ φ : G →g H) (hψ : Πg, R g → S (ψ g)) (hφ : Πg, R g → S (φ g)) :
+    homomorphism_mul (ab_subgroup_functor ψ hψ) (ab_subgroup_functor φ hφ) ~
+    ab_subgroup_functor (homomorphism_mul ψ φ)
+                        (λg hg, subgroup_respect_mul S (hψ g hg) (hφ g hg)) :=
+  begin
+    intro g, induction g with g hg, reflexivity
+  end
+
+  definition subgroup_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
+    (hφ : Πg, R g → S (φ g)) (p : φ ~ ψ) :
+    subgroup_functor φ hφ ~ subgroup_functor ψ hψ :=
+  begin
+    intro g, induction g with g hg,
+    exact subtype_eq (p g)
+  end
+
+
+end group open group
+
+namespace left_module
+/- submodules -/
+variables {R : Ring} {M : LeftModule R} {m m₁ m₂ : M}
+
+structure submodule_rel (M : LeftModule R) : Type :=
+  (S : M → Prop)
+  (Szero : S 0)
+  (Sadd : Π⦃g h⦄, S g → S h → S (g + h))
+  (Ssmul : Π⦃g⦄ (r : R), S g → S (r • g))
+
+definition contains_zero := @submodule_rel.Szero
+definition contains_add  := @submodule_rel.Sadd
+definition contains_smul := @submodule_rel.Ssmul
+attribute submodule_rel.S [coercion]
+
+theorem contains_neg (S : submodule_rel M) ⦃m⦄ (H : S m) : S (-m) :=
+transport (λx, S x) (neg_one_smul m) (contains_smul S (- 1) H)
+
+theorem is_normal_submodule (S : submodule_rel M) ⦃m₁ m₂⦄ (H : S m₁) : S (m₂ + m₁ + (-m₂)) :=
+transport (λx, S x) (by rewrite [add.comm, neg_add_cancel_left]) H
+
+open submodule_rel
+
+variables {S : submodule_rel M}
+
+definition subgroup_rel_of_submodule_rel [constructor] (S : submodule_rel M) :
+  subgroup_rel (AddGroup_of_AddAbGroup M) :=
+subgroup_rel.mk S (contains_zero S) (contains_add S) (contains_neg S)
+
+definition submodule_rel_of_subgroup_rel [constructor] (S : subgroup_rel (AddGroup_of_AddAbGroup M))
+  (h : Π⦃g⦄ (r : R), S g → S (r • g)) : submodule_rel M :=
+submodule_rel.mk S (subgroup_has_one S) @(subgroup_respect_mul S) h
+
+definition submodule' (S : submodule_rel M) : AddAbGroup :=
+ab_subgroup (subgroup_rel_of_submodule_rel S)
+
+definition submodule_smul [constructor] (S : submodule_rel M) (r : R) :
+  submodule' S →a submodule' S :=
+ab_subgroup_functor (smul_homomorphism M r) (λg, contains_smul S r)
+
+definition submodule_smul_right_distrib (r s : R) (n : submodule' S) :
+  submodule_smul S (r + s) n = submodule_smul S r n + submodule_smul S s n :=
+begin
+  refine subgroup_functor_homotopy _ _ _ n ⬝ !subgroup_functor_mul⁻¹,
+  intro m, exact to_smul_right_distrib r s m
+end
+
+definition submodule_mul_smul' (r s : R) (n : submodule' S) :
+  submodule_smul S (r * s) n = (submodule_smul S r ∘g submodule_smul S s) n :=
+begin
+  refine subgroup_functor_homotopy _ _ _ n ⬝ (subgroup_functor_compose _ _ _ _ n)⁻¹ᵖ,
+  intro m, exact to_mul_smul r s m
+end
+
+definition submodule_mul_smul (r s : R) (n : submodule' S) :
+  submodule_smul S (r * s) n = submodule_smul S r (submodule_smul S s n) :=
+by rexact submodule_mul_smul' r s n
+
+definition submodule_one_smul (n : submodule' S) : submodule_smul S 1 n = n :=
+begin
+  refine subgroup_functor_homotopy _ _ _ n ⬝ !subgroup_functor_gid,
+  intro m, exact to_one_smul m
+end
+
+definition submodule (S : submodule_rel M) : LeftModule R :=
+LeftModule_of_AddAbGroup (submodule' S) (submodule_smul S)
+  (λr, homomorphism.addstruct (submodule_smul S r))
+  submodule_smul_right_distrib
+  submodule_mul_smul
+  submodule_one_smul
+
+definition submodule_incl [constructor] (S : submodule_rel M) : submodule S →lm M :=
+lm_homomorphism_of_group_homomorphism (incl_of_subgroup _)
+  begin
+    intro r m, induction m with m hm, reflexivity
+  end
+
+definition incl_smul (S : submodule_rel M) (r : R) (m : M) (h : S m) :
+  r • ⟨m, h⟩ = ⟨_, contains_smul S r h⟩ :> submodule S :=
+by reflexivity
+
+definition submodule_rel_of_submodule [constructor] (S₂ S₁ : submodule_rel M) :
+  submodule_rel (submodule S₂) :=
+submodule_rel.mk (λm, S₁ (submodule_incl S₂ m))
+  (contains_zero S₁)
+  (λm n p q, contains_add S₁ p q)
+  begin
+    intro m r p, induction m with m hm, exact contains_smul S₁ r p
+  end
+
+end left_module
+
+/- move to quotient_group -/
+
+namespace group
+
+  variables {G H K : Group} {R : normal_subgroup_rel G} {S : normal_subgroup_rel H}
+    {T : normal_subgroup_rel K}
+
+  definition quotient_ab_group_functor [constructor] {G H : AbGroup} {R : subgroup_rel G}
+    {S : subgroup_rel H} (φ : G →g H)
+    (h : Πg, R g → S (φ g)) : quotient_ab_group R →g quotient_ab_group S :=
+  quotient_group_functor φ h
+
+  theorem quotient_group_functor_compose (ψ : H →g K) (φ : G →g H)
+    (hψ : Πg, S g → T (ψ g)) (hφ : Πg, R g → S (φ g)) :
+    quotient_group_functor ψ hψ ∘g quotient_group_functor φ hφ ~
+    quotient_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
+  end
+
+  definition quotient_group_functor_gid :
+    quotient_group_functor (gid G) (λg, id) ~ gid (quotient_group R) :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
+  end
+
+set_option pp.universes true
+  definition quotient_group_functor_mul.{u₁ v₁ u₂ v₂}
+    {G H : AbGroup} {R : subgroup_rel.{u₁ v₁} G} {S : subgroup_rel.{u₂ v₂} H}
+    (ψ φ : G →g H) (hψ : Πg, R g → S (ψ g)) (hφ : Πg, R g → S (φ g)) :
+    homomorphism_mul (quotient_ab_group_functor ψ hψ) (quotient_ab_group_functor φ hφ) ~
+    quotient_ab_group_functor (homomorphism_mul ψ φ)
+                        (λg hg, subgroup_respect_mul S (hψ g hg) (hφ g hg)) :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
+  end
+
+  definition quotient_group_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
+    (hφ : Πg, R g → S (φ g)) (p : φ ~ ψ) :
+    quotient_group_functor φ hφ ~ quotient_group_functor ψ hψ :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg,
+    exact ap set_quotient.class_of (p g)
+  end
+
+end group open group
+
+namespace left_module
+
+/- quotient modules -/
+variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M} {S : submodule_rel M}
+
+definition quotient_module' (S : submodule_rel M) : AddAbGroup :=
+quotient_ab_group (subgroup_rel_of_submodule_rel S)
+
+definition quotient_module_smul [constructor] (S : submodule_rel M) (r : R) :
+  quotient_module' S →a quotient_module' S :=
+quotient_ab_group_functor (smul_homomorphism M r) (λg, contains_smul S r)
+
+set_option formatter.hide_full_terms false
+
+definition quotient_module_smul_right_distrib (r s : R) (n : quotient_module' S) :
+  quotient_module_smul S (r + s) n = quotient_module_smul S r n + quotient_module_smul S s n :=
+begin
+  refine quotient_group_functor_homotopy _ _ _ n ⬝ !quotient_group_functor_mul⁻¹,
+  intro m, exact to_smul_right_distrib r s m
+end
+
+definition quotient_module_mul_smul' (r s : R) (n : quotient_module' S) :
+  quotient_module_smul S (r * s) n = (quotient_module_smul S r ∘g quotient_module_smul S s) n :=
+begin
+  refine quotient_group_functor_homotopy _ _ _ n ⬝ (quotient_group_functor_compose _ _ _ _ n)⁻¹ᵖ,
+  intro m, exact to_mul_smul r s m
+end
+
+definition quotient_module_mul_smul (r s : R) (n : quotient_module' S) :
+  quotient_module_smul S (r * s) n = quotient_module_smul S r (quotient_module_smul S s n) :=
+by rexact quotient_module_mul_smul' r s n
+
+definition quotient_module_one_smul (n : quotient_module' S) : quotient_module_smul S 1 n = n :=
+begin
+  refine quotient_group_functor_homotopy _ _ _ n ⬝ !quotient_group_functor_gid,
+  intro m, exact to_one_smul m
+end
+
+definition quotient_module (S : submodule_rel M) : LeftModule R :=
+LeftModule_of_AddAbGroup (quotient_module' S) (quotient_module_smul S)
+  (λr, homomorphism.addstruct (quotient_module_smul S r))
+  quotient_module_smul_right_distrib
+  quotient_module_mul_smul
+  quotient_module_one_smul
+
+definition quotient_map (S : submodule_rel M) : M →lm quotient_module S :=
+lm_homomorphism_of_group_homomorphism (ab_qg_map _) (λr g, idp)
+
+/- specific submodules -/
+definition has_scalar_image (φ : M₁ →lm M₂) ⦃m : M₂⦄ (r : R)
+  (h : image φ m) : image φ (r • m) :=
+begin
+  induction h with m' p,
+  apply image.mk (r • m'),
+  refine to_respect_smul φ r m' ⬝ ap (λx, r • x) p,
+end
+
+definition image_rel (φ : M₁ →lm M₂) : submodule_rel M₂ :=
+submodule_rel_of_subgroup_rel
+  (image_subgroup (group_homomorphism_of_lm_homomorphism φ))
+  (has_scalar_image φ)
+
+definition has_scalar_kernel (φ : M₁ →lm M₂) ⦃m : M₁⦄ (r : R)
+  (p : φ m = 0) : φ (r • m) = 0 :=
+begin
+  refine to_respect_smul φ r m ⬝ ap (λx, r • x) p ⬝ smul_zero r,
+end
+
+definition kernel_rel (φ : M₁ →lm M₂) : submodule_rel M₁ :=
+submodule_rel_of_subgroup_rel
+  (kernel_subgroup (group_homomorphism_of_lm_homomorphism φ))
+  (has_scalar_kernel φ)
+
+definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R :=
+@quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_of_submodule _ (image_rel φ))
+
+variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} (h : Πm, ψ (φ m) = 0)
+definition homology.mk (m : M₂) (h : ψ m = 0) : homology ψ φ :=
+quotient_map _ ⟨m, h⟩
+
+definition homology_eq0 {m : M₂} {hm : ψ m = 0} (h : image φ m) :
+  homology.mk m hm = 0 :> homology ψ φ :=
+ab_qg_map_eq_one _ h
+
+definition homology_eq0' {m : M₂} {hm : ψ m = 0} (h : image φ m):
+  homology.mk m hm = homology.mk 0 (to_respect_zero ψ) :> homology ψ φ :=
+ab_qg_map_eq_one _ h
+
+definition homology_eq {m n : M₂} {hm : ψ m = 0} {hn : ψ n = 0} (h : image φ (m - n)) :
+  homology.mk m hm = homology.mk n hn :> homology ψ φ :=
+eq_of_sub_eq_zero (homology_eq0 h)
+
+-- definition homology.rec (P : homology ψ φ → Type)
+--   [H : Πx, is_set (P x)] (h₀ : Π(m : M₂) (h : ψ m = 0), P (homology.mk m h))
+--   (h₁ : Π(m : M₂) (h : ψ m = 0) (k : image φ m), h₀ m h =[homology_eq0' k] h₀ 0 (to_respect_zero ψ))
+--   : Πx, P x :=
+-- begin
+--   refine @set_quotient.rec _ _ _ H _ _,
+--   { intro v, induction v with m h, exact h₀ m h },
+--   { intro v v', induction v with m hm, induction v' with n hn,
+--     esimp, intro h,
+--     exact change_path _ _, }
+-- end
+
+
+
+end left_module

lessons.md

@@ -0,0 +1,19 @@
+Things I would do differently with hindsight:
+
+* Make pointed dependent maps primitive:
+```lean
+structure ppi (A : Type*) (P : A → Type) (p : P pt) :=
+  (to_fun : Π a : A, P a)
+  (resp_pt : to_fun (Point A) = p)
+```
+(maybe the last argument should be `[p : pointed (P pt)]`). Define pointed (non-dependent) maps as a special case.
+Note: assuming `P : A → Type*` is not general enough.
+
+* Use squares, also for maps, pointed maps, ... heavily
+
+* Type classes for equivalences don't really work
+
+* Coercions should all be defined *immediately* after defining a structure, *before* declaring any
+  instances. This is because the coercion graph is updated after each declared coercion.
+
+* [maybe] make bundled structures primitive

move_to_lib.hlean

@@ -32,6 +32,33 @@ namespace algebra
 
   definition one_unique {A : Type} [group A] {a : A} (H : Πb, a * b = b) : a = 1 :=
   !mul_one⁻¹ ⬝ H 1
+
+  definition pSet_of_AddGroup [constructor] [reducible] [coercion] (G : AddGroup) : Set* :=
+  pSet_of_Group G
+  attribute algebra._trans_of_pSet_of_AddGroup [unfold 1]
+  attribute algebra._trans_of_pSet_of_AddGroup_1 algebra._trans_of_pSet_of_AddGroup_2 [constructor]
+
+  definition pType_of_AddGroup [reducible] [constructor] : AddGroup → Type* :=
+  algebra._trans_of_pSet_of_AddGroup_1
+  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 _
+
+  attribute algebra._trans_of_AddGroup_of_AddAbGroup_1
+            algebra._trans_of_AddGroup_of_AddAbGroup
+            algebra._trans_of_AddGroup_of_AddAbGroup_3 [constructor]
+  attribute algebra._trans_of_AddGroup_of_AddAbGroup_2 [unfold 1]
+
+  definition add_ab_group_AddAbGroup2 [instance] (G : AddAbGroup) : add_ab_group G :=
+  AddAbGroup.struct G
+
 end algebra
 
 namespace eq
@@ -484,12 +511,53 @@ namespace pointed
 end pointed open pointed
 
 namespace group
-  open is_trunc
+  open is_trunc algebra
 
   definition to_fun_isomorphism_trans {G H K : Group} (φ : G ≃g H) (ψ : H ≃g K) :
     φ ⬝g ψ ~ ψ ∘ φ :=
   by reflexivity
 
+  definition add_homomorphism (G H : AddGroup) : Type := homomorphism G H
+  infix ` →a `:55 := add_homomorphism
+
+  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 →g H :=
+  homomorphism.mk φ h
+
+  definition add_homomorphism_compose [constructor] [trans] {G₁ G₂ G₃ : AddGroup}
+    (ψ : G₂ →a G₃) (φ : G₁ →a G₂) : G₁ →a G₃ :=
+  add_homomorphism.mk (ψ ∘ φ) (is_add_hom_compose _ _)
+
+  definition add_homomorphism_id [constructor] [refl] (G : AddGroup) : G →a G :=
+  add_homomorphism.mk (@id G) (is_add_hom_id G)
+
+  abbreviation aid [constructor] := @add_homomorphism_id
+  infixr ` ∘a `:75 := add_homomorphism_compose
+
+  definition to_respect_add' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g h : H₁) : χ (g + h) = χ g + χ h :=
+  respect_add χ g h
+
+  theorem to_respect_zero' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) : χ 0 = 0 :=
+  respect_zero χ
+
+  theorem to_respect_neg' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g : H₁) : χ (-g) = -(χ g) :=
+  respect_neg χ g
+
+  definition homomorphism_add [constructor] {G H : AddAbGroup} (φ ψ : G →a H) : G →a H :=
+  add_homomorphism.mk (λg, φ g + ψ g)
+    abstract begin
+      intro g g', refine ap011 add !to_respect_add' !to_respect_add' ⬝ _,
+      refine !add.assoc ⬝ ap (add _) (!add.assoc⁻¹ ⬝ ap (λx, x + _) !add.comm ⬝ !add.assoc) ⬝ !add.assoc⁻¹
+    end end
+
+  definition homomorphism_mul [constructor] {G H : AbGroup} (φ ψ : G →g H) : G →g H :=
+  homomorphism.mk (λg, φ g * ψ g) (to_respect_add (homomorphism_add φ ψ))
+
   definition pmap_of_homomorphism_gid (G : Group) : pmap_of_homomorphism (gid G) ~* pid G :=
   begin
     fapply phomotopy_of_homotopy, reflexivity
@@ -938,7 +1006,6 @@ namespace sphere
     { exact psusp_pequiv e }
   end
 
-
   -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
   --   f ~* pconst (S* n) (S* m) :=
   -- begin