From 94066a6ba8cce3d6fa65d18ea6715df314368fe7 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 9 Oct 2018 21:27:37 -0400 Subject: [PATCH] some more algebra --- algebra/exact_couple.hlean | 4 +- algebra/exactness.hlean | 32 +-------- algebra/left_module.hlean | 14 ++++ algebra/quotient_group.hlean | 71 +++++++++++++------ algebra/spectral_sequence.hlean | 16 +++-- algebra/subgroup.hlean | 13 +++- algebra/submodule.hlean | 122 ++++++++++++++++++++------------ move_to_lib.hlean | 4 ++ 8 files changed, 173 insertions(+), 103 deletions(-) diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean index 2cfdfad..a302cfa 100644 --- a/algebra/exact_couple.hlean +++ b/algebra/exact_couple.hlean @@ -671,8 +671,8 @@ namespace pointed definition homotopy_group_conn_nat_functor (n : ℕ) {A B : Type*[1]} (f : A →* B) : homotopy_group_conn_nat n A →g homotopy_group_conn_nat n B := begin - cases n with n, { apply trivial_homomorphism }, - cases n with n, { apply trivial_homomorphism }, + cases n with n, { apply group.trivial_homomorphism }, + cases n with n, { apply group.trivial_homomorphism }, exact π→g[n+2] f end diff --git a/algebra/exactness.hlean b/algebra/exactness.hlean index 8e78fca..b90bdd9 100644 --- a/algebra/exactness.hlean +++ b/algebra/exactness.hlean @@ -243,37 +243,6 @@ definition is_contr_left_of_is_short_exact {A B : Type} {C : Type*} {f : A → B (H : is_short_exact f g) (HB : is_contr B) (a₀ : A) : is_contr A := is_contr_of_is_embedding f (is_short_exact.is_emb H) _ a₀ -/- TODO: move and remove other versions -/ - - definition is_surjective_qg_map {A : Group} (N : property A) [is_normal_subgroup A N] : - is_surjective (qg_map N) := - begin - intro x, induction x, - fapply image.mk, - exact a, reflexivity, - apply is_prop.elimo - end - - definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_normal_subgroup A N] : - is_surjective (ab_qg_map N) := - is_surjective_ab_qg_map _ - - definition qg_map_eq_one {A : Group} {K : property A} [is_normal_subgroup A K] (g : A) - (H : g ∈ K) : - qg_map K g = 1 := - begin - apply set_quotient.eq_of_rel, - have e : g * 1⁻¹ = g, - from calc - g * 1⁻¹ = g * 1 : one_inv - ... = g : mul_one, - exact transport (λx, K x) e⁻¹ H - end - - definition ab_qg_map_eq_one {A : AbGroup} {K : property A} [is_subgroup A K] (g : A) - (H : g ∈ K) : - ab_qg_map K g = 1 := - ab_qg_map_eq_one g H definition is_short_exact_normal_subgroup {G : Group} (S : property G) [is_normal_subgroup G S] : is_short_exact (incl_of_subgroup S) (qg_map S) := @@ -287,4 +256,5 @@ begin { exact is_surjective_qg_map S }, end + end algebra diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean index acc277a..257a620 100644 --- a/algebra/left_module.hlean +++ b/algebra/left_module.hlean @@ -183,6 +183,10 @@ definition left_module_AddAbGroup_of_LeftModule [instance] {R : Ring} (M : LeftM left_module R (AddAbGroup_of_LeftModule M) := LeftModule.struct M +definition left_module_AddAbGroup_of_LeftModule2 [instance] {R : Ring} (M : LeftModule R) : + left_module R (Group_of_AbGroup (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)) @@ -423,6 +427,15 @@ section (g : B →lm C) (h : @is_short_exact A B C f g) + structure five_exact_mod (A B C D E : LeftModule R) := + (f₁ : A →lm B) + (f₂ : B →lm C) + (f₃ : C →lm D) + (f₄ : D →lm E) + (h₁ : @is_exact A B C f₁ f₂) + (h₂ : @is_exact B C D f₂ f₃) + (h₃ : @is_exact C D E f₃ f₄) + 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) @@ -610,4 +623,5 @@ group_isomorphism_of_lm_isomorphism φ end int + end left_module diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index bdc433d..45c0e8e 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -150,7 +150,8 @@ namespace group definition ab_qg_map {G : AbGroup} (N : property G) [is_subgroup G N] : G →g quotient_ab_group N := @qg_map _ N (is_normal_subgroup_ab _) - definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_subgroup A N] : is_surjective (ab_qg_map N) := + definition is_surjective_qg_map {A : Group} (N : property A) [is_normal_subgroup A N] : + is_surjective (qg_map N) := begin intro x, induction x, fapply image.mk, @@ -158,6 +159,10 @@ namespace group apply is_prop.elimo end + definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_subgroup A N] : + is_surjective (ab_qg_map N) := + @is_surjective_qg_map _ _ _ + namespace quotient notation `⟦`:max a `⟧`:0 := qg_map _ a end quotient @@ -165,25 +170,20 @@ namespace group open quotient variables {N N'} - definition qg_map_eq_one (g : G) (H : N g) : qg_map N g = 1 := + definition qg_map_eq_one {A : Group} {K : property A} [is_normal_subgroup A K] (g : A) + (H : g ∈ K) : qg_map K g = 1 := begin - apply eq_of_rel, - have e : (g * 1⁻¹ = g), - from calc + apply set_quotient.eq_of_rel, + have e : g * 1⁻¹ = g, + from calc g * 1⁻¹ = g * 1 : one_inv ... = g : mul_one, - unfold quotient_rel, rewrite e, exact H + exact transport (λx, K x) e⁻¹ H end - definition ab_qg_map_eq_one {K : property A} [is_subgroup A K] (g :A) (H : K g) : ab_qg_map K g = 1 := - begin - apply eq_of_rel, - have e : (g * 1⁻¹ = g), - from calc - g * 1⁻¹ = g * 1 : one_inv - ... = g : mul_one, - unfold quotient_rel, xrewrite e, exact H - end + definition ab_qg_map_eq_one {A : AbGroup} {K : property A} [is_subgroup A K] (g : A) (H : g ∈ K) : + ab_qg_map K g = 1 := + @qg_map_eq_one _ _ _ g H --- there should be a smarter way to do this!! Please have a look, Floris. definition rel_of_qg_map_eq_one (g : G) (H : qg_map N g = 1) : g ∈ N := @@ -454,16 +454,14 @@ namespace group definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel f) →g B := begin - unfold quotient_ab_group, - fapply @quotient_group_elim A B _ (@is_normal_subgroup_ab _ (kernel f) _) f, + apply quotient_ab_group_elim f, intro a, intro p, exact p end definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) : kernel_quotient_extension f ∘ ab_qg_map (kernel f) ~ f := begin - intro a, - apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _) + intro a, reflexivity end definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) : @@ -474,7 +472,7 @@ definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) note H := is_surjective_ab_qg_map (kernel f) x, induction H, induction p, intro q, - apply @qg_map_eq_one _ _ (@is_normal_subgroup_ab _ (kernel f) _), + apply ab_qg_map_eq_one, refine _ ⬝ q, symmetry, rexact kernel_quotient_extension_triangle f a @@ -698,6 +696,27 @@ namespace group exact ap set_quotient.class_of (p g) end + definition quotient_group_isomorphism_quotient_group [constructor] (φ : G ≃g H) + (h : Πg, g ∈ R ↔ φ g ∈ S) : quotient_group R ≃g quotient_group S := + begin + refine isomorphism.MK (quotient_group_functor φ (λg, iff.mp (h g))) + (quotient_group_functor φ⁻¹ᵍ (λg gS, iff.mpr (h _) (transport S (right_inv φ g)⁻¹ gS))) _ _, + { refine quotient_group_functor_compose _ _ _ _ ⬝hty + quotient_group_functor_homotopy _ _ proof right_inv φ qed ⬝hty + quotient_group_functor_gid }, + { refine quotient_group_functor_compose _ _ _ _ ⬝hty + quotient_group_functor_homotopy _ _ proof left_inv φ qed ⬝hty + quotient_group_functor_gid } + end + + definition is_equiv_qg_map {G : Group} (H : property G) [is_normal_subgroup G H] + (H₂ : Π⦃g⦄, g ∈ H → g = 1) : is_equiv (qg_map H) := + set_quotient.is_equiv_class_of _ (λg h r, eq_of_mul_inv_eq_one (H₂ r)) + + definition quotient_group_isomorphism [constructor] {G : Group} (H : property G) + [is_normal_subgroup G H] (h : Πg, g ∈ H → g = 1) : quotient_group H ≃g G := + (isomorphism.mk _ (is_equiv_qg_map H h))⁻¹ᵍ + end group namespace group @@ -735,4 +754,16 @@ namespace group quotient_ab_group_functor φ hφ ~ quotient_ab_group_functor ψ hψ := @quotient_group_functor_homotopy G H R _ S _ ψ φ hψ hφ p + definition is_equiv_ab_qg_map {G : AbGroup} (H : property G) [is_subgroup G H] + (h : Π⦃g⦄, g ∈ H → g = 1) : is_equiv (ab_qg_map H) := + proof @is_equiv_qg_map G H (is_normal_subgroup_ab _) h qed + + definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : property G) + [is_subgroup G H] (h : Πg, H g → g = 1) : quotient_ab_group H ≃g G := + (isomorphism.mk _ (is_equiv_ab_qg_map H h))⁻¹ᵍ + + definition quotient_ab_group_isomorphism_quotient_ab_group [constructor] (φ : G ≃g H) + (h : Πg, g ∈ R ↔ φ g ∈ S) : quotient_ab_group R ≃g quotient_ab_group S := + @quotient_group_isomorphism_quotient_group _ _ _ _ _ _ φ h + end group diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean index ec3bdcf..4fb98cd 100644 --- a/algebra/spectral_sequence.hlean +++ b/algebra/spectral_sequence.hlean @@ -140,7 +140,16 @@ namespace spectral_sequence Einf c (n, s) ≃lm E' n s := E_isomorphism0 c (λr Hr, H1 r) (λr Hr, H2 r) - /- we call a spectral sequence normal if it is a first-quadrant spectral sequence and the degree of d is what we expect -/ + definition convergence_0 (n : ℤ) (H : Πm, lb c m = 0) : + is_built_from (Dinf n) (λ(k : ℕ), Einf c (n - k, k)) := + is_built_from_isomorphism isomorphism.rfl + (λk, left_module.isomorphism_of_eq (ap (Einf c) + (prod_eq (ap (sub n) (ap (add _) !H ⬝ add_zero _)) (ap (add _) !H ⬝ add_zero _)))) + (HDinf c n) + + /- we call a spectral sequence normal if it is a first-quadrant spectral sequence and + the degree of d on page r (for r ≥ 2) is (r, -(r-1)). + The indexing is different, because we start counting pages at 2. -/ include c structure is_normal : Type := (normal1 : Π{n} s, n < 0 → is_contr (E' n s)) @@ -166,10 +175,7 @@ namespace spectral_sequence refine lt_of_lt_of_le H2 (le.trans _ (le_of_eq !add_zero⁻¹)), exact add_le_add_right (of_nat_le_of_nat_of_le Hr') 1 }, end - /- some properties which use the degree of the spectral sequence we construct. For the AHSS and SSS the hypothesis is by reflexivity -/ - - --- definition foo + omit d end spectral_sequence diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index e58ccb1..ad25140 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -79,7 +79,7 @@ namespace group variables {G₁ G₂ : Group} - -- TODO: maybe define this in more generality for pointed propertys? + -- TODO: maybe define this in more generality for pointed sets? definition kernel [constructor] (φ : G₁ →g G₂) : property G₁ := { g | trunctype.mk (φ g = 1) _} theorem mul_mem_kernel (φ : G₁ →g G₂) (g h : G₁) (H₁ : g ∈ kernel φ) (H₂ : h ∈ kernel φ) : g * h ∈ kernel φ := @@ -555,6 +555,17 @@ end intro r, induction r, reflexivity end + definition is_equiv_incl_of_subgroup {G : Group} (H : property G) [is_subgroup G H] + (h : Πg, g ∈ H) : is_equiv (incl_of_subgroup H) := + have is_surjective (incl_of_subgroup H), + begin intro g, exact image.mk ⟨g, h g⟩ idp end, + have is_embedding (incl_of_subgroup H), from is_embedding_incl_of_subgroup H, + function.is_equiv_of_is_surjective_of_is_embedding (incl_of_subgroup H) + + definition subgroup_isomorphism [constructor] {G : Group} (H : property G) [is_subgroup G H] + (h : Πg, g ∈ H) : subgroup H ≃g G := + isomorphism.mk _ (is_equiv_incl_of_subgroup H h) + end group open group diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean index 0e2722e..6fdd463 100644 --- a/algebra/submodule.hlean +++ b/algebra/submodule.hlean @@ -5,41 +5,6 @@ import .left_module .quotient_group open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv property - definition group_homomorphism_of_add_group_homomorphism [constructor] {G₁ G₂ : AddGroup} - (φ : G₁ →a G₂) : G₁ →g G₂ := - φ - --- move to subgroup --- attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2] --- attribute normal_subgroup_rel.to_subgroup_rel [constructor] - - definition is_equiv_incl_of_subgroup {G : Group} (H : property G) [is_subgroup G H] (h : Πg, g ∈ H) : - is_equiv (incl_of_subgroup H) := - have is_surjective (incl_of_subgroup H), - begin intro g, exact image.mk ⟨g, h g⟩ idp end, - have is_embedding (incl_of_subgroup H), from is_embedding_incl_of_subgroup H, - function.is_equiv_of_is_surjective_of_is_embedding (incl_of_subgroup H) - -definition subgroup_isomorphism [constructor] {G : Group} (H : property G) [is_subgroup G H] (h : Πg, g ∈ H) : - subgroup H ≃g G := -isomorphism.mk _ (is_equiv_incl_of_subgroup H h) - -definition is_equiv_qg_map {G : Group} (H : property G) [is_normal_subgroup G H] (H₂ : Π⦃g⦄, g ∈ H → g = 1) : - is_equiv (qg_map H) := -set_quotient.is_equiv_class_of _ (λg h r, eq_of_mul_inv_eq_one (H₂ r)) - -definition quotient_group_isomorphism [constructor] {G : Group} (H : property G) [is_normal_subgroup G H] - (h : Πg, g ∈ H → g = 1) : quotient_group H ≃g G := -(isomorphism.mk _ (is_equiv_qg_map H h))⁻¹ᵍ - -definition is_equiv_ab_qg_map {G : AbGroup} (H : property G) [is_subgroup G H] (h : Π⦃g⦄, g ∈ H → g = 1) : - is_equiv (ab_qg_map H) := -proof @is_equiv_qg_map G H (is_normal_subgroup_ab _) h qed - -definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : property G) [is_subgroup G H] - (h : Πg, H g → g = 1) : quotient_ab_group H ≃g G := -(isomorphism.mk _ (is_equiv_ab_qg_map H h))⁻¹ᵍ - namespace left_module /- submodules -/ variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M} @@ -61,7 +26,7 @@ transport (λx, S x) (by rewrite [add.comm, neg_add_cancel_left]) H -- open is_submodule -variables {S : property M} [is_submodule M S] +variables {S : property M} [is_submodule M S] {S₂ : property M₂} [is_submodule M₂ S₂] definition is_subgroup_of_is_submodule [instance] (S : property M) [is_submodule M S] : is_subgroup (AddGroup_of_AddAbGroup M) S := @@ -221,22 +186,29 @@ definition quotient_map [constructor] : M →lm quotient_module S := lm_homomorphism_of_group_homomorphism (ab_qg_map _) (λr g, idp) definition quotient_map_eq_zero (m : M) (H : S m) : quotient_map S m = 0 := -@qg_map_eq_one _ _ (is_normal_subgroup_ab _) _ H +@ab_qg_map_eq_one _ _ _ _ H definition rel_of_quotient_map_eq_zero (m : M) (H : quotient_map S m = 0) : S m := -@rel_of_qg_map_eq_one _ _ (is_normal_subgroup_ab _) m H +@rel_of_qg_map_eq_one _ _ _ m H variable {S} +definition respect_smul_quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, m ∈ S → φ m = 0) + (r : R) (m : quotient_module S) : + quotient_ab_group_elim (group_homomorphism_of_lm_homomorphism φ) H + (@has_scalar.smul _ (quotient_module S) _ r m) = + r • quotient_ab_group_elim (group_homomorphism_of_lm_homomorphism φ) H m := +begin + revert m, + refine @set_quotient.rec_prop _ _ _ (λ x, !is_trunc_eq) _, + intro m, + exact to_respect_smul φ r m +end + definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, m ∈ S → φ m = 0) : quotient_module S →lm M₂ := lm_homomorphism_of_group_homomorphism (quotient_ab_group_elim (group_homomorphism_of_lm_homomorphism φ) H) - begin - intro r, esimp, - refine @set_quotient.rec_prop _ _ _ (λ x, !is_trunc_eq) _, - intro m, - exact to_respect_smul φ r m - end + (respect_smul_quotient_elim φ H) definition is_prop_quotient_module (S : property M) [is_submodule M S] [H : is_prop M] : is_prop (quotient_module S) := begin apply @set_quotient.is_trunc_set_quotient, exact H end @@ -255,6 +227,17 @@ definition quotient_module_isomorphism [constructor] (S : property M) [is_submod quotient_module S ≃lm M := (isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map S h))⁻¹ˡᵐ +definition quotient_module_functor [constructor] (φ : M →lm M₂) (h : Πg, g ∈ S → φ g ∈ S₂) : + quotient_module S →lm quotient_module S₂ := +quotient_elim (quotient_map S₂ ∘lm φ) + begin intros m Hm, rexact quotient_map_eq_zero S₂ (φ m) (h m Hm) end + +definition quotient_module_isomorphism_quotient_module [constructor] (φ : M ≃lm M₂) + (h : Πm, m ∈ S ↔ φ m ∈ S₂) : quotient_module S ≃lm quotient_module S₂ := +lm_isomorphism_of_group_isomorphism + (quotient_ab_group_isomorphism_quotient_ab_group (group_isomorphism_of_lm_isomorphism φ) h) + (to_respect_smul (quotient_module_functor φ (λg, iff.mp (h g)))) + /- specific submodules -/ definition has_scalar_image (φ : M₁ →lm M₂) ⦃m : M₂⦄ (r : R) (h : image φ m) : image φ (r • m) := @@ -455,6 +438,57 @@ definition is_surjective_of_is_contr_homology_of_is_contr (ψ : M₂ →lm M₃) (H₁ : is_contr (homology ψ φ)) (H₂ : is_contr M₃) : is_surjective φ := is_surjective_of_is_contr_homology_of_constant ψ H₁ (λm, @eq_of_is_contr _ H₂ _ _) +definition cokernel_module (φ : M₁ →lm M₂) : LeftModule R := +quotient_module (image φ) + +definition cokernel_module_isomorphism_homology (φ : M₁ →lm M₂) : + homology (trivial_homomorphism M₂ (trivial_LeftModule R)) φ ≃lm cokernel_module φ := +quotient_module_isomorphism_quotient_module + (submodule_isomorphism _ (λm, idp)) + begin intro m, reflexivity end + +open chain_complex fin nat +definition LES_of_SESs.{u} {N : succ_str} (A B C : N → LeftModule.{_ u} R) (φ : Πn, A n →lm B n) + (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) : + chain_complex.{_ u} (stratified N 2) := +begin + fapply chain_complex.mk, + { intro x, apply @pSet_of_LeftModule R, + induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), + { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left}, + { /-k=0-/ exact B n }, + { /-k=1-/ exact A n }, + { /-k=2-/ exact C n }}, + { intro x, apply @pmap_of_homomorphism R, + induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), + { /-k≥3-/ exfalso, apply lt_le_antisymm H, apply le_add_left}, + { /-k=0-/ exact φ n }, + { /-k=1-/ exact submodule_incl _ ∘lm short_exact_mod.g (ses n) }, + { /-k=2-/ change B (succ_str.S n) →lm C n, exact short_exact_mod.f (ses n) ∘lm !quotient_map }}, + { intros x m, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), + { exfalso, apply lt_le_antisymm H, apply le_add_left}, + { exact (short_exact_mod.g (ses n) m).2 }, + { exact ap pr1 (is_short_exact.im_in_ker (short_exact_mod.h (ses n)) (quotient_map _ m)) }, + { exact ap (short_exact_mod.f (ses n)) (quotient_map_eq_zero _ _ (image.mk m idp)) ⬝ + to_respect_zero (short_exact_mod.f (ses n)) }} +end + +definition is_exact_LES_of_SESs.{u} {N : succ_str} (A B C : N → LeftModule.{_ u} R) (φ : Πn, A n →lm B n) + (ses : Πn : N, short_exact_mod (cokernel_module (φ (succ_str.S n))) (C n) (kernel_module (φ n))) : + is_exact (LES_of_SESs A B C φ ses) := +begin + intros x m p, induction x with n k, induction k with k H, do 3 (cases k with k; rotate 1), + { exfalso, apply lt_le_antisymm H, apply le_add_left}, + { induction is_short_exact.is_surj (short_exact_mod.h (ses n)) ⟨m, p⟩ with m' q, + exact image.mk m' (ap pr1 q) }, + { induction is_short_exact.ker_in_im (short_exact_mod.h (ses n)) m (subtype_eq p) with m' q, + induction m' using set_quotient.rec_prop with m', + exact image.mk m' q }, + { apply rel_of_quotient_map_eq_zero (image (φ (succ_str.S n))) m, + apply @is_injective_of_is_embedding _ _ _ (is_short_exact.is_emb (short_exact_mod.h (ses n))), + exact p ⬝ (to_respect_zero (short_exact_mod.f (ses n)))⁻¹ } +end + -- remove: -- definition homology.rec (P : homology ψ φ → Type) diff --git a/move_to_lib.hlean b/move_to_lib.hlean index 381cc5f..83e5c09 100644 --- a/move_to_lib.hlean +++ b/move_to_lib.hlean @@ -157,6 +157,10 @@ end sigma open sigma namespace group + definition group_homomorphism_of_add_group_homomorphism [constructor] {G₁ G₂ : AddGroup} + (φ : G₁ →a G₂) : G₁ →g G₂ := + φ + -- definition is_equiv_isomorphism