From 371818002029419c4320bbb48da278a2001ba0d5 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 03:59:48 +0100 Subject: [PATCH 1/6] subgroup_group iso lemmas and all trivial subgroups are iso Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 49 ++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index b2c764ae06..54b98696f9 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -177,6 +177,37 @@ Global Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G) Definition issig_subgroup {G : Group} : _ <~> Subgroup G := ltac:(issig). +Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H} + (f : G $-> H) (g : forall x, J x -> K (f x)) + : subgroup_group J $-> subgroup_group K. +Proof. + snrapply Build_GroupHomomorphism. + - exact (functor_sigma f g). + - intros x y. + rapply path_sigma_hprop. + snrapply grp_homo_op. +Defined. + +Definition grp_iso_subgroup_group {G H : Group@{i}} + {J : Subgroup@{i i} G} (K : Subgroup@{i i} H) + (e : G $<~> H) (f : forall x, J x <-> K (e x)) + : subgroup_group J $<~> subgroup_group K. +Proof. + snrapply cate_adjointify. + - exact (functor_subgroup_group e (fun x => fst (f x))). + - nrefine (functor_subgroup_group e^-1$ _). + equiv_intro e x. + intros k. + nrefine ((eissect e _)^ # _). + exact (snd (f x) k). + - intros x. + rapply path_sigma_hprop. + nrapply eisretr. + - intros x. + rapply path_sigma_hprop. + nrapply eissect. +Defined. + (** Trivial subgroup *) Definition trivial_subgroup G : Subgroup G. Proof. @@ -195,6 +226,24 @@ Proof. apply issubgroup_in_unit. Defined. +(** All trivial subgroups are isomorphic as groups. *) +Definition grp_iso_trivial_subgroup (G H : Group) + : subgroup_group (trivial_subgroup G) + $<~> subgroup_group (trivial_subgroup H). +Proof. + snrapply cate_adjointify. + - snrapply functor_subgroup_group. + + exact grp_homo_const. + + reflexivity. + - snrapply functor_subgroup_group. + + exact grp_homo_const. + + reflexivity. + - intros [x p]; rapply path_sigma_hprop. + symmetry; exact p. + - intros [x p]; rapply path_sigma_hprop. + symmetry; exact p. +Defined. + (** The preimage of a subgroup under a group homomorphism is a subgroup. *) Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H) : Subgroup G. From efda7ad62f30d2f7057324976c6db8de058826a7 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Wed, 15 Jan 2025 10:09:09 -0500 Subject: [PATCH 2/6] Subgroup: simplify grp_iso_trivial_subgroup --- theories/Algebra/Groups/Subgroup.v | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 54b98696f9..863ff0ec0f 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -232,12 +232,7 @@ Definition grp_iso_trivial_subgroup (G H : Group) $<~> subgroup_group (trivial_subgroup H). Proof. snrapply cate_adjointify. - - snrapply functor_subgroup_group. - + exact grp_homo_const. - + reflexivity. - - snrapply functor_subgroup_group. - + exact grp_homo_const. - + reflexivity. + 1,2: exact grp_homo_const. - intros [x p]; rapply path_sigma_hprop. symmetry; exact p. - intros [x p]; rapply path_sigma_hprop. @@ -553,7 +548,7 @@ Proof. exact p. Defined. -(** The property of being the trivial group is useful. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *) +(** The property of being the trivial subgroup. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *) Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) := istrivialgroup : forall x, H x -> trivial_subgroup G x. From b4d907cb30413ed358ada73369fe9d0f8becf333 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 17:43:32 +0100 Subject: [PATCH 3/6] simplify and rename istrivial_iff_grp_iso_trivial Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 27 ++++++++++++--------------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 863ff0ec0f..a0b58e3f99 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -561,23 +561,20 @@ Global Instance istrivial_trivial_subgroup {G : Group} := fun x => idmap. (** Trivial groups are isomorphic to the trivial group. *) -Definition istrivial_iff_grp_iso_trivial_subgroup {G : Group} (H : Subgroup G) - : IsTrivialGroup H - <-> (subgroup_group H $<~> subgroup_group (trivial_subgroup G)). +Definition istrivial_iff_grp_iso_trivial {G : Group} (H : Subgroup G) + : IsTrivialGroup H <-> (subgroup_group H $<~> grp_trivial). Proof. split. - - intros T. - snrapply Build_GroupIsomorphism'. - + snrapply equiv_functor_sigma_id. - intros x. - rapply equiv_iff_hprop_uncurried. - split; only 1: apply T. - apply trivial_subgroup_rec. - + intros [x Hx] [y Hy]. - by rapply path_sigma_hprop. - - unfold IsTrivialGroup. - intros e x h. - change ((x; h).1 = (1; idpath).1). + - intros triv. + snrapply cate_adjointify. + 1,2: exact grp_homo_const. + + by intros []. + + intros [x Hx]; simpl. + apply path_sigma_hprop. + symmetry. + by apply triv. + - intros e x Hx. + change ((x; Hx).1 = (1; idpath).1). snrapply (pr1_path (u:=(_;_)) (v:=(_;_))). 1: apply subgroup_in_unit. rhs_V nrapply (grp_homo_unit e^-1$). From 772137fb81d8a8c53259b5181c87d6b5d7c14fd6 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 17:50:27 +0100 Subject: [PATCH 4/6] reorganise trivial and maximal subgroup material and simplify Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 142 +++++++++++++++-------------- 1 file changed, 73 insertions(+), 69 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index a0b58e3f99..b9f732e65b 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -208,37 +208,6 @@ Proof. nrapply eissect. Defined. -(** Trivial subgroup *) -Definition trivial_subgroup G : Subgroup G. -Proof. - rapply (Build_Subgroup' (fun x => x = mon_unit)). - 1: reflexivity. - intros x y p q. - rewrite p, q. - rewrite left_identity. - apply inverse_mon_unit. -Defined. - -Definition trivial_subgroup_rec {G : Group} (H : Subgroup G) - : forall x, trivial_subgroup G x -> H x. -Proof. - snrapply paths_ind_r; cbn beta. - apply issubgroup_in_unit. -Defined. - -(** All trivial subgroups are isomorphic as groups. *) -Definition grp_iso_trivial_subgroup (G H : Group) - : subgroup_group (trivial_subgroup G) - $<~> subgroup_group (trivial_subgroup H). -Proof. - snrapply cate_adjointify. - 1,2: exact grp_homo_const. - - intros [x p]; rapply path_sigma_hprop. - symmetry; exact p. - - intros [x p]; rapply path_sigma_hprop. - symmetry; exact p. -Defined. - (** The preimage of a subgroup under a group homomorphism is a subgroup. *) Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H) : Subgroup G. @@ -255,26 +224,6 @@ Proof. by apply subgroup_in_inv. Defined. -(** Every group is a (maximal) subgroup of itself *) -Definition maximal_subgroup G : Subgroup G. -Proof. - rapply (Build_Subgroup G (fun x => Unit)). - split; auto; exact _. -Defined. - -(** We wish to coerce a group to its maximal subgroup. However, if we don't explicitly print [maximal_subgroup] things can get confusing, so we mark it as a coercion to be printed. *) -Coercion maximal_subgroup : Group >-> Subgroup. -Add Printing Coercion maximal_subgroup. - -(** The group associated to the maximal subgroup is the original group. *) -Definition grp_iso_subgroup_group_maximal (G : Group) - : subgroup_group (maximal_subgroup G) $<~> G. -Proof. - snrapply Build_GroupIsomorphism'. - - rapply equiv_sigma_contr. - - hnf; reflexivity. -Defined. - (** Paths between subgroups correspond to homotopies between the underlying predicates. *) Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G) : (H == K) <~> (H = K). @@ -480,22 +429,6 @@ Proof. by snrapply Build_IsNormalSubgroup'. Defined. -(** The trivial subgroup is a normal subgroup. *) -Global Instance isnormal_trivial_subgroup {G : Group} - : IsNormalSubgroup (trivial_subgroup G). -Proof. - intros x y p; cbn in p |- *. - apply grp_moveL_1V in p. - by apply grp_moveL_V1. -Defined. - -(** The maximal subgroup (the group itself) is a normal subgroup. *) -Global Instance isnormal_maximal_subgroup {G : Group} - : IsNormalSubgroup (maximal_subgroup G). -Proof. - intros x y p; exact tt. -Defined. - (** Left and right cosets are equivalent in normal subgroups. *) Definition equiv_in_cosetL_in_cosetR_normalsubgroup {G : Group} (N : NormalSubgroup G) (x y : G) @@ -548,6 +481,36 @@ Proof. exact p. Defined. +(** *** Trivial subgroup *) + +(** The trivial subgroup of a group [G]. *) +Definition trivial_subgroup G : Subgroup G. +Proof. + rapply (Build_Subgroup' (fun x => x = 1)). + 1: reflexivity. + intros x y p q. + rewrite p, q. + rewrite left_identity. + apply grp_inv_unit. +Defined. + +(** The trivial subgroup is always included in any subgroup. *) +Definition trivial_subgroup_rec {G : Group} (H : Subgroup G) + : forall x, trivial_subgroup G x -> H x. +Proof. + snrapply paths_ind_r; cbn beta. + apply issubgroup_in_unit. +Defined. + +(** The trivial subgroup is a normal subgroup. *) +Global Instance isnormal_trivial_subgroup {G : Group} + : IsNormalSubgroup (trivial_subgroup G). +Proof. + intros x y p; cbn in p |- *. + apply grp_moveL_1V in p. + by apply grp_moveL_V1. +Defined. + (** The property of being the trivial subgroup. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *) Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) := istrivialgroup : forall x, H x -> trivial_subgroup G x. @@ -582,7 +545,46 @@ Proof. apply path_contr. Defined. -(** A maximal subgroup of a group [G] is a subgroup where every element of [G] is included. *) +(** All trivial subgroups are isomorphic as groups. *) +Definition grp_iso_trivial_subgroup (G H : Group) + : subgroup_group (trivial_subgroup G) + $<~> subgroup_group (trivial_subgroup H). +Proof. + snrefine (_^-1$ $oE _). + 1: exact grp_trivial. + 1,2: apply istrivial_iff_grp_iso_trivial; exact _. +Defined. + +(** *** Maximal Subgroups *) + +(** Every group is a (maximal) subgroup of itself *) +Definition maximal_subgroup G : Subgroup G. +Proof. + rapply (Build_Subgroup G (fun x => Unit)). + split; auto; exact _. +Defined. + +(** We wish to coerce a group to its maximal subgroup. However, if we don't explicitly print [maximal_subgroup] things can get confusing, so we mark it as a coercion to be printed. *) +Coercion maximal_subgroup : Group >-> Subgroup. +Add Printing Coercion maximal_subgroup. + +(** The group associated to the maximal subgroup is the original group. *) +Definition grp_iso_subgroup_group_maximal (G : Group) + : subgroup_group (maximal_subgroup G) $<~> G. +Proof. + snrapply Build_GroupIsomorphism'. + - rapply equiv_sigma_contr. + - hnf; reflexivity. +Defined. + +(** The maximal subgroup (the group itself) is a normal subgroup. *) +Global Instance isnormal_maximal_subgroup {G : Group} + : IsNormalSubgroup (maximal_subgroup G). +Proof. + intros x y p; exact tt. +Defined. + +(** The property of being a maximal subgroup of a group [G]. *) Class IsMaximalSubgroup {G : Group} (H : Subgroup G) := ismaximalsubgroup : forall (x : G), H x. @@ -595,7 +597,9 @@ Global Instance ismaximalsubgroup_maximalsubgroup {G : Group} : IsMaximalSubgroup (maximal_subgroup G) := fun g => tt. -(** Note that we don't have an analogue for [istrivial_iff_grp_iso_trivial_group] since a proper subgroup of a group may be isomorphic to the entire group, whilst still being different from the maximal subgroup. The example to keep in mind is the group of integers [Z] and the subgroup of even integers [2Z]. Clearly, the integers are isomorphic to the even integers as groups, however the even integers are not equal to the maximal subgroup. *) +(** Note that we don't have an analogue for [istrivial_iff_grp_iso_trivial] since a proper subgroup of a group may be isomorphic to the entire group, whilst still being different from the maximal subgroup. The example to keep in mind is the group of integers [Z] and the subgroup of even integers [2Z]. Clearly, the integers are isomorphic to the even integers as groups, however the even integers are not equal to the maximal subgroup. *) + +(** *** Subgroup intersection *) (** Intersection of two subgroups *) Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G. From 9dbb8e59185dcf20a04817da199bcd03bb61de81 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 19:35:34 +0100 Subject: [PATCH 5/6] Update theories/Algebra/Groups/Subgroup.v Co-authored-by: Dan Christensen --- theories/Algebra/Groups/Subgroup.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index b9f732e65b..29f420e32e 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -557,7 +557,7 @@ Defined. (** *** Maximal Subgroups *) -(** Every group is a (maximal) subgroup of itself *) +(** Every group is a (maximal) subgroup of itself. *) Definition maximal_subgroup G : Subgroup G. Proof. rapply (Build_Subgroup G (fun x => Unit)). From 94f8ac7f3ffb56c59ebe1986a98e507ac50d21fb Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 19:37:26 +0100 Subject: [PATCH 6/6] update comment mentioning proper subgroups being isomorphic Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 29f420e32e..0ebeb032cc 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -568,7 +568,7 @@ Defined. Coercion maximal_subgroup : Group >-> Subgroup. Add Printing Coercion maximal_subgroup. -(** The group associated to the maximal subgroup is the original group. *) +(** The group associated to the maximal subgroup is the original group. Note that this equivalence does not characterize the maximal subgroup, as a proper subgroup can be isomorphic to the whole group. For example, the even integers are isomorphic to the integers. *) Definition grp_iso_subgroup_group_maximal (G : Group) : subgroup_group (maximal_subgroup G) $<~> G. Proof. @@ -597,8 +597,6 @@ Global Instance ismaximalsubgroup_maximalsubgroup {G : Group} : IsMaximalSubgroup (maximal_subgroup G) := fun g => tt. -(** Note that we don't have an analogue for [istrivial_iff_grp_iso_trivial] since a proper subgroup of a group may be isomorphic to the entire group, whilst still being different from the maximal subgroup. The example to keep in mind is the group of integers [Z] and the subgroup of even integers [2Z]. Clearly, the integers are isomorphic to the even integers as groups, however the even integers are not equal to the maximal subgroup. *) - (** *** Subgroup intersection *) (** Intersection of two subgroups *)