From fb5254172027636770f4b0621161227707619567 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 21:07:59 +0000 Subject: [PATCH] sugroup_group of maximal_subgroup is iso to original group Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 0878378979..6b3f35ea63 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -222,6 +222,15 @@ Defined. Coercion maximal_subgroup : Group >-> Subgroup. Add Printing Coercion maximal_subgroup. +(** The group inferred from 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).