From 752d5327197eb92cf048bf11feedcfeed64c42a6 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 16:11:03 +0100 Subject: [PATCH 1/3] minor cleanup in quotient group Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/QuotientGroup.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v index 21ea46dd7e..4aebf2f80b 100644 --- a/theories/Algebra/Groups/QuotientGroup.v +++ b/theories/Algebra/Groups/QuotientGroup.v @@ -253,9 +253,8 @@ Section FirstIso. snrapply isequiv_surj_emb. 1: srapply cancelR_conn_map. srapply isembedding_isinj_hset. - refine (Quotient_ind_hprop _ _ _); intro x. - refine (Quotient_ind_hprop _ _ _); intro y. - intros h; simpl in h. + srapply Quotient_ind2_hprop. + intros x y h; simpl in h. apply qglue; cbn. apply (equiv_path_sigma_hprop _ _)^-1%equiv in h; cbn in h. cbn. rewrite grp_homo_op, grp_homo_inv, h. From 0f268e72f293c3fee6f765a147225d58088c7e78 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Wed, 15 Jan 2025 19:55:30 +0100 Subject: [PATCH 2/3] minor style tweak in Group.v Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Group.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 4eabe756de..c48c7ce291 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -930,7 +930,7 @@ Definition grp_prod_corec_natural {X Y A B : Group} (** The left factor injects into the direct product. *) Definition grp_prod_inl {H K : Group} - : H $-> (grp_prod H K) + : H $-> grp_prod H K := grp_prod_corec grp_homo_id grp_homo_const. (** The left injection is an embedding. *) @@ -944,7 +944,7 @@ Defined. (** The right factor injects into the direct product. *) Definition grp_prod_inr {H K : Group} - : K $-> (grp_prod H K) + : K $-> grp_prod H K := grp_prod_corec grp_homo_const grp_homo_id. (** The right injection is an embedding. *) From 3cdf2c672a9e89fd9bf7d2ed5ba43dc9c43a4c95 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 16 Jan 2025 01:00:27 +0100 Subject: [PATCH 3/3] style tweak in grp_prod_decompose Signed-off-by: Ali Caglayan --- theories/Algebra/Groups/Group.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index c48c7ce291..3281b94a9e 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -995,7 +995,7 @@ Defined. (** Pairs in direct products can be decomposed *) Definition grp_prod_decompose {G H : Group} (g : G) (h : H) - : (g, h) = ((g, group_unit) : grp_prod G H) * (group_unit, h). + : (g, h) = ((g, 1) : grp_prod G H) * (1, h). Proof. snrapply path_prod; symmetry. - snrapply grp_unit_r.