From aefc8eccc120b85f9bf9cc3127abb2198ee9d0e1 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 13 Apr 2017 20:39:04 -0400 Subject: [PATCH] define submodules, quotient modules and homology of module morphisms --- algebra/direct_sum.hlean | 2 +- algebra/graded.hlean | 3 +- algebra/left_module.hlean | 13 ++ algebra/subgroup.hlean | 6 +- algebra/submodule.hlean | 311 ++++++++++++++++++++++++++++++++++++++ move_to_lib.hlean | 3 + 6 files changed, 333 insertions(+), 5 deletions(-) create mode 100644 algebra/submodule.hlean diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index 5c84a57..5363b8a 100644 --- a/algebra/direct_sum.hlean +++ b/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') : diff --git a/algebra/graded.hlean b/algebra/graded.hlean index 119ece2..82d43bc 100644 --- a/algebra/graded.hlean +++ b/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 diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean index 165a5ab..d51514e 100644 --- a/algebra/left_module.hlean +++ b/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 := diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index 1ed1376..e65cfa2 100644 --- a/algebra/subgroup.hlean +++ b/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 diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean new file mode 100644 index 0000000..47dfc33 --- /dev/null +++ b/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 diff --git a/move_to_lib.hlean b/move_to_lib.hlean index b79d422..4f0b981 100644 --- a/move_to_lib.hlean +++ b/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