From 6491fd34ac2aeec4d43217b8d7da41f0da0e7ddb Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Wed, 15 Jan 2025 04:00:59 +0100
Subject: [PATCH] quotient is trivial iff subgroup is maximal

<!-- ps-id: 44cdcb20-64cf-4d05-8292-1e1887cd2b7c -->

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

diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
index f8b22f2729..21ea46dd7e 100644
--- a/theories/Algebra/Groups/QuotientGroup.v
+++ b/theories/Algebra/Groups/QuotientGroup.v
@@ -322,3 +322,29 @@ Definition grp_quotient_trivial (G : Group) (N : NormalSubgroup G)
   (triv : IsTrivialGroup N)
   : G $<~> G / N
   := Build_CatEquiv grp_quotient_map.
+
+(** A quotient by a maximal subgroup is trivial. *)
+Global Instance istrivial_grp_quotient_maximal
+  (G : Group) (N : NormalSubgroup G)
+  : IsMaximalSubgroup N -> IsTrivialGroup (G / N).
+Proof.
+  intros max x _; revert x.
+  rapply grp_quotient_ind_hprop.
+  intros x.
+  apply qglue, max.
+Defined.
+
+(** Conversely, a trivial quotient means the subgroup is maximal. *)
+Definition ismaximalsubgroup_istrivial_grp_quotient `{Univalence}
+  (G : Group) (N : NormalSubgroup G)
+  : IsTrivialGroup (G / N) -> IsMaximalSubgroup N.
+Proof.
+  intros triv x.
+  specialize (triv (grp_quotient_map x) tt).
+  simpl in triv.
+  apply related_quotient_paths in triv.
+  2-5: exact _.
+  apply equiv_subgroup_inverse.
+  nrapply (subgroup_in_op_l _ _ 1 triv) .
+  apply subgroup_in_unit.
+Defined.