quotient by a trivial group

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jan 4, 2025 · dcc21b2 · dcc21b2
1 parent ff0cbd5
commit dcc21b2
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
@@ -304,3 +304,16 @@ Proof.
     + srapply path_sigma_hprop.
       reflexivity.
 Defined.
+
+(** The group quotient by a trivial group is isomorphic to the original group. *)
+Definition grp_quotient_trivial (G : Group) (N : NormalSubgroup G)
+  : IsTrivialGroup N -> G / N ≅ G.
+Proof.
+  intros T.
+  snrapply cate_adjointify.
+  - srapply (grp_quotient_rec _ _ (Id _)).
+    apply T.
+  - srapply grp_quotient_map.
+  - reflexivity.
+  - by srapply grp_quotient_ind_hprop.
+Defined.