From 9e50a905a737f1cb3cb685fcd02e6dc75a55482e Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Wed, 15 Jan 2025 16:11:17 +0100
Subject: [PATCH 01/14] image of a subgroup

<!-- ps-id: a131ab0f-2a90-4e3c-86d0-37a687960d7b -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Groups/Subgroup.v | 86 +++++++++++++++++++++++++++++-
 1 file changed, 85 insertions(+), 1 deletion(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 78a49bc07a..c861b87726 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -1,5 +1,5 @@
 Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
-Require Import Truncations.Core.
+Require Import Truncations.Core Modalities.ReflectiveSubuniverse.
 Require Import Algebra.Groups.Group TruncType.
 
 Local Open Scope mc_scope.
@@ -808,3 +808,87 @@ Defined.
 Definition equiv_subgroup_group {G : Group} (H1 H2 : Subgroup G)
   : H1 = H2 -> GroupIsomorphism H1 H2
   := ltac:(intros []; exact grp_iso_id).
+
+(** ** Image of a subgroup under a group homomoprhism *)
+
+(** The image of a subgroup under group homomorphism. *) 
+Definition subgroup_image {G H : Group} (f : G $-> H) : Subgroup G -> Subgroup H.
+Proof.
+  intros J.
+  snrapply Build_Subgroup'.
+  - exact (fun b => hexists (fun (j : J) => f j.1 = b)).
+  - exact _.
+  - apply tr.
+    exists 1.
+    apply grp_homo_unit.
+  - intros x y p q; strip_truncations; apply tr.
+    destruct p as [a p], q as [b q].
+    exists (a * b^).
+    lhs nrapply grp_homo_op; f_ap.
+    lhs nrapply grp_homo_inv; f_ap.
+Defined.
+
+(** By definition, values of [f x] where [x] is in a subgroup [J] are in the image of [J] under [f]. *)
+Definition subgroup_image_in {G H : Group} (f : G $-> H) (J : Subgroup G)
+  : forall x, J x -> subgroup_image f J (f x)
+  := fun x Jx => tr ((x; Jx); idpath).
+
+(** Converting the subgroups to groups, we get the expected surjective (epi) restriction homomorphism. *)
+Definition grp_homo_subgroup_image {G H : Group} (f : G $-> H) (J : Subgroup G)
+  : subgroup_group J $-> subgroup_image f J
+  := functor_subgroup_group f (subgroup_image_in _ _).
+
+(** The restriction map from the subgroup to the image is surjective as expected. *)
+Global Instance issurj_grp_homo_subgroup_image {G H : Group}
+  (f : G $-> H) (J : Subgroup G)
+  : IsSurjection (grp_homo_subgroup_image f J).
+Proof.
+  snrapply BuildIsSurjection.
+  intros [x p].
+  strip_truncations; apply tr.
+  exists p.1.
+  rapply path_sigma_hprop.
+  exact p.2.
+Defined.
+
+(** An image of a subgroup [J] is included in a subgroup [J] if (and only if) the [J] is included in the preimage of the subgroup [K]. *) 
+Definition subgroup_image_rec {G H : Group}
+  (f : G $-> H) {J : Subgroup G} {K : Subgroup H}
+  (g : forall x, J x -> K (f x))
+  : forall x, subgroup_image f J x -> K x.
+Proof.
+  intros x; apply Trunc_rec; intros [[j Jj] p].
+  destruct p.
+  exact (g j Jj).
+Defined.
+
+(** The image functor is adjoint to the preimage functor. *) 
+Definition iff_subgroup_image_rec {G H : Group}
+  (f : G $-> H) {J : Subgroup G} {K : Subgroup H}
+  : (forall x, subgroup_image f J x -> K x)
+    <-> (forall x, J x -> subgroup_preimage f K x).
+Proof.
+  split.
+  - intros rec x Jx.
+    apply rec, tr.
+    by exists (x; Jx).
+  - snrapply subgroup_image_rec.
+Defined.
+
+(** [subgorup_image] preserves normal subgroups when the group homomorphism is surjective. *)
+Global Instance isnormal_subgroup_image {G H : Group} (f : G $-> H)
+  (J : Subgroup G) `{!IsNormalSubgroup J} `{!IsSurjection f}
+  : IsNormalSubgroup (subgroup_image f J).
+Proof.
+  snrapply Build_IsNormalSubgroup'.
+  intros x y; revert x.
+  change (subgroup_image f J (y * ?x * y^))
+    with (subgroup_preimage (grp_conj y) (subgroup_image f J) x).
+  snrapply subgroup_image_rec.
+  intros x Jx.
+  change (subgroup_image f J ((grp_conj y $o f) x)).
+  revert y; rapply (conn_map_elim (Tr (-1)) f); intros y.
+  rewrite <- grp_homo_conj.
+  nrapply subgroup_image_in.
+  by rapply isnormal_conj.
+Defined.

From f6f20fe32612ef3c05a5c42f168b2dd3fa24646d Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 20 Jan 2025 11:24:07 -0500
Subject: [PATCH 02/14] Subgroup: use conn_map_factor1_image and fix comment

---
 theories/Algebra/Groups/Subgroup.v | 17 +++++------------
 1 file changed, 5 insertions(+), 12 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index c861b87726..3ec45ed416 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -1,5 +1,5 @@
 Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
-Require Import Truncations.Core Modalities.ReflectiveSubuniverse.
+Require Import Truncations.Core Modalities.ReflectiveSubuniverse Modalities.Modality.
 Require Import Algebra.Groups.Group TruncType.
 
 Local Open Scope mc_scope.
@@ -838,20 +838,13 @@ Definition grp_homo_subgroup_image {G H : Group} (f : G $-> H) (J : Subgroup G)
   : subgroup_group J $-> subgroup_image f J
   := functor_subgroup_group f (subgroup_image_in _ _).
 
-(** The restriction map from the subgroup to the image is surjective as expected. *)
+(** The restriction map from the subgroup to the image is surjective as expected, by [conn_map_factor1_image]. *)
 Global Instance issurj_grp_homo_subgroup_image {G H : Group}
   (f : G $-> H) (J : Subgroup G)
-  : IsSurjection (grp_homo_subgroup_image f J).
-Proof.
-  snrapply BuildIsSurjection.
-  intros [x p].
-  strip_truncations; apply tr.
-  exists p.1.
-  rapply path_sigma_hprop.
-  exact p.2.
-Defined.
+  : IsSurjection (grp_homo_subgroup_image f J)
+  := _.
 
-(** An image of a subgroup [J] is included in a subgroup [J] if (and only if) the [J] is included in the preimage of the subgroup [K]. *) 
+(** An image of a subgroup [J] is included in a subgroup [K] if (and only if) [J] is included in the preimage of the subgroup [K]. *)
 Definition subgroup_image_rec {G H : Group}
   (f : G $-> H) {J : Subgroup G} {K : Subgroup H}
   (g : forall x, J x -> K (f x))

From 70d25d9560b48a21851a4c13c808d32bed275ca4 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 08:48:12 +0100
Subject: [PATCH 03/14] export conn_map_factor1_image in Subgroup.v

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Groups/Subgroup.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 3ec45ed416..e9a06b6725 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -1,5 +1,6 @@
 Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
-Require Import Truncations.Core Modalities.ReflectiveSubuniverse Modalities.Modality.
+Require Import Truncations.Core Modalities.Modality.
+Require Export Modalities.Modality (conn_map_factor1_image).
 Require Import Algebra.Groups.Group TruncType.
 
 Local Open Scope mc_scope.
@@ -839,7 +840,7 @@ Definition grp_homo_subgroup_image {G H : Group} (f : G $-> H) (J : Subgroup G)
   := functor_subgroup_group f (subgroup_image_in _ _).
 
 (** The restriction map from the subgroup to the image is surjective as expected, by [conn_map_factor1_image]. *)
-Global Instance issurj_grp_homo_subgroup_image {G H : Group}
+Definition issurj_grp_homo_subgroup_image {G H : Group}
   (f : G $-> H) (J : Subgroup G)
   : IsSurjection (grp_homo_subgroup_image f J)
   := _.

From 2f495e1801df6fd7ad8bfe47a8990d9d8730e0e4 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 08:48:58 +0100
Subject: [PATCH 04/14] make subgroup_group in grp_homo_subgroup_image more
 explicit

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 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 e9a06b6725..39eadd7d3c 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -836,7 +836,7 @@ Definition subgroup_image_in {G H : Group} (f : G $-> H) (J : Subgroup G)
 
 (** Converting the subgroups to groups, we get the expected surjective (epi) restriction homomorphism. *)
 Definition grp_homo_subgroup_image {G H : Group} (f : G $-> H) (J : Subgroup G)
-  : subgroup_group J $-> subgroup_image f J
+  : subgroup_group J $-> subgroup_group (subgroup_image f J)
   := functor_subgroup_group f (subgroup_image_in _ _).
 
 (** The restriction map from the subgroup to the image is surjective as expected, by [conn_map_factor1_image]. *)

From 733b48ad139810222ac17e46480935c26f6807e3 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 09:32:58 +0100
Subject: [PATCH 05/14] absorb Image.v into Subgroup.v

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbGroups/AbPushout.v   |  2 +-
 theories/Algebra/Groups.v               |  1 -
 theories/Algebra/Groups/Image.v         | 73 --------------------
 theories/Algebra/Groups/QuotientGroup.v |  3 +-
 theories/Algebra/Groups/Subgroup.v      | 90 ++++++++++++++++++++++---
 theories/Algebra/Rings/Module.v         |  2 +-
 theories/Algebra/Rings/Ring.v           |  2 +-
 7 files changed, 86 insertions(+), 87 deletions(-)
 delete mode 100644 theories/Algebra/Groups/Image.v

diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v
index 6654c549cc..f4e518fcf3 100644
--- a/theories/Algebra/AbGroups/AbPushout.v
+++ b/theories/Algebra/AbGroups/AbPushout.v
@@ -1,6 +1,6 @@
 Require Import Basics Types Truncations.Core.
 Require Import WildCat.Core HSet.
-Require Export Algebra.Groups.Image Algebra.Groups.QuotientGroup.
+Require Export Algebra.Groups.QuotientGroup.
 Require Import AbGroups.AbelianGroup AbGroups.Biproduct.
 
 Local Open Scope mc_scope.
diff --git a/theories/Algebra/Groups.v b/theories/Algebra/Groups.v
index 89d347bd34..7722aae14c 100644
--- a/theories/Algebra/Groups.v
+++ b/theories/Algebra/Groups.v
@@ -2,7 +2,6 @@
 
 Require Export HoTT.Algebra.Groups.Group.
 Require Export HoTT.Algebra.Groups.Subgroup.
-Require Export HoTT.Algebra.Groups.Image.
 Require Export HoTT.Algebra.Groups.Kernel.
 
 Require Export HoTT.Algebra.Groups.QuotientGroup.
diff --git a/theories/Algebra/Groups/Image.v b/theories/Algebra/Groups/Image.v
deleted file mode 100644
index e5409faed0..0000000000
--- a/theories/Algebra/Groups/Image.v
+++ /dev/null
@@ -1,73 +0,0 @@
-Require Import Basics Types.
-Require Import Truncations.Core.
-Require Import Algebra.Groups.Group.
-Require Import Algebra.Groups.Subgroup.
-Require Import WildCat.Core.
-Require Import HSet.
-
-(** Image of group homomorphisms *)
-
-Local Open Scope mc_scope.
-Local Open Scope mc_mult_scope.
-
-(** The image of a group homomorphism between groups is a subgroup *)
-Definition grp_image {A B : Group} (f : A $-> B) : Subgroup B.
-Proof.
-  snrapply (Build_Subgroup' (fun b => hexists (fun a => f a = b))).
-  - exact _.
-  - apply tr.
-    exists mon_unit.
-    apply grp_homo_unit.
-  - intros x y p q; strip_truncations; apply tr.
-    destruct p as [a p], q as [b q].
-    exists (a * b^).
-    lhs nrapply grp_homo_op; f_ap.
-    lhs nrapply grp_homo_inv; f_ap.
-Defined.
-
-Definition grp_image_in {A B : Group} (f : A $-> B) : A $-> grp_image f.
-Proof.
-  snrapply Build_GroupHomomorphism.
-  { intro x.
-    exists (f x).
-    srapply tr.
-    exists x.
-    reflexivity. }
-  cbn. grp_auto.
-Defined.
-
-(** When the homomorphism is an embedding, we don't need to truncate. *)
-Definition grp_image_embedding {A B : Group} (f : A $-> B) `{IsEmbedding f} : Subgroup B.
-Proof.
-  snrapply (Build_Subgroup _ (hfiber f)).
-  repeat split.
-  - exact _.
-  - exact (mon_unit; grp_homo_unit f).
-  - intros x y [a []] [b []].
-    exists (a * b).
-    apply grp_homo_op.
-  - intros b [a []].
-    exists a^.
-    apply grp_homo_inv.
-Defined.
-
-Definition grp_image_in_embedding {A B : Group} (f : A $-> B) `{IsEmbedding f}
-  : GroupIsomorphism A (grp_image_embedding f).
-Proof.
-  snrapply Build_GroupIsomorphism.
-  - snrapply Build_GroupHomomorphism.
-    + intro x.
-      exists (f x).
-      exists x.
-      reflexivity.
-    + cbn; grp_auto.
-  - apply isequiv_surj_emb.
-    2: apply (cancelL_isembedding (g:=pr1)).
-    intros [b [a p]]; cbn.
-    rapply contr_inhabited_hprop.
-    refine (tr (a; _)).
-    srapply path_sigma'.
-    1: exact p.
-    refine (transport_sigma' _ _ @ _).
-    by apply path_sigma_hprop.
-Defined.
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index c19b207626..a82672afe3 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -3,7 +3,6 @@ Require Import Truncations.Core.
 Require Import Algebra.Congruence.
 Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.Subgroup.
-Require Export Algebra.Groups.Image.
 Require Export Algebra.Groups.Kernel.
 Require Export Colimits.Quotient.
 Require Import HSet.
@@ -292,7 +291,7 @@ Section FirstIso.
     : A / grp_kernel phi $-> grp_image phi.
   Proof.
     srapply grp_quotient_rec.
-    + srapply grp_image_in.
+    + srapply grp_homo_image_in.
     + intros n x.
       by apply path_sigma_hprop.
   Defined.
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 39eadd7d3c..83b9215e36 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -1,7 +1,7 @@
 Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
 Require Import Truncations.Core Modalities.Modality.
 Require Export Modalities.Modality (conn_map_factor1_image).
-Require Import Algebra.Groups.Group TruncType.
+Require Import Algebra.Groups.Group Universes.TruncType Universes.HSet.
 
 Local Open Scope mc_scope.
 Local Open Scope mc_mult_scope.
@@ -216,6 +216,11 @@ Proof.
     nrapply eissect.
 Defined.
 
+(** Restriction of a group homomorphism to a subgroup. *)
+Definition grp_homo_restr {G H : Group} (f : G $-> H) (K : Subgroup G)
+  : subgroup_group K $-> H
+  := f $o subgroup_incl _.
+
 (** The preimage of a subgroup under a group homomorphism is a subgroup. *)
 Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
   : Subgroup G.
@@ -810,15 +815,12 @@ Definition equiv_subgroup_group {G : Group} (H1 H2 : Subgroup G)
   : H1 = H2 -> GroupIsomorphism H1 H2
   := ltac:(intros []; exact grp_iso_id).
 
-(** ** Image of a subgroup under a group homomoprhism *)
+(** ** Image of a group homomorphism *)
 
-(** The image of a subgroup under group homomorphism. *) 
-Definition subgroup_image {G H : Group} (f : G $-> H) : Subgroup G -> Subgroup H.
+(** The image of a group homomorphism between groups is a subgroup. *)
+Definition grp_image {G H : Group} (f : G $-> H) : Subgroup H.
 Proof.
-  intros J.
-  snrapply Build_Subgroup'.
-  - exact (fun b => hexists (fun (j : J) => f j.1 = b)).
-  - exact _.
+  srapply (Build_Subgroup' (fun y => hexists (fun x => f x = y))); cbn beta.
   - apply tr.
     exists 1.
     apply grp_homo_unit.
@@ -829,6 +831,78 @@ Proof.
     lhs nrapply grp_homo_inv; f_ap.
 Defined.
 
+Definition grp_image_in {G H : Group} (f : G $-> H)
+  : forall x, grp_image f (f x).
+Proof.
+  intros x.
+  apply tr.
+  by exists x.
+Defined.
+
+Definition grp_homo_image_in {G H : Group} (f : G $-> H) : G $-> grp_image f.
+Proof.
+  snrapply Build_GroupHomomorphism.
+  - intros x.
+    exists (f x).
+    apply grp_image_in.
+  - intros x y.
+    rapply path_sigma_hprop; simpl.
+    apply grp_homo_op.
+Defined.
+
+(** ** Image of a group embedding *)
+
+(** When the homomorphism is an embedding, we don't need to truncate. *)
+Definition grp_image_embedding {G H : Group} (f : G $-> H) `{IsEmbedding f}
+  : Subgroup H.
+Proof.
+  snrapply (Build_Subgroup _ (hfiber f)).
+  repeat split.
+  - exact _.
+  - exact (mon_unit; grp_homo_unit f).
+  - intros x y [a []] [b []].
+    exists (a * b).
+    apply grp_homo_op.
+  - intros b [a []].
+    exists a^.
+    apply grp_homo_inv.
+Defined.
+
+Definition grp_image_in_embedding {G H : Group} (f : G $-> H) `{IsEmbedding f}
+  : GroupIsomorphism G (grp_image_embedding f).
+Proof.
+  snrapply Build_GroupIsomorphism.
+  - snrapply Build_GroupHomomorphism.
+    + intro x.
+      by exists (f x), x.
+    + cbn; grp_auto.
+  - apply isequiv_surj_emb.
+    2: apply (cancelL_isembedding (g:=pr1)).
+    intros [b [a p]]; cbn.
+    rapply contr_inhabited_hprop.
+    refine (tr (a; _)).
+    srapply path_sigma'.
+    1: exact p.
+    refine (transport_sigma' _ _ @ _).
+    by apply path_sigma_hprop.
+Defined.
+
+(** The image of a surjective group homomorphism is the maximal subgroup. *)
+Global Instance ismaximal_image_issurj {G H : Group}
+  (f : G $-> H) `{IsSurjection f}
+  : IsMaximalSubgroup (grp_image f).
+Proof.
+  rapply conn_map_elim.
+  apply grp_image_in.
+Defined.
+
+(** ** Image of a subgroup under a group homomoprhism *)
+
+(** The image of a subgroup under group homomorphism. *) 
+Definition subgroup_image {G H : Group} (f : G $-> H)
+  : Subgroup G -> Subgroup H
+  := fun K => grp_image (grp_homo_restr f K).
+
 (** By definition, values of [f x] where [x] is in a subgroup [J] are in the image of [J] under [f]. *)
 Definition subgroup_image_in {G H : Group} (f : G $-> H) (J : Subgroup G)
   : forall x, J x -> subgroup_image f J (f x)
diff --git a/theories/Algebra/Rings/Module.v b/theories/Algebra/Rings/Module.v
index a477adff3e..e693f7f524 100644
--- a/theories/Algebra/Rings/Module.v
+++ b/theories/Algebra/Rings/Module.v
@@ -2,7 +2,7 @@ Require Import WildCat.
 Require Import Spaces.Nat.Core.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.canonical_names.
-Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup.
+Require Import Algebra.Groups.Kernel Algebra.Groups.QuotientGroup.
 Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct.
 Require Import Rings.Ring.
 
diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v
index 9384c9394d..d1746a20d0 100644
--- a/theories/Algebra/Rings/Ring.v
+++ b/theories/Algebra/Rings/Ring.v
@@ -2,7 +2,7 @@ Require Import WildCat.
 Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.abstract_algebra.
-Require Import Algebra.Groups.Group Algebra.Groups.Subgroup Algebra.Groups.Image.
+Require Import Algebra.Groups.Group Algebra.Groups.Subgroup.
 Require Export Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct Algebra.AbGroups.FiniteSum.
 
 Require Export Classes.theory.rings.

From acdcfd5b714da4b0769b15335097b2ea77845958 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 09:50:37 +0100
Subject: [PATCH 06/14] rename grp_homo_subgroup_image_in

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Groups/Subgroup.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 83b9215e36..d7b6bcb1b4 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -909,14 +909,15 @@ Definition subgroup_image_in {G H : Group} (f : G $-> H) (J : Subgroup G)
   := fun x Jx => tr ((x; Jx); idpath).
 
 (** Converting the subgroups to groups, we get the expected surjective (epi) restriction homomorphism. *)
-Definition grp_homo_subgroup_image {G H : Group} (f : G $-> H) (J : Subgroup G)
+Definition grp_homo_subgroup_image_in {G H : Group}
+  (f : G $-> H) (J : Subgroup G)
   : subgroup_group J $-> subgroup_group (subgroup_image f J)
   := functor_subgroup_group f (subgroup_image_in _ _).
 
 (** The restriction map from the subgroup to the image is surjective as expected, by [conn_map_factor1_image]. *)
-Definition issurj_grp_homo_subgroup_image {G H : Group}
+Definition issurj_grp_homo_subgroup_image_in {G H : Group}
   (f : G $-> H) (J : Subgroup G)
-  : IsSurjection (grp_homo_subgroup_image f J)
+  : IsSurjection (grp_homo_subgroup_image_in f J)
   := _.
 
 (** An image of a subgroup [J] is included in a subgroup [K] if (and only if) [J] is included in the preimage of the subgroup [K]. *)

From e2f36c280a162b4a9529011b519cbd97a52155f5 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 11:35:01 +0100
Subject: [PATCH 07/14] absorb Kernel.v into Subgroup.v and reuse preimage for
 kernel

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Groups.v                    |  1 -
 theories/Algebra/Groups/Kernel.v             | 94 --------------------
 theories/Algebra/Groups/QuotientGroup.v      |  1 -
 theories/Algebra/Groups/ShortExactSequence.v |  2 +-
 theories/Algebra/Groups/Subgroup.v           | 88 ++++++++++++++++++
 theories/Algebra/Rings/Ideal.v               |  2 +-
 theories/Algebra/Rings/Module.v              |  2 +-
 7 files changed, 91 insertions(+), 99 deletions(-)
 delete mode 100644 theories/Algebra/Groups/Kernel.v

diff --git a/theories/Algebra/Groups.v b/theories/Algebra/Groups.v
index 7722aae14c..26efb965fc 100644
--- a/theories/Algebra/Groups.v
+++ b/theories/Algebra/Groups.v
@@ -2,7 +2,6 @@
 
 Require Export HoTT.Algebra.Groups.Group.
 Require Export HoTT.Algebra.Groups.Subgroup.
-Require Export HoTT.Algebra.Groups.Kernel.
 
 Require Export HoTT.Algebra.Groups.QuotientGroup.
 Require Export HoTT.Algebra.Groups.GrpPullback.
diff --git a/theories/Algebra/Groups/Kernel.v b/theories/Algebra/Groups/Kernel.v
deleted file mode 100644
index 34f5977771..0000000000
--- a/theories/Algebra/Groups/Kernel.v
+++ /dev/null
@@ -1,94 +0,0 @@
-Require Import Basics Types.
-Require Import Algebra.Groups.Group.
-Require Import Algebra.Groups.Subgroup.
-Require Import WildCat.Core.
-Require Import Universes.HSet.
-
-(** * Kernels of group homomorphisms *)
-
-Local Open Scope mc_scope.
-Local Open Scope mc_mult_scope.
-
-Definition grp_kernel {A B : Group} (f : GroupHomomorphism A B) : NormalSubgroup A.
-Proof.
-  snrapply Build_NormalSubgroup.
-  - srapply (Build_Subgroup' (fun x => f x = 1)); cbn beta.
-    1: apply grp_homo_unit.
-    intros x y p q.
-    apply (grp_homo_moveL_1M _ _ _)^-1.
-    exact (p @ q^).
-  - intros x y; cbn; intros p.
-    apply (grp_homo_moveL_1V _ _ _)^-1.
-    lhs_V nrapply grp_inv_inv.
-    nrapply (ap (-) _^).
-    by apply grp_homo_moveL_1V.
-Defined.
-
-(** ** Corecursion principle for group kernels *)
-
-Proposition grp_kernel_corec {A B G : Group} {f : A $-> B} (g : G $-> A)
-            (h : f $o g == grp_homo_const) : G $-> grp_kernel f.
-Proof.
-  snrapply Build_GroupHomomorphism.
-  - exact (fun x:G => (g x; h x)).
-  - intros x x'.
-    apply path_sigma_hprop; cbn.
-    apply grp_homo_op.
-Defined.
-
-Theorem equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B}
-  : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const).
-Proof.
-  srapply equiv_adjointify.
-  - intro k.
-    srefine (_ $o k; _).
-    1: apply subgroup_incl.
-    intro x; cbn.
-    exact (k x).2.
-  - intros [g p].
-    exact (grp_kernel_corec _ p).
-  - intros [g p].
-    apply path_sigma_hprop; unfold pr1.
-    apply equiv_path_grouphomomorphism; intro; reflexivity.
-  - intro k.
-    apply equiv_path_grouphomomorphism; intro x.
-    apply path_sigma_hprop; reflexivity.
-Defined.
-
-(** The underlying map of a group homomorphism with a trivial kernel is an embedding. *)
-Global Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H)
-  (triv : IsTrivialGroup (grp_kernel f))
-  : IsEmbedding f.
-Proof.
-  intros h.
-  apply hprop_allpath.
-  intros [x p] [y q].
-  srapply path_sigma_hprop; unfold pr1.
-  apply grp_moveL_1M.
-  apply triv; simpl.
-  rhs_V nrapply (grp_inv_r h).
-  lhs nrapply grp_homo_op.
-  nrapply (ap011 (.*.) p).
-  lhs nrapply grp_homo_inv.
-  exact (ap (^) q).
-Defined.
-
-(** If the underlying map of a group homomorphism is an embedding then the kernel is trivial. *)
-Definition istrivial_kernel_isembedding {G H : Group} (f : G $-> H)
-  (emb : IsEmbedding f)
-  : IsTrivialGroup (grp_kernel f).
-Proof.
-  intros g p.
-  rapply (isinj_embedding f).
-  exact (p @ (grp_homo_unit f)^).
-Defined.
-Global Hint Immediate istrivial_kernel_isembedding : typeclass_instances.
-
-(** Characterisation of group embeddings *)
-Proposition equiv_istrivial_kernel_isembedding `{F : Funext}
-  {G H : Group} (f : G $-> H)
-  : IsTrivialGroup (grp_kernel f) <~> IsEmbedding f.
-Proof.
-  apply equiv_iff_hprop_uncurried.
-  split; exact _.
-Defined.
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index a82672afe3..3ebf57fe1b 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -3,7 +3,6 @@ Require Import Truncations.Core.
 Require Import Algebra.Congruence.
 Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.Subgroup.
-Require Export Algebra.Groups.Kernel.
 Require Export Colimits.Quotient.
 Require Import HSet.
 Require Import Spaces.Finite.Finite.
diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v
index 29973f191c..f86b8677b5 100644
--- a/theories/Algebra/Groups/ShortExactSequence.v
+++ b/theories/Algebra/Groups/ShortExactSequence.v
@@ -1,7 +1,7 @@
 Require Import Basics Types.
 Require Import Truncations.Core.
 Require Import WildCat.Core Pointed.
-Require Import Groups.Group Groups.Subgroup Groups.Kernel.
+Require Import Groups.Group Groups.Subgroup.
 Require Import Homotopy.ExactSequence Modalities.Identity.
 
 (** * Complexes of groups *)
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index d7b6bcb1b4..4efb099bfa 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -629,6 +629,19 @@ Global Instance ismaximalsubgroup_maximalsubgroup {G : Group}
   : IsMaximalSubgroup (maximal_subgroup G)
   := fun g => tt.
 
+(** *** Preimage subgroup *)
+
+(** The preimage of a normal subgroup is again normal. *)
+Global Instance isnormal_subgroup_preimage {G H : Group} (f : G $-> H)
+  (N : Subgroup H) `{!IsNormalSubgroup N}
+  : IsNormalSubgroup (subgroup_preimage f N).
+Proof.
+  intros x y Nfxy; simpl.
+  nrefine (transport N (grp_homo_op _ _ _)^ _).
+  apply isnormal.
+  exact (transport N (grp_homo_op _ _ _) Nfxy).
+Defined.
+
 (** *** Subgroup intersection *)
 
 (** Intersection of two subgroups *)
@@ -961,3 +974,78 @@ Proof.
   nrapply subgroup_image_in.
   by rapply isnormal_conj.
 Defined.
+
+(** ** Kernels of group homomorphisms *)
+
+Definition grp_kernel {G H : Group} (f : G $-> H)
+  : NormalSubgroup G
+  := Build_NormalSubgroup G (subgroup_preimage f (trivial_subgroup _)) _.
+
+(** Corecursion principle for group kernels *)
+Definition grp_kernel_corec {A B G : Group} {f : A $-> B}
+  (g : G $-> A) (h : f $o g == grp_homo_const)
+  : G $-> grp_kernel f.
+Proof.
+  snrapply Build_GroupHomomorphism.
+  - exact (fun x:G => (g x; h x)).
+  - intros x x'.
+    apply path_sigma_hprop; cbn.
+    apply grp_homo_op.
+Defined.
+
+Definition equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B}
+  : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const).
+Proof.
+  srapply equiv_adjointify.
+  - intro k.
+    srefine (_ $o k; _).
+    1: apply subgroup_incl.
+    intro x; cbn.
+    exact (k x).2.
+  - intros [g p].
+    exact (grp_kernel_corec _ p).
+  - intros [g p].
+    apply path_sigma_hprop; unfold pr1.
+    apply equiv_path_grouphomomorphism; intro; reflexivity.
+  - intro k.
+    apply equiv_path_grouphomomorphism; intro x.
+    apply path_sigma_hprop; reflexivity.
+Defined.
+
+(** The underlying map of a group homomorphism with a trivial kernel is an embedding. *)
+Global Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H)
+  (triv : IsTrivialGroup (grp_kernel f))
+  : IsEmbedding f.
+Proof.
+  intros h.
+  apply hprop_allpath.
+  intros [x p] [y q].
+  srapply path_sigma_hprop; unfold pr1.
+  apply grp_moveL_1M.
+  apply triv; simpl.
+  rhs_V nrapply (grp_inv_r h).
+  lhs nrapply grp_homo_op.
+  nrapply (ap011 (.*.) p).
+  lhs nrapply grp_homo_inv.
+  exact (ap (^) q).
+Defined.
+
+(** If the underlying map of a group homomorphism is an embedding then the kernel is trivial. *)
+Definition istrivial_kernel_isembedding {G H : Group} (f : G $-> H)
+  (emb : IsEmbedding f)
+  : IsTrivialGroup (grp_kernel f).
+Proof.
+  intros g p.
+  rapply (isinj_embedding f).
+  exact (p @ (grp_homo_unit f)^).
+Defined.
+Global Hint Immediate istrivial_kernel_isembedding : typeclass_instances.
+
+(** Characterisation of group embeddings *)
+Proposition equiv_istrivial_kernel_isembedding `{F : Funext}
+  {G H : Group} (f : G $-> H)
+  : IsTrivialGroup (grp_kernel f) <~> IsEmbedding f.
+Proof.
+  apply equiv_iff_hprop_uncurried.
+  split; exact _.
+Defined.
diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index 3e19ae9f05..cb1ffb5307 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -2,7 +2,7 @@ Require Import Basics Types.
 Require Import Spaces.Finite.Fin.
 Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.Rings.Ring.
-Require Import Algebra.Groups.Subgroup Algebra.Groups.Kernel.
+Require Import Algebra.Groups.Subgroup.
 Require Import Algebra.AbGroups.AbelianGroup.
 Require Import WildCat.Core.
 
diff --git a/theories/Algebra/Rings/Module.v b/theories/Algebra/Rings/Module.v
index e693f7f524..13a6c88849 100644
--- a/theories/Algebra/Rings/Module.v
+++ b/theories/Algebra/Rings/Module.v
@@ -2,7 +2,7 @@ Require Import WildCat.
 Require Import Spaces.Nat.Core.
 (* Some of the material in abstract_algebra and canonical names could be selectively exported to the user, as is done in Groups/Group.v. *)
 Require Import Classes.interfaces.canonical_names.
-Require Import Algebra.Groups.Kernel Algebra.Groups.QuotientGroup.
+Require Import Algebra.Groups.QuotientGroup.
 Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct.
 Require Import Rings.Ring.
 

From bf5646d2418b1b11ad1bdcd51e43520e14e6cb61 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 11:56:14 +0100
Subject: [PATCH 08/14] move preimage to own section and fix some section
 headers

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Groups/Subgroup.v | 38 +++++++++++++++---------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 4efb099bfa..f2933d3e2d 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -221,22 +221,6 @@ Definition grp_homo_restr {G H : Group} (f : G $-> H) (K : Subgroup G)
   : subgroup_group K $-> H
   := f $o subgroup_incl _.
 
-(** The preimage of a subgroup under a group homomorphism is a subgroup. *)
-Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
-  : Subgroup G.
-Proof.
-  snrapply Build_Subgroup'.
-  - exact (S o f).
-  - hnf; exact _.
-  - nrefine (transport S (grp_homo_unit f)^ _).
-    apply subgroup_in_unit.
-  - hnf; intros x y Sfx Sfy.
-    nrefine (transport S (grp_homo_op f _ _)^ _).
-    nrapply subgroup_in_op; only 1: assumption.
-    nrefine (transport S (grp_homo_inv f _)^ _).
-    by apply subgroup_in_inv.
-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).
@@ -629,7 +613,23 @@ Global Instance ismaximalsubgroup_maximalsubgroup {G : Group}
   : IsMaximalSubgroup (maximal_subgroup G)
   := fun g => tt.
 
-(** *** Preimage subgroup *)
+(** ** Preimage subgroup *)
+
+(** The preimage of a subgroup under a group homomorphism is a subgroup. *)
+Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
+  : Subgroup G.
+Proof.
+  snrapply Build_Subgroup'.
+  - exact (S o f).
+  - hnf; exact _.
+  - nrefine (transport S (grp_homo_unit f)^ _).
+    apply subgroup_in_unit.
+  - hnf; intros x y Sfx Sfy.
+    nrefine (transport S (grp_homo_op f _ _)^ _).
+    nrapply subgroup_in_op; only 1: assumption.
+    nrefine (transport S (grp_homo_inv f _)^ _).
+    by apply subgroup_in_inv.
+Defined.
 
 (** The preimage of a normal subgroup is again normal. *)
 Global Instance isnormal_subgroup_preimage {G H : Group} (f : G $-> H)
@@ -655,13 +655,13 @@ Proof.
   split; by apply subgroup_in_op_inv.
 Defined.
 
-(** *** Simple groups *)
+(** ** Simple groups *)
 
 Class IsSimpleGroup (G : Group)
   := is_simple_group : forall (N : Subgroup G) `{IsNormalSubgroup G N},
     IsTrivialGroup N + IsMaximalSubgroup N.
 
-(** *** The subgroup generated by a subset *)
+(** ** The subgroup generated by a subset *)
 
 (** Underlying type family of a subgroup generated by subset *)
 Inductive subgroup_generated_type {G : Group} (X : G -> Type) : G -> Type :=

From 6bb531f0c4c49f08617360ee756e21030c2871bb Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 12:03:21 +0100
Subject: [PATCH 09/14] more comments and reorganization

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Groups/Subgroup.v | 90 ++++++++++++++++++------------
 1 file changed, 53 insertions(+), 37 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index f2933d3e2d..f4c6a8db8b 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -10,6 +10,8 @@ Generalizable Variables G H A B C N f g.
 
 (** * Subgroups *)
 
+(** ** Definition of being a subgroup *)
+
 (** A subgroup H of a group G is a predicate (i.e. an hProp-valued type family) on G which is closed under the group operations. The group underlying H is given by the total space { g : G & H g }, defined in [subgroup_group] below. *)
 Class IsSubgroup {G : Group} (H : G -> Type) := {
   issubgroup_predicate : forall x, IsHProp (H x) ;
@@ -20,6 +22,8 @@ Class IsSubgroup {G : Group} (H : G -> Type) := {
 
 Global Existing Instance issubgroup_predicate.
 
+(** Basic properties of subgroups *)
+
 (** Smart constructor for subgroups.  *)
 Definition Build_IsSubgroup' {G : Group}
   (H : G -> Type) `{forall x, IsHProp (H x)}
@@ -102,6 +106,8 @@ Proof.
   exact (istrunc_equiv_istrunc _ (issig_issubgroup H)).
 Defined.
 
+(** ** Definition of subgroup *) 
+
 (** The type (set) of subgroups of a group G. *)
 Record Subgroup (G : Group) := {
   subgroup_pred : G -> Type ;
@@ -111,6 +117,11 @@ Record Subgroup (G : Group) := {
 Coercion subgroup_pred : Subgroup >-> Funclass.
 Global Existing Instance subgroup_issubgroup.
 
+Definition issig_subgroup {G : Group} : _ <~> Subgroup G
+  := ltac:(issig).
+
+(** ** Basics properties of subgroups *)
+
 Definition Build_Subgroup' {G : Group}
   (H : G -> Type) `{forall x, IsHProp (H x)}
   (unit : H mon_unit)
@@ -150,6 +161,38 @@ Proof.
   by rewrite grp_inv_op, grp_inv_inv.
 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).
+Proof.
+  refine ((equiv_ap' issig_subgroup^-1%equiv _ _)^-1%equiv oE _); cbn.
+  refine (equiv_path_sigma_hprop _ _ oE _); cbn.
+  apply equiv_path_arrow.
+Defined.
+
+Proposition equiv_path_subgroup' `{U : Univalence} {G : Group} (H K : Subgroup G)
+  : (forall g:G, H g <-> K g) <~> (H = K).
+Proof.
+  refine (equiv_path_subgroup _ _ oE _).
+  apply equiv_functor_forall_id; intro g.
+  exact equiv_path_iff_ishprop.
+Defined.
+
+Global Instance ishset_subgroup `{Univalence} {G : Group} : IsHSet (Subgroup G).
+Proof.
+  nrefine (istrunc_equiv_istrunc _ issig_subgroup).
+  nrefine (istrunc_equiv_istrunc _ (equiv_functor_sigma_id _)).
+  - intro P; apply issig_issubgroup.
+  - nrefine (istrunc_equiv_istrunc _ (equiv_sigma_assoc' _ _)^-1%equiv).
+    nrapply istrunc_sigma.
+    2: intros []; apply istrunc_hprop.
+    nrefine (istrunc_equiv_istrunc
+               _ (equiv_sig_coind (fun g:G => Type) (fun g x => IsHProp x))^-1%equiv).
+    apply istrunc_forall.
+Defined.
+
+(** ** Underlying group of a subgroup *)
+
 (** The group given by a subgroup *)
 Definition subgroup_group {G : Group} (H : Subgroup G) : Group.
 Proof.
@@ -170,6 +213,7 @@ Defined.
 
 Coercion subgroup_group : Subgroup >-> Group.
 
+(** The underlying group of a subgroup of [G] has an inclusion map into [G]. *) 
 Definition subgroup_incl {G : Group} (H : Subgroup G)
   : subgroup_group H $-> G.
 Proof.
@@ -178,13 +222,11 @@ Proof.
   hnf; reflexivity.
 Defined.
 
+(** The inclusion map is an embedding. *)
 Global Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G)
   : IsEmbedding (subgroup_incl H)
   := fun _ => istrunc_equiv_istrunc _ (hfiber_fibration _ _).
 
-Definition issig_subgroup {G : Group} : _ <~> Subgroup G
-  := ltac:(issig).
-
 Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H}
   (f : G $-> H) (g : forall x, J x -> K (f x))
   : subgroup_group J $-> subgroup_group K.
@@ -221,35 +263,7 @@ Definition grp_homo_restr {G H : Group} (f : G $-> H) (K : Subgroup G)
   : subgroup_group K $-> H
   := f $o subgroup_incl _.
 
-(** 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).
-Proof.
-  refine ((equiv_ap' issig_subgroup^-1%equiv _ _)^-1%equiv oE _); cbn.
-  refine (equiv_path_sigma_hprop _ _ oE _); cbn.
-  apply equiv_path_arrow.
-Defined.
-
-Proposition equiv_path_subgroup' `{U : Univalence} {G : Group} (H K : Subgroup G)
-  : (forall g:G, H g <-> K g) <~> (H = K).
-Proof.
-  refine (equiv_path_subgroup _ _ oE _).
-  apply equiv_functor_forall_id; intro g.
-  exact equiv_path_iff_ishprop.
-Defined.
-
-Global Instance ishset_subgroup `{Univalence} {G : Group} : IsHSet (Subgroup G).
-Proof.
-  nrefine (istrunc_equiv_istrunc _ issig_subgroup).
-  nrefine (istrunc_equiv_istrunc _ (equiv_functor_sigma_id _)).
-  - intro P; apply issig_issubgroup.
-  - nrefine (istrunc_equiv_istrunc _ (equiv_sigma_assoc' _ _)^-1%equiv).
-    nrapply istrunc_sigma.
-    2: intros []; apply istrunc_hprop.
-    nrefine (istrunc_equiv_istrunc
-               _ (equiv_sig_coind (fun g:G => Type) (fun g x => IsHProp x))^-1%equiv).
-    apply istrunc_forall.
-Defined.
+(** ** Cosets of subgroups *)
 
 Section Cosets.
 
@@ -325,7 +339,7 @@ Section Cosets.
 
 End Cosets.
 
-(** Identities related to the left and right cosets. *)
+(** ** Properties of left and right cosets *)
 
 Definition in_cosetL_unit {G : Group} {N : Subgroup G}
   : forall x y, in_cosetL N (x^ * y) mon_unit <~> in_cosetL N x y.
@@ -382,6 +396,8 @@ Proof.
     apply equiv_subgroup_op_inv.
 Defined.
 
+(** ** Normal subgroups *)
+
 (** A normal subgroup is a subgroup closed under conjugation. *)
 Class IsNormalSubgroup {G : Group} (N : Subgroup G)
   := isnormal : forall {x y}, N (x * y) -> N (y * x).
@@ -497,7 +513,7 @@ Proof.
   exact p.
 Defined.
 
-(** *** Trivial subgroup *)
+(** ** Trivial subgroup *)
 
 (** The trivial subgroup of a group [G]. *)
 Definition trivial_subgroup G : Subgroup G.
@@ -571,7 +587,7 @@ Proof.
   1,2: apply istrivial_iff_grp_iso_trivial; exact _.
 Defined.
 
-(** *** Maximal Subgroups *)
+(** ** Maximal Subgroups *)
 
 (** Every group is a (maximal) subgroup of itself. *)
 Definition maximal_subgroup G : Subgroup G.
@@ -642,7 +658,7 @@ Proof.
   exact (transport N (grp_homo_op _ _ _) Nfxy).
 Defined.
 
-(** *** Subgroup intersection *)
+(** ** Subgroup intersection *)
 
 (** Intersection of two subgroups *)
 Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G.
@@ -796,7 +812,7 @@ Definition normalsubgroup_product {G : Group} (H K : NormalSubgroup G)
   : NormalSubgroup G
   := Build_NormalSubgroup G (subgroup_product H K) _.
 
-(* **** Paths between generated subgroups *)
+(* *** Paths between generated subgroups *)
 
 (* This gets used twice in [path_subgroup_generated], so we factor it out here. *)
 Local Lemma path_subgroup_generated_helper {G : Group}

From 7a6440b4a46803a0362e20a10088d93c84a275a8 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 21 Jan 2025 09:29:38 -0500
Subject: [PATCH 10/14] Subgroup: add and use subgroup_corec

---
 theories/Algebra/Groups/Subgroup.v | 46 +++++++++++-------------------
 1 file changed, 17 insertions(+), 29 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index f4c6a8db8b..0dc835e719 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -227,17 +227,22 @@ Global Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G)
   : IsEmbedding (subgroup_incl H)
   := fun _ => istrunc_equiv_istrunc _ (hfiber_fibration _ _).
 
-Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H}
-  (f : G $-> H) (g : forall x, J x -> K (f x))
-  : subgroup_group J $-> subgroup_group K.
+Definition subgroup_corec {G H : Group} {K : Subgroup H}
+  (f : G $-> H) (g : forall x, K (f x))
+  : G $-> subgroup_group K.
 Proof.
   snrapply Build_GroupHomomorphism.
-  - exact (functor_sigma f g).
+  - exact (fun x => (f x; g x)).
   - intros x y.
     rapply path_sigma_hprop.
     snrapply grp_homo_op.
 Defined.
 
+Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H}
+  (f : G $-> H) (g : forall x, J x -> K (f x))
+  : subgroup_group J $-> subgroup_group K
+  := subgroup_corec (f $o subgroup_incl _) (sig_ind _ g).
+
 Definition grp_iso_subgroup_group {G H : Group@{i}}
   {J : Subgroup@{i i} G} (K : Subgroup@{i i} H)
   (e : G $<~> H) (f : forall x, J x <-> K (e x))
@@ -861,23 +866,12 @@ Proof.
 Defined.
 
 Definition grp_image_in {G H : Group} (f : G $-> H)
-  : forall x, grp_image f (f x).
-Proof.
-  intros x.
-  apply tr.
-  by exists x.
-Defined.
+  : forall x, grp_image f (f x)
+  := fun x => tr (x; idpath).
 
-Definition grp_homo_image_in {G H : Group} (f : G $-> H) : G $-> grp_image f.
-Proof.
-  snrapply Build_GroupHomomorphism.
-  - intros x.
-    exists (f x).
-    apply grp_image_in.
-  - intros x y.
-    rapply path_sigma_hprop; simpl.
-    apply grp_homo_op.
-Defined.
+Definition grp_homo_image_in {G H : Group} (f : G $-> H)
+  : G $-> grp_image f
+  := subgroup_corec f (grp_image_in f).
 
 (** ** Image of a group embedding *)
 
@@ -901,10 +895,8 @@ Definition grp_image_in_embedding {G H : Group} (f : G $-> H) `{IsEmbedding f}
   : GroupIsomorphism G (grp_image_embedding f).
 Proof.
   snrapply Build_GroupIsomorphism.
-  - snrapply Build_GroupHomomorphism.
-    + intro x.
-      by exists (f x), x.
-    + cbn; grp_auto.
+  - snrapply (subgroup_corec f).
+    exact (fun x => (x; idpath)).
   - apply isequiv_surj_emb.
     2: apply (cancelL_isembedding (g:=pr1)).
     intros [b [a p]]; cbn.
@@ -1002,11 +994,7 @@ Definition grp_kernel_corec {A B G : Group} {f : A $-> B}
   (g : G $-> A) (h : f $o g == grp_homo_const)
   : G $-> grp_kernel f.
 Proof.
-  snrapply Build_GroupHomomorphism.
-  - exact (fun x:G => (g x; h x)).
-  - intros x x'.
-    apply path_sigma_hprop; cbn.
-    apply grp_homo_op.
+  snrapply (subgroup_corec g); exact h.
 Defined.
 
 Definition equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B}

From 5d0823f6a40ec7a3042f6a234ee72bdd0f248bef Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 21 Jan 2025 09:36:14 -0500
Subject: [PATCH 11/14] Subgroup: move grp_homo_restr earlier and use it

---
 theories/Algebra/Groups/Subgroup.v | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 0dc835e719..3a92577ed1 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -227,6 +227,12 @@ Global Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G)
   : IsEmbedding (subgroup_incl H)
   := fun _ => istrunc_equiv_istrunc _ (hfiber_fibration _ _).
 
+(** Restriction of a group homomorphism to a subgroup. *)
+Definition grp_homo_restr {G H : Group} (f : G $-> H) (K : Subgroup G)
+  : subgroup_group K $-> H
+  := f $o subgroup_incl _.
+
+(** Corestriction of a group homomorphism to a subgroup. *)
 Definition subgroup_corec {G H : Group} {K : Subgroup H}
   (f : G $-> H) (g : forall x, K (f x))
   : G $-> subgroup_group K.
@@ -238,10 +244,11 @@ Proof.
     snrapply grp_homo_op.
 Defined.
 
+(** Functoriality on subgroups. *)
 Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H}
   (f : G $-> H) (g : forall x, J x -> K (f x))
   : subgroup_group J $-> subgroup_group K
-  := subgroup_corec (f $o subgroup_incl _) (sig_ind _ g).
+  := subgroup_corec (grp_homo_restr f J) (sig_ind _ g).
 
 Definition grp_iso_subgroup_group {G H : Group@{i}}
   {J : Subgroup@{i i} G} (K : Subgroup@{i i} H)
@@ -263,11 +270,6 @@ Proof.
     nrapply eissect.
 Defined.
 
-(** Restriction of a group homomorphism to a subgroup. *)
-Definition grp_homo_restr {G H : Group} (f : G $-> H) (K : Subgroup G)
-  : subgroup_group K $-> H
-  := f $o subgroup_incl _.
-
 (** ** Cosets of subgroups *)
 
 Section Cosets.

From 5db2ab0efdfcc4be3cfe6246b417574baae37843 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 21 Jan 2025 09:43:06 -0500
Subject: [PATCH 12/14] Subgroup: fix comments

---
 theories/Algebra/Groups/Subgroup.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 3a92577ed1..c5bbf70e23 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -819,9 +819,9 @@ Definition normalsubgroup_product {G : Group} (H K : NormalSubgroup G)
   : NormalSubgroup G
   := Build_NormalSubgroup G (subgroup_product H K) _.
 
-(* *** Paths between generated subgroups *)
+(** *** Paths between generated subgroups *)
 
-(* This gets used twice in [path_subgroup_generated], so we factor it out here. *)
+(** This gets used twice in [path_subgroup_generated], so we factor it out here. *)
 Local Lemma path_subgroup_generated_helper {G : Group}
   (X Y : G -> Type) (K : forall g, merely (X g) -> merely (Y g))
   : forall g, Trunc (-1) (subgroup_generated_type X g)
@@ -835,7 +835,7 @@ Proof.
     by apply tr, sgt_op.
 Defined.
 
-(* If the predicates selecting the generators are merely equivalent, then the generated subgroups are equal. (One could probably prove that the generated subgroup are isomorphic without using univalence.) *)
+(** If the predicates selecting the generators are merely equivalent, then the generated subgroups are equal. (One could probably prove that the generated subgroup are isomorphic without using univalence.) *)
 Definition path_subgroup_generated `{Univalence} {G : Group}
   (X Y : G -> Type) (K : forall g, Trunc (-1) (X g) <-> Trunc (-1) (Y g))
   : subgroup_generated X = subgroup_generated Y.
@@ -846,7 +846,7 @@ Proof.
   - apply path_subgroup_generated_helper, (fun x => snd (K x)).
 Defined.
 
-(* Equal subgroups have isomorphic underlying groups. *)
+(** Equal subgroups have isomorphic underlying groups. *)
 Definition equiv_subgroup_group {G : Group} (H1 H2 : Subgroup G)
   : H1 = H2 -> GroupIsomorphism H1 H2
   := ltac:(intros []; exact grp_iso_id).
@@ -967,7 +967,7 @@ Proof.
   - snrapply subgroup_image_rec.
 Defined.
 
-(** [subgorup_image] preserves normal subgroups when the group homomorphism is surjective. *)
+(** [subgroup_image] preserves normal subgroups when the group homomorphism is surjective. *)
 Global Instance isnormal_subgroup_image {G H : Group} (f : G $-> H)
   (J : Subgroup G) `{!IsNormalSubgroup J} `{!IsSurjection f}
   : IsNormalSubgroup (subgroup_image f J).

From c8258ce757ae8e0709fda132c5e937905cf22a02 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 21 Jan 2025 23:14:50 +0100
Subject: [PATCH 13/14] generalise equiv_grp_kernel_corec

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Groups/Subgroup.v | 37 ++++++++++++++++--------------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index c5bbf70e23..e9fa7c8cf3 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -244,6 +244,24 @@ Proof.
     snrapply grp_homo_op.
 Defined.
 
+(** Corestriction is an equivalence on group homomorphisms. *)
+Definition equiv_subgroup_corec {F : Funext}
+  (G : Group) {H : Group} (K : Subgroup H)
+  : (exists (f : G $-> H), forall x, K (f x)) <~> (G $-> subgroup_group K).
+Proof.
+  snrapply equiv_adjointify.
+  - exact (sig_rec subgroup_corec).
+  - intros g.
+    exists (subgroup_incl _ $o g).
+    intros x.
+    exact (g x).2.
+  - intros g.
+    by snrapply equiv_path_grouphomomorphism.
+  - intros [f p].
+    rapply path_sigma_hprop.
+    by snrapply equiv_path_grouphomomorphism.
+Defined.
+
 (** Functoriality on subgroups. *)
 Definition functor_subgroup_group {G H : Group} {J : Subgroup G} {K : Subgroup H}
   (f : G $-> H) (g : forall x, J x -> K (f x))
@@ -1000,23 +1018,8 @@ Proof.
 Defined.
 
 Definition equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B}
-  : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const).
-Proof.
-  srapply equiv_adjointify.
-  - intro k.
-    srefine (_ $o k; _).
-    1: apply subgroup_incl.
-    intro x; cbn.
-    exact (k x).2.
-  - intros [g p].
-    exact (grp_kernel_corec _ p).
-  - intros [g p].
-    apply path_sigma_hprop; unfold pr1.
-    apply equiv_path_grouphomomorphism; intro; reflexivity.
-  - intro k.
-    apply equiv_path_grouphomomorphism; intro x.
-    apply path_sigma_hprop; reflexivity.
-Defined.
+  : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const)
+  := (equiv_subgroup_corec G (grp_kernel f))^-1.
 
 (** The underlying map of a group homomorphism with a trivial kernel is an embedding. *)
 Global Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H)

From 9f85dd5a728123724f0f0f5a3711e9eec50ef713 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Wed, 22 Jan 2025 01:05:15 +0100
Subject: [PATCH 14/14] flip direction of equiv_grp_kernel_corec

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 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 e9fa7c8cf3..f65f1c4555 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -247,7 +247,7 @@ Defined.
 (** Corestriction is an equivalence on group homomorphisms. *)
 Definition equiv_subgroup_corec {F : Funext}
   (G : Group) {H : Group} (K : Subgroup H)
-  : (exists (f : G $-> H), forall x, K (f x)) <~> (G $-> subgroup_group K).
+  : {f : G $-> H & forall x, K (f x)} <~> (G $-> subgroup_group K).
 Proof.
   snrapply equiv_adjointify.
   - exact (sig_rec subgroup_corec).
@@ -1018,8 +1018,8 @@ Proof.
 Defined.
 
 Definition equiv_grp_kernel_corec `{Funext} {A B G : Group} {f : A $-> B}
-  : (G $-> grp_kernel f) <~> (exists g : G $-> A, f $o g == grp_homo_const)
-  := (equiv_subgroup_corec G (grp_kernel f))^-1.
+  : {g : G $-> A & f $o g == grp_homo_const} <~> (G $-> grp_kernel f)
+  := equiv_subgroup_corec G (grp_kernel f).
 
 (** The underlying map of a group homomorphism with a trivial kernel is an embedding. *)
 Global Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H)