From fa2fc2c0213f5403ff194430827b6b31aef91fe1 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 9 Oct 2025 10:50:30 +0200 Subject: [PATCH 1/3] more carefully split groups --- theories/Algebra/Groups/FreeGroup.v | 9 +++- theories/Algebra/Groups/FreeProduct.v | 9 +++- theories/Algebra/Groups/Group.v | 15 +++---- theories/Homotopy/HomotopyGroup.v | 59 ++++++++++++++------------- 4 files changed, 54 insertions(+), 38 deletions(-) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 1e7165a780..62a46d0613 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -241,7 +241,14 @@ Section Reduction. (** Finally we have defined the free group on [A] *) Definition FreeGroup : Group. Proof. - snapply (Build_Group freegroup_type); repeat split; exact _. + snapply (Build_Group freegroup_type). + - exact _. + - exact _. + - exact _. + - split. + + repeat split; exact _. + + exact _. + + exact _. Defined. Definition word_rec (G : Group) (s : A -> G) : A + A -> G. diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 4926462ef0..23b56f6f10 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -524,7 +524,14 @@ Section AmalgamatedFreeProduct. Definition AmalgamatedFreeProduct : Group. Proof. - snapply (Build_Group amal_type); repeat split; exact _. + snapply (Build_Group amal_type). + - exact _. + - exact _. + - exact _. + - split. + + repeat split; exact _. + + exact _. + + exact _. Defined. End AmalgamatedFreeProduct. diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v index 9e3ca71757..953e0d6eda 100644 --- a/theories/Algebra/Groups/Group.v +++ b/theories/Algebra/Groups/Group.v @@ -969,17 +969,18 @@ Definition grp_prod : Group -> Group -> Group. Proof. intros G H. snapply (Build_Group (G * H)). - 4: repeat split. - intros [g1 h1] [g2 h2]. exact (g1 * g2, h1 * h2). - exact (1, 1). - exact (functor_prod inv inv). - - exact _. - - intros x y z; apply path_prod'; apply simple_associativity. - - intros x; apply path_prod'; apply left_identity. - - intros x; apply path_prod'; apply right_identity. - - intros x; apply path_prod'; apply left_inverse. - - intros x; apply path_prod'; apply right_inverse. + - split. + + repeat split. + * exact _. + * intros x y z; apply path_prod'; apply simple_associativity. + * intros x; apply path_prod'; apply left_identity. + * intros x; apply path_prod'; apply right_identity. + + intros x; apply path_prod'; apply left_inverse. + + intros x; apply path_prod'; apply right_inverse. Defined. (** Maps into the direct product can be built by mapping separately into each factor. *) diff --git a/theories/Homotopy/HomotopyGroup.v b/theories/Homotopy/HomotopyGroup.v index 1aeb127db1..9071a90b2b 100644 --- a/theories/Homotopy/HomotopyGroup.v +++ b/theories/Homotopy/HomotopyGroup.v @@ -46,8 +46,7 @@ Instance is1functor_homotopygroup_type_ptype (n : nat) definitionally equal to [Pi 1 (iterated_loops n X)] *) Definition Pi1 (X : pType) : Group. Proof. - srapply (Build_Group (Tr 0 (loops X))); - repeat split. + srapply (Build_Group (Tr 0 (loops X))). (** Operation *) - intros x y. strip_truncations. @@ -57,33 +56,35 @@ Proof. (** Inverse *) - srapply Trunc_rec; intro x. exact (tr x^). - (** [IsHSet] *) - - exact _. - (** Associativity *) - - intros x y z. - strip_truncations. - cbn; apply ap. - apply concat_p_pp. - (** Left identity *) - - intro x. - strip_truncations. - cbn; apply ap. - apply concat_1p. - (** Right identity *) - - intro x. - strip_truncations. - cbn; apply ap. - apply concat_p1. - (** Left inverse *) - - intro x. - strip_truncations. - apply (ap tr). - apply concat_Vp. - (** Right inverse *) - - intro x. - strip_truncations. - apply (ap tr). - apply concat_pV. + - split. + + repeat split. + (** [IsHSet] *) + * exact _. + (** Associativity *) + * intros x y z. + strip_truncations. + cbn; apply ap. + apply concat_p_pp. + (** Left identity *) + * intro x. + strip_truncations. + cbn; apply ap. + apply concat_1p. + (** Right identity *) + * intro x. + strip_truncations. + cbn; apply ap. + apply concat_p1. + (** Left inverse *) + + intro x. + strip_truncations. + apply (ap tr). + apply concat_Vp. + (** Right inverse *) + + intro x. + strip_truncations. + apply (ap tr). + apply concat_pV. Defined. (** Definition of the nth homotopy group *) From 872ba2dad47347359cff71a3a63798a111176906 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 9 Oct 2025 17:13:44 +0200 Subject: [PATCH 2/3] shorter fix --- theories/Algebra/Groups/FreeGroup.v | 9 ++------- theories/Algebra/Groups/FreeProduct.v | 9 ++------- 2 files changed, 4 insertions(+), 14 deletions(-) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 62a46d0613..6b7a3e41a6 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -242,13 +242,8 @@ Section Reduction. Definition FreeGroup : Group. Proof. snapply (Build_Group freegroup_type). - - exact _. - - exact _. - - exact _. - - split. - + repeat split; exact _. - + exact _. - + exact _. + 4: split. 4: repeat split. + all: exact _. Defined. Definition word_rec (G : Group) (s : A -> G) : A + A -> G. diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 23b56f6f10..4656220240 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -525,13 +525,8 @@ Section AmalgamatedFreeProduct. Definition AmalgamatedFreeProduct : Group. Proof. snapply (Build_Group amal_type). - - exact _. - - exact _. - - exact _. - - split. - + repeat split; exact _. - + exact _. - + exact _. + 4: split. 4: repeat split. + all: exact _. Defined. End AmalgamatedFreeProduct. From 2a5e2c8a974ac89d79ba3257192bb018db0a285c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 10 Oct 2025 11:37:00 +0200 Subject: [PATCH 3/3] even shorter fix --- theories/Algebra/Groups/FreeGroup.v | 4 +--- theories/Algebra/Groups/FreeProduct.v | 4 +--- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/theories/Algebra/Groups/FreeGroup.v b/theories/Algebra/Groups/FreeGroup.v index 6b7a3e41a6..49eb0f190a 100644 --- a/theories/Algebra/Groups/FreeGroup.v +++ b/theories/Algebra/Groups/FreeGroup.v @@ -241,9 +241,7 @@ Section Reduction. (** Finally we have defined the free group on [A] *) Definition FreeGroup : Group. Proof. - snapply (Build_Group freegroup_type). - 4: split. 4: repeat split. - all: exact _. + srapply (Build_Group freegroup_type sgop_freegroup); repeat split; exact _. Defined. Definition word_rec (G : Group) (s : A -> G) : A + A -> G. diff --git a/theories/Algebra/Groups/FreeProduct.v b/theories/Algebra/Groups/FreeProduct.v index 4656220240..d4aaf7accc 100644 --- a/theories/Algebra/Groups/FreeProduct.v +++ b/theories/Algebra/Groups/FreeProduct.v @@ -524,9 +524,7 @@ Section AmalgamatedFreeProduct. Definition AmalgamatedFreeProduct : Group. Proof. - snapply (Build_Group amal_type). - 4: split. 4: repeat split. - all: exact _. + snapply (Build_Group amal_type sgop_amal_type); repeat split; exact _. Defined. End AmalgamatedFreeProduct.