define submodules, quotient modules and homology of module morphisms

algebra/direct_sum.hlean

@@ -119,7 +119,7 @@ namespace group
     dirsum_functor (λi, homomorphism_add (f i) (f' i)) :=
   begin
     apply dirsum_homotopy,
-    intro i y, exact sorry
+    intro i y, esimp, exact sorry
   end
 
   definition dirsum_functor_homotopy {f f' : Πi, Y i →a Y' i} (p : f ~2 f') :

algebra/graded.hlean

@@ -183,7 +183,8 @@ begin
 end
 
 definition dirsum : LeftModule R :=
-LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n) (λr, homomorphism.addstruct (dirsum_smul 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

algebra/left_module.hlean

@@ -158,6 +158,11 @@ 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
@@ -364,6 +369,14 @@ 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 :=

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

move_to_lib.hlean

@@ -555,6 +555,9 @@ namespace group
       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