From c5ba6a348732924979ae15d67d25f3e845889c0a Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Mon, 16 Oct 2023 15:50:10 +0100
Subject: [PATCH] Perfect subgroups (#847)

This PR defines perfect subgroups.

---------

Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
---
 src/group-theory.lagda.md                   |  1 +
 src/group-theory/perfect-subgroups.lagda.md | 47 +++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 src/group-theory/perfect-subgroups.lagda.md

diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
index e3324d5180..c6288bf371 100644
--- a/src/group-theory.lagda.md
+++ b/src/group-theory.lagda.md
@@ -125,6 +125,7 @@ open import group-theory.orbits-group-actions public
 open import group-theory.orbits-monoid-actions public
 open import group-theory.orders-of-elements-groups public
 open import group-theory.perfect-groups public
+open import group-theory.perfect-subgroups public
 open import group-theory.powers-of-elements-commutative-monoids public
 open import group-theory.powers-of-elements-groups public
 open import group-theory.powers-of-elements-monoids public
diff --git a/src/group-theory/perfect-subgroups.lagda.md b/src/group-theory/perfect-subgroups.lagda.md
new file mode 100644
index 0000000000..9e4dac3fc1
--- /dev/null
+++ b/src/group-theory/perfect-subgroups.lagda.md
@@ -0,0 +1,47 @@
+# Perfect subgroups
+
+```agda
+module group-theory.perfect-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.perfect-groups
+open import group-theory.subgroups
+```
+
+</details>
+
+## Idea
+
+A [subgroup](group-theory.subgroups.md) `H` of a [group](group-theory.groups.md)
+`G` is a **perfect subgroup** if it is a
+[perfect group](group-theory.perfect-groups.md) on its own.
+
+## Definitions
+
+### The predicate of being a perfect subgroup
+
+```agda
+module _
+  {l1 l2 : Level} (G : Group l1) (H : Subgroup l2 G)
+  where
+
+  is-perfect-prop-Subgroup : Prop (l1 ⊔ l2)
+  is-perfect-prop-Subgroup = is-perfect-prop-Group (group-Subgroup G H)
+
+  is-perfect-Subgroup : UU (l1 ⊔ l2)
+  is-perfect-Subgroup = type-Prop is-perfect-prop-Subgroup
+
+  is-prop-is-perfect-Subgroup : is-prop is-perfect-Subgroup
+  is-prop-is-perfect-Subgroup = is-prop-type-Prop is-perfect-prop-Subgroup
+```
+
+## External links
+
+A wikidata identifier was not available for this concept.