From 78860cb98aea953372e14bc29cd5dc5b35c5fc41 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 21:09:49 +0000 Subject: [PATCH 1/4] better subgroup_generated_rec lemma Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index 84a692b804..a9b0f614f8 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -557,20 +557,28 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H : : subgroup_generated X := (g; tr (sgt_in H)). +Definition subgroup_generated_rec {G H : Group} (X : G -> Type) (S : Subgroup H) + (f : G $-> H) (i : forall x, X x -> S (f x)) + : forall x, subgroup_generated X x -> S (f x). +Proof. + intros x; rapply Trunc_rec; intros p. + induction p as [g Xg | | g h p1 IHp1 p2 IHp2]. + - by apply i. + - rewrite grp_homo_unit. + apply subgroup_in_unit. + - rewrite grp_homo_op, grp_homo_inv. + by apply subgroup_in_op_inv. +Defined. + (** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *) Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type) (f : G $-> H) (preserves : forall g, X g -> Y (f g)) : forall g, subgroup_generated X g -> subgroup_generated Y (f g). Proof. - intro g. - apply Trunc_functor. - intro p. - induction p as [g i | | g h p1 IHp1 p2 IHp2]. - - apply sgt_in, preserves, i. - - rewrite grp_homo_unit. - apply sgt_unit. - - rewrite grp_homo_op, grp_homo_inv. - by apply sgt_op. + apply subgroup_generated_rec. + intros g x. + apply tr, sgt_in. + by apply preserves. Defined. (** The product of two subgroups. *) From 6b99b15ad7081171b15f4b3cb728790dfee6ce1a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 22:37:25 +0000 Subject: [PATCH 2/4] change x to g Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index a9b0f614f8..5e99889665 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -558,10 +558,10 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H : := (g; tr (sgt_in H)). Definition subgroup_generated_rec {G H : Group} (X : G -> Type) (S : Subgroup H) - (f : G $-> H) (i : forall x, X x -> S (f x)) - : forall x, subgroup_generated X x -> S (f x). + (f : G $-> H) (i : forall g, X g -> S (f g)) + : forall g, subgroup_generated X g -> S (f g). Proof. - intros x; rapply Trunc_rec; intros p. + intros g; rapply Trunc_rec; intros p. induction p as [g Xg | | g h p1 IHp1 p2 IHp2]. - by apply i. - rewrite grp_homo_unit. From 10b911ba3dd136991b8020a0a24cc23aa3008945 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 22:50:08 +0000 Subject: [PATCH 3/4] rename variables Signed-off-by: Ali Caglayan --- 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 5e99889665..b4cfa7aeff 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -576,7 +576,7 @@ Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Ty : forall g, subgroup_generated X g -> subgroup_generated Y (f g). Proof. apply subgroup_generated_rec. - intros g x. + intros g p. apply tr, sgt_in. by apply preserves. Defined. From 88934ed4780c40657e070f7c6bec130f51f2bd76 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Fri, 3 Jan 2025 22:55:26 +0000 Subject: [PATCH 4/4] simplify subgroup_generated_rec further and add comment Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Subgroup.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v index b4cfa7aeff..da08b1d317 100644 --- a/theories/Algebra/Groups/Subgroup.v +++ b/theories/Algebra/Groups/Subgroup.v @@ -557,17 +557,16 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H : : subgroup_generated X := (g; tr (sgt_in H)). -Definition subgroup_generated_rec {G H : Group} (X : G -> Type) (S : Subgroup H) - (f : G $-> H) (i : forall g, X g -> S (f g)) - : forall g, subgroup_generated X g -> S (f g). +(** The generated subgroup is the smallest subgroup containing the generating set. *) +Definition subgroup_generated_rec {G : Group} (X : G -> Type) (S : Subgroup G) + (i : forall g, X g -> S g) + : forall g, subgroup_generated X g -> S g. Proof. intros g; rapply Trunc_rec; intros p. induction p as [g Xg | | g h p1 IHp1 p2 IHp2]. - by apply i. - - rewrite grp_homo_unit. - apply subgroup_in_unit. - - rewrite grp_homo_op, grp_homo_inv. - by apply subgroup_in_op_inv. + - apply subgroup_in_unit. + - by apply subgroup_in_op_inv. Defined. (** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *) @@ -575,6 +574,8 @@ Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Ty (f : G $-> H) (preserves : forall g, X g -> Y (f g)) : forall g, subgroup_generated X g -> subgroup_generated Y (f g). Proof. + change (subgroup_generated Y (f ?g)) + with (subgroup_preimage f (subgroup_generated Y) g). apply subgroup_generated_rec. intros g p. apply tr, sgt_in.