From 94f8ac7f3ffb56c59ebe1986a98e507ac50d21fb Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 19:37:26 +0100 Subject: [PATCH] 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 *)