Merge pull request #2201 from Alizter/ps/rr/image_of_a_subgroup

image of a subgroup
HoTT · Jan 22, 2025 · 03ff069 · 03ff069
2 parents 8340a1f + 9f85dd5
commit 03ff069
Show file tree

Hide file tree

Showing 10 changed files with 319 additions and 240 deletions.
diff --git 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
@@ -2,8 +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.
 Require Export HoTT.Algebra.Groups.GrpPullback.

diff --git a/theories/Algebra/Groups/Image.v b/theories/Algebra/Groups/Image.v
diff --git a/theories/Algebra/Groups/Kernel.v b/theories/Algebra/Groups/Kernel.v
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
@@ -3,8 +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.
 Require Import Spaces.Finite.Finite.
@@ -292,7 +290,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/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 *)