Characteristic subgroups (#863)

This PR adds a definition of characteristic subgroups to the library. I
proof of the expected properties is expected to follow in a later PR

src/commutative-algebra/isomorphisms-commutative-rings.lagda.md

@@ -353,7 +353,7 @@ module _
 
   iso-ab-iso-ab-Commutative-Ring :
     iso-ab-Commutative-Ring →
-    type-iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
+    iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
   iso-ab-iso-ab-Commutative-Ring =
     iso-ab-iso-ab-Ring
       ( ring-Commutative-Ring A)
@@ -376,7 +376,7 @@ module _
 
   iso-ab-iso-Commutative-Ring :
     iso-Commutative-Ring A B →
-    type-iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
+    iso-Ab (ab-Commutative-Ring A) (ab-Commutative-Ring B)
   iso-ab-iso-Commutative-Ring =
     iso-ab-iso-Ring
       ( ring-Commutative-Ring A)

src/commutative-algebra/transporting-commutative-ring-structure-isomorphisms-abelian-groups.lagda.md

@@ -50,7 +50,7 @@ transported ring structure.
 ```agda
 module _
   {l1 l2 : Level} (A : Commutative-Ring l1) (B : Ab l2)
-  (f : type-iso-Ab (ab-Commutative-Ring A) B)
+  (f : iso-Ab (ab-Commutative-Ring A) B)
   where
 
   ring-transport-commutative-ring-structure-iso-Ab : Ring l2

src/finite-group-theory/finite-type-groups.lagda.md

@@ -126,7 +126,7 @@ module _
           ( id)))
 
   iso-loop-group-fin-UU-Fin-Group :
-    type-iso-Group
+    iso-Group
       ( abstract-group-Concrete-Group (UU-Fin-Group l n))
       ( loop-group-Set (raise-Set l (Fin-Set n)))
   pr1 iso-loop-group-fin-UU-Fin-Group =

src/finite-group-theory/groups-of-order-2.lagda.md

@@ -102,7 +102,7 @@ iso-Group-of-Order-2 :
   {l1 l2 : Level} (G : Group-of-Order-2 l1) (H : Group-of-Order-2 l2) →
   UU (l1 ⊔ l2)
 iso-Group-of-Order-2 G H =
-  type-iso-Group (group-Group-of-Order-2 G) (group-Group-of-Order-2 H)
+  iso-Group (group-Group-of-Order-2 G) (group-Group-of-Order-2 H)
 
 module _
   {l : Level} (G : Group-of-Order-2 l)

src/foundation/images-subtypes.lagda.md

@@ -28,7 +28,7 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
   where
 
-  subtype-im-subtype :
+  im-subtype :
     {l3 : Level} → subtype l3 A → subtype (l1 ⊔ l2 ⊔ l3) B
-  subtype-im-subtype S y = subtype-im (f ∘ inclusion-subtype S) y
+  im-subtype S y = subtype-im (f ∘ inclusion-subtype S) y
 ```

src/group-theory.lagda.md

@@ -25,6 +25,7 @@ open import group-theory.central-elements-groups public
 open import group-theory.central-elements-monoids public
 open import group-theory.central-elements-semigroups public
 open import group-theory.centralizer-subgroups public
+open import group-theory.characteristic-subgroups public
 open import group-theory.commutative-monoids public
 open import group-theory.commutator-subgroups public
 open import group-theory.commutators-of-elements-groups public

src/group-theory/category-of-groups.lagda.md

@@ -32,7 +32,7 @@ is-large-category-Group G =
     ( is-contr-total-iso-Group G)
     ( iso-eq-Group G)
 
-eq-iso-Group : {l : Level} (G H : Group l) → type-iso-Group G H → Id G H
+eq-iso-Group : {l : Level} (G H : Group l) → iso-Group G H → Id G H
 eq-iso-Group G H = map-inv-is-equiv (is-large-category-Group G H)
 
 Group-Large-Category : Large-Category lsuc (_⊔_)

src/group-theory/category-of-semigroups.lagda.md

@@ -41,12 +41,12 @@ is-large-category-Semigroup G =
     ( iso-eq-Semigroup G)
 
 extensionality-Semigroup :
-  {l : Level} (G H : Semigroup l) → Id G H ≃ type-iso-Semigroup G H
+  {l : Level} (G H : Semigroup l) → Id G H ≃ iso-Semigroup G H
 pr1 (extensionality-Semigroup G H) = iso-eq-Semigroup G H
 pr2 (extensionality-Semigroup G H) = is-large-category-Semigroup G H
 
 eq-iso-Semigroup :
-  {l : Level} (G H : Semigroup l) → type-iso-Semigroup G H → Id G H
+  {l : Level} (G H : Semigroup l) → iso-Semigroup G H → Id G H
 eq-iso-Semigroup G H = map-inv-is-equiv (is-large-category-Semigroup G H)
 
 Semigroup-Large-Category : Large-Category lsuc (_⊔_)

src/group-theory/characteristic-subgroups.lagda.md

@@ -0,0 +1,75 @@
+# Characteristic subgroups
+
+```agda
+module group-theory.characteristic-subgroups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import group-theory.groups
+open import group-theory.images-of-group-homomorphisms
+open import group-theory.isomorphisms-groups
+open import group-theory.subgroups
+```
+
+</details>
+
+## Idea
+
+A **characteristic subgroup** of a [group](group-theory.groups.md) `G` is a
+[subgroup](group-theory.subgroups.md) `H` of `G` such that `f H ⊆ H` for every
+[isomorphism](group-theory.isomorphisms-groups.md) `f : G ≅ G`. The seemingly
+stronger condition, which asserts that `f H ＝ H` for every isomorphism
+`f : G ≅ G` is equivalent.
+
+Note that any characteristic subgroup is
+[normal](group-theory.normal-subgroups.md), since the condition of being
+characteristic implies that `conjugation x H ＝ H`.
+
+## Definition
+
+### The predicate of being a characteristic subgroup
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
+  where
+
+  is-characteristic-prop-Subgroup : Prop (l1 ⊔ l2)
+  is-characteristic-prop-Subgroup =
+    Π-Prop
+      ( iso-Group G G)
+      ( λ f →
+        leq-prop-Subgroup G
+          ( im-hom-Subgroup G G (hom-iso-Group G G f) H)
+          ( H))
+```
+
+### The stronger predicate of being a characteristic subgroup
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
+  where
+
+  is-characteristic-prop-Subgroup' : Prop (l1 ⊔ l2)
+  is-characteristic-prop-Subgroup' =
+    Π-Prop
+      ( iso-Group G G)
+      ( λ f →
+        has-same-elements-prop-Subgroup G
+          ( im-hom-Subgroup G G (hom-iso-Group G G f) H)
+          ( H))
+```
+
+## See also
+
+- [Characteristic subgroup](https://groupprops.subwiki.org/wiki/Characteristic_subgroup)
+  at Groupprops
+- [Characteristic subgroup](https://www.wikidata.org/entity/Q747027) at Wikidata
+- [Characteristic subgroup](https://en.wikipedia.org/wiki/Characteristic_subgroup)
+  at Wikipedia

src/group-theory/conjugation.lagda.md

@@ -385,7 +385,7 @@ module _
   pr1 (conjugation-equiv-Group x) = equiv-conjugation-Group G x
   pr2 (conjugation-equiv-Group x) = distributive-conjugation-mul-Group G x
 
-  conjugation-iso-Group : type-Group G → type-iso-Group G G
+  conjugation-iso-Group : type-Group G → iso-Group G G
   conjugation-iso-Group x = iso-equiv-Group G G (conjugation-equiv-Group x)
 
   preserves-integer-powers-conjugation-Group :

src/group-theory/epimorphisms-groups.lagda.md

@@ -60,7 +60,7 @@ module _
 ```agda
 module _
   {l1 l2 : Level} (l3 : Level) (G : Group l1)
-  (H : Group l2) (f : type-iso-Group G H)
+  (H : Group l2) (f : iso-Group G H)
   where
 
   is-epi-iso-Group :

src/group-theory/full-subgroups.lagda.md

@@ -111,12 +111,12 @@ module _
   pr2 equiv-group-inclusion-full-Subgroup =
     preserves-mul-inclusion-full-Subgroup
 
-  iso-full-Subgroup : type-iso-Group group-full-Subgroup G
+  iso-full-Subgroup : iso-Group group-full-Subgroup G
   iso-full-Subgroup =
     iso-equiv-Group group-full-Subgroup G equiv-group-inclusion-full-Subgroup
 
   inv-iso-full-Subgroup :
-    type-iso-Group G group-full-Subgroup
+    iso-Group G group-full-Subgroup
   inv-iso-full-Subgroup =
     inv-iso-Group group-full-Subgroup G iso-full-Subgroup
 ```
@@ -141,7 +141,7 @@ module _
       ( is-equiv-inclusion-is-full-subtype (subset-Subgroup G H) K)
 
   iso-inclusion-is-full-Subgroup :
-    is-full-Subgroup G H → type-iso-Group (group-Subgroup G H) G
+    is-full-Subgroup G H → iso-Group (group-Subgroup G H) G
   pr1 (iso-inclusion-is-full-Subgroup K) = hom-inclusion-Subgroup G H
   pr2 (iso-inclusion-is-full-Subgroup K) = is-iso-inclusion-is-full-Subgroup K
 

src/group-theory/generating-elements-groups.lagda.md

@@ -607,7 +607,7 @@ module _
       ( is-equiv-ev-element-Group-With-Generating-Element)
 
   iso-ev-element-Group-With-Generating-Element :
-    type-iso-Ab
+    iso-Ab
       ( ab-hom-Ab
         ( abelian-group-Group-With-Generating-Element G)
         ( abelian-group-Group-With-Generating-Element G))

src/group-theory/images-of-group-homomorphisms.lagda.md

@@ -10,6 +10,7 @@ module group-theory.images-of-group-homomorphisms where
 open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.images
+open import foundation.images-subtypes
 open import foundation.logical-equivalences
 open import foundation.propositional-truncations
 open import foundation.universal-property-image
@@ -128,6 +129,58 @@ module _
     backward-implication (is-image-image-hom-Group K)
 ```
 
+### The image of a subgroup of a group homomorphism
+
+```agda
+module _
+  {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
+  (K : Subgroup l3 G)
+  where
+
+  subset-im-hom-Subgroup : subset-Group (l1 ⊔ l2 ⊔ l3) H
+  subset-im-hom-Subgroup =
+    im-subtype (map-hom-Group G H f) (subset-Subgroup G K)
+
+  contains-unit-im-hom-Subgroup :
+    contains-unit-subset-Group H subset-im-hom-Subgroup
+  contains-unit-im-hom-Subgroup =
+    unit-trunc-Prop (unit-Subgroup G K , preserves-unit-hom-Group G H f)
+
+  abstract
+    is-closed-under-multiplication-im-hom-Subgroup :
+      is-closed-under-multiplication-subset-Group H subset-im-hom-Subgroup
+    is-closed-under-multiplication-im-hom-Subgroup x y u v =
+      apply-twice-universal-property-trunc-Prop u v
+        ( subset-im-hom-Subgroup (mul-Group H x y))
+        ( λ where
+          ((x' , k) , refl) ((y' , l) , refl) →
+            unit-trunc-Prop
+              ( ( mul-Subgroup G K (x' , k) (y' , l)) ,
+                ( preserves-mul-hom-Group G H f x' y')))
+
+  abstract
+    is-closed-under-inverses-im-hom-Subgroup :
+      is-closed-under-inverses-subset-Group H subset-im-hom-Subgroup
+    is-closed-under-inverses-im-hom-Subgroup x u =
+      apply-universal-property-trunc-Prop u
+        ( subset-im-hom-Subgroup (inv-Group H x))
+        ( λ where
+          ((x' , k) , refl) →
+            unit-trunc-Prop
+              ( ( inv-Subgroup G K (x' , k)) ,
+                ( preserves-inv-hom-Group G H f x')))
+
+  im-hom-Subgroup : Subgroup (l1 ⊔ l2 ⊔ l3) H
+  pr1 im-hom-Subgroup =
+    subset-im-hom-Subgroup
+  pr1 (pr2 im-hom-Subgroup) =
+    contains-unit-im-hom-Subgroup
+  pr1 (pr2 (pr2 im-hom-Subgroup)) =
+    is-closed-under-multiplication-im-hom-Subgroup
+  pr2 (pr2 (pr2 im-hom-Subgroup)) =
+    is-closed-under-inverses-im-hom-Subgroup
+```
+
 ## Properties
 
 ### A group homomorphism is surjective if and only if its image is the full subgroup