From aa3fc44aee5f8fa7d92d5f5c75e474cbe254508e Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 03:57:31 +0100 Subject: [PATCH] lemmas about subgroup_product Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 24608bd39b..63d615ad8a 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -641,7 +641,7 @@ Defined. (** The product of two subgroups. *) Definition subgroup_product {G : Group} (H K : Subgroup G) : Subgroup G - := subgroup_generated (fun x => ((H x) + (K x))%type). + := subgroup_generated (fun x => (H x + K x)%type). (** The induction principle for the product. *) Definition subgroup_product_ind {G : Group} (H K : Subgroup G) @@ -663,6 +663,30 @@ Proof. + by apply P_op. Defined. +Definition subgroup_product_incl_l {G : Group} (H K : Subgroup G) + : forall x, H x -> subgroup_product H K x + := fun x => tr o sgt_in o inl. + +Definition subgroup_product_incl_r {G : Group} (H K : Subgroup G) + : forall x, K x -> subgroup_product H K x + := fun x => tr o sgt_in o inr. + +(** A product of normal subgroups is normal. *) +Global Instance isnormal_subgroup_product {G : Group} (H K : Subgroup G) + `{!IsNormalSubgroup H, !IsNormalSubgroup K} + : IsNormalSubgroup (subgroup_product H K). +Proof. + snrapply Build_IsNormalSubgroup'. + intros x y; revert x. + nrapply (functor_subgroup_generated _ _ (grp_conj y)). + intros x. + apply functor_sum; rapply isnormal_conj. +Defined. + +Definition normalsubgroup_product {G : Group} (H K : NormalSubgroup G) + : NormalSubgroup G + := Build_NormalSubgroup G (subgroup_product H K) _. + (* **** Paths between generated subgroups *) (* This gets used twice in [path_subgroup_generated], so we factor it out here. *)