quotient by a trivial group

theories/Algebra/AbSES/Core.v

@@ -172,7 +172,7 @@ Proof.
     refine ((grp_assoc _ _ _)^ @ _).
     refine (ap _ (left_inverse (phi e0.1)) @ _).
     apply grp_unit_r.
-  - apply isembedding_grouphomomorphism.
+  - apply isembedding_istrivial_kernel.
     intros e p.
     assert (a : Tr (-1) (hfiber (inclusion E) e)).
     1: { refine (isexact_preimage _ (inclusion E) (projection E) _ _).

theories/Algebra/AbSES/PullbackFiberSequence.v

@@ -71,7 +71,7 @@ Proof.
     intro b.
     refine (ap (projection E) (abses_pullback_inclusion_transpose_beta (inclusion E) F p b) @ _).
     apply iscomplex_abses.
-  - apply isembedding_grouphomomorphism.
+  - apply isembedding_istrivial_kernel.
     intros a q0.
     (* Since [inclusion F a] is killed by [grp_quotient_map], its in the image of [B]. *)
     pose proof (in_coset := related_quotient_paths _ _ _ q0).

theories/Algebra/Groups/Group.v

@@ -1098,25 +1098,6 @@ Global Instance isfreegroup_isfreegroupon (S : Type) (F_S : Group) (i : S -> F_S
 
 (** ** Further properties of group homomorphisms. *)
 
-(** Characterisation of injective group homomorphisms. *)
-Lemma isembedding_grouphomomorphism {A B : Group} (f : A $-> B)
-  : (forall a, f a = group_unit -> a = group_unit) <-> IsEmbedding f.
-Proof.
-  split.
-  - intros h b.
-    apply hprop_allpath.
-    intros [a0 p0] [a1 p1].
-    srapply path_sigma_hprop; simpl.
-    apply grp_moveL_1M.
-    apply h.
-    rewrite grp_homo_op, grp_homo_inv.
-    rewrite p0, p1.
-    apply right_inverse.
-  - intros E a p.
-    rapply (isinj_embedding f).
-    exact (p @ (grp_homo_unit f)^).
-Defined.
-
 (** Commutativity can be transferred across isomorphisms. *)
 Definition commutative_iso_commutative {G H : Group}
   {C : Commutative (@group_sgop G)} (f : GroupIsomorphism G H)

theories/Algebra/Groups/Kernel.v

@@ -2,26 +2,26 @@ Require Import Basics Types.
 Require Import Algebra.Groups.Group.
 Require Import Algebra.Groups.Subgroup.
 Require Import WildCat.Core.
+Require Import Universes.HSet.
 
 (** * Kernels of group homomorphisms *)
 
 Local Open Scope mc_scope.
 Local Open Scope mc_mult_scope.
-Local Open Scope path_scope.
 
 Definition grp_kernel {A B : Group} (f : GroupHomomorphism A B) : NormalSubgroup A.
 Proof.
   snrapply Build_NormalSubgroup.
-  - srapply (Build_Subgroup' (fun x => f x = group_unit)); cbn beta.
+  - srapply (Build_Subgroup' (fun x => f x = 1)); cbn beta.
     1: apply grp_homo_unit.
     intros x y p q.
     apply (grp_homo_moveL_1M _ _ _)^-1.
     exact (p @ q^).
   - intros x y; cbn; intros p.
     apply (grp_homo_moveL_1V _ _ _)^-1.
     lhs_V nrapply grp_inv_inv.
-    apply (ap (-)).
-    exact (grp_homo_moveL_1V f x y p)^.
+    nrapply (ap (-) _^).
+    by apply grp_homo_moveL_1V.
 Defined.
 
 (** ** Corecursion principle for group kernels *)
@@ -55,17 +55,40 @@ Proof.
     apply path_sigma_hprop; reflexivity.
 Defined.
 
-(** ** Characterisation of group embeddings *)
-Proposition equiv_kernel_isembedding `{Univalence} {A B : Group} (f : A $-> B)
-  : (grp_kernel f = trivial_subgroup A :> Subgroup A) <~> IsEmbedding f.
+(** The underlying map of a group homomorphism with a trivial kernel is an embedding. *)
+Global Instance isembedding_istrivial_kernel {G H : Group} (f : G $-> H)
+  (triv : IsTrivialGroup (grp_kernel f))
+  : IsEmbedding f.
+Proof.
+  intros h.
+  apply hprop_allpath.
+  intros [x p] [y q].
+  srapply path_sigma_hprop; unfold pr1.
+  apply grp_moveL_1M.
+  apply triv; simpl.
+  rhs_V nrapply (grp_inv_r h).
+  lhs nrapply grp_homo_op.
+  nrapply (ap011 (.*.) p).
+  lhs nrapply grp_homo_inv.
+  exact (ap (^) q).
+Defined.
+
+(** If the underlying map of a group homomorphism is an embedding then the kernel is trivial. *)
+Definition istrivial_kernel_isembedding {G H : Group} (f : G $-> H)
+  (emb : IsEmbedding f)
+  : IsTrivialGroup (grp_kernel f).
+Proof.
+  intros g p.
+  rapply (isinj_embedding f).
+  exact (p @ (grp_homo_unit f)^).
+Defined.
+Global Hint Immediate istrivial_kernel_isembedding : typeclass_instances.
+
+(** Characterisation of group embeddings *)
+Proposition equiv_istrivial_kernel_isembedding `{F : Funext}
+  {G H : Group} (f : G $-> H)
+  : IsTrivialGroup (grp_kernel f) <~> IsEmbedding f.
 Proof.
-  refine (_ oE (equiv_path_subgroup' _ _)^-1%equiv).
   apply equiv_iff_hprop_uncurried.
-  refine (iff_compose _ (isembedding_grouphomomorphism f)); split.
-  - intros E ? ?.
-    by apply E.
-  - intros e a; split.
-    + apply e.
-    + intro p.
-      exact (ap _ p @ grp_homo_unit f).
+  split; exact _.
 Defined.

theories/Algebra/Groups/QuotientGroup.v

@@ -304,3 +304,21 @@ Proof.
     + srapply path_sigma_hprop.
       reflexivity.
 Defined.
+
+(** When the normal subgroup [N] is trivial, the inclusion map [G $-> G / N] is an isomorphism. *)
+Global Instance catie_grp_quotient_map_trivial {G : Group} (N : NormalSubgroup G)
+  (triv : IsTrivialGroup N)
+  : CatIsEquiv (@grp_quotient_map G N).
+Proof.
+  snrapply catie_adjointify.
+  - srapply (grp_quotient_rec _ _ (Id _)).
+    apply triv.
+  - by srapply grp_quotient_ind_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)
+  (triv : IsTrivialGroup N)
+  : G $<~> G / N
+  := Build_CatEquiv grp_quotient_map.

theories/Algebra/Groups/ShortExactSequence.v

@@ -51,7 +51,6 @@ Defined.
 
 (** A complex 0 -> A -> B is purely exact if and only if the kernel of the map A -> B is trivial. *)
 Definition equiv_grp_isexact_kernel `{Univalence} {A B : Group} (f : A $-> B)
-  : IsExact purely (grp_trivial_rec A) f
-      <~> (grp_kernel f = trivial_subgroup A :> Subgroup _)
-  := (equiv_kernel_isembedding f)^-1%equiv
+  : IsExact purely (grp_trivial_rec A) f <~> IsTrivialGroup (grp_kernel f)
+  := (equiv_istrivial_kernel_isembedding f)^-1%equiv
        oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).

theories/Algebra/Groups/Subgroup.v

@@ -499,6 +499,10 @@ Defined.
 Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) :=
   istrivialgroup : forall x, H x -> trivial_subgroup G x.
 
+Global Instance ishprop_istrivialgroup `{F : Funext} {G : Group} (H : Subgroup G)
+  : IsHProp (IsTrivialGroup H)
+  := istrunc_forall.
+
 Global Instance istrivial_trivial_subgroup {G : Group}
   : IsTrivialGroup (trivial_subgroup G)
   := fun x => idmap.