Merge branch 'master' into ps/rr/sugroup_group_of_maximal_subgroup_is…

…_iso_to_original_group

theories/Algebra/AbGroups/Centralizer.v

@@ -11,10 +11,8 @@ Local Open Scope mc_mult_scope.
 Definition centralizer {G : Group} (g : G)
   := fun h => g * h = h * g.
 
-Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit.
-Proof.
-  exact (grp_unit_r _ @ (grp_unit_l _)^).
-Defined.
+Definition centralizer_unit {G : Group} (g : G) : centralizer g mon_unit
+  := grp_g1_1g _ _ idpath.
 
 Definition centralizer_sgop {G : Group} (g h k : G)
            (p : centralizer g h) (q : centralizer g k)
@@ -33,7 +31,7 @@ Definition centralizer_inverse {G : Group} (g h : G)
 Proof.
   unfold centralizer in *.
   symmetry.
-  refine ((grp_unit_r _)^ @ _ @ grp_unit_l _).
+  apply grp_g1_1g.
   refine (ap ((_ * g) *.) (grp_inv_r h)^ @ _ @ ap (.* (g * _)) (grp_inv_l h)).
   refine (grp_assoc _ _ _ @ _ @ (grp_assoc _ _ _)^).
   refine (ap (.* h^) _).

theories/Algebra/Groups/Group.v

@@ -465,6 +465,12 @@ Section GroupEquations.
   Definition grp_inv_gV_g : (x * y^) * y = x
     := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_l y) @ grp_unit_r x.
 
+  Definition grp_1g_g1 : x = y <~> 1 * x = y * 1
+    := equiv_concat_r (grp_unit_r _)^ _ oE equiv_concat_l (grp_unit_l _) _.
+
+  Definition grp_g1_1g : x = y <~> x * 1 = 1 * y
+    := equiv_concat_r (grp_unit_l _)^ _ oE equiv_concat_l (grp_unit_r _) _.
+
 End GroupEquations.
 
 (** ** Cancelation lemmas *)
@@ -678,7 +684,7 @@ Definition grp_pow_commutes {G : Group} (n : Int) (g h : G)
   : h * (grp_pow g n) = (grp_pow g n) * h.
 Proof.
   induction n.
-  - exact (grp_unit_r _ @ (grp_unit_l _)^).
+  - by apply grp_g1_1g.
   - rewrite grp_pow_succ.
     nrapply grp_commutes_op; assumption.
   - rewrite grp_pow_pred.
@@ -1168,8 +1174,7 @@ Definition grp_conj_unit {G : Group} : grp_conj (G:=G) 1 $== Id _.
 Proof.
   intros x.
   apply grp_moveR_gV.
-  rhs nrapply grp_unit_r.
-  nrapply grp_unit_l.
+  by nrapply grp_1g_g1.
 Defined.
 
 (** Conjugation commutes with group homomorphisms. *)

theories/Algebra/Groups/Subgroup.v

@@ -1,4 +1,4 @@
-Require Import Basics Types HFiber WildCat.Core.
+Require Import Basics Types HFiber WildCat.Core WildCat.Equiv.
 Require Import Truncations.Core.
 Require Import Algebra.Groups.Group TruncType.
 
@@ -188,6 +188,13 @@ Proof.
   apply inverse_mon_unit.
 Defined.
 
+Definition trivial_subgroup_rec {G : Group} (H : Subgroup G)
+  : forall x, trivial_subgroup G x -> H x.
+Proof.
+  snrapply paths_ind_r; cbn beta.
+  apply issubgroup_in_unit.
+Defined.
+
 (** The preimage of a subgroup under a group homomorphism is a subgroup. *)
 Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
   : Subgroup G.
@@ -497,14 +504,38 @@ Proof.
   exact p.
 Defined.
 
-(** The property of being the trivial subgroup is useful. *)
-Definition IsTrivialSubgroup {G : Group} (H : Subgroup G) : Type :=
-  forall x, H x <-> trivial_subgroup G x.
-Existing Class IsTrivialSubgroup.
-
-Global Instance istrivialsubgroup_trivial_subgroup {G : Group}
-  : IsTrivialSubgroup (@trivial_subgroup G)
-  := ltac:(hnf; reflexivity).
+(** The property of being the trivial group is useful. Note that any group can be automatically coerced to its maximal subgroup, so it makes sense for this predicate to be applied to groups in general. *)
+Class IsTrivialGroup@{i} {G : Group@{i}} (H : Subgroup@{i i} G) :=
+  istrivialgroup : forall x, H x -> trivial_subgroup G x.
+
+Global Instance istrivial_trivial_subgroup {G : Group}
+  : IsTrivialGroup (trivial_subgroup G)
+  := fun x => idmap.
+
+(** Trivial groups are isomorphic to the trivial group. *)
+Definition istrivial_iff_grp_iso_trivial_subgroup {G : Group} (H : Subgroup G)
+  : IsTrivialGroup H
+    <-> (subgroup_group H $<~> subgroup_group (trivial_subgroup G)).
+Proof.
+  split.
+  - intros T.
+    snrapply Build_GroupIsomorphism'.
+    + snrapply equiv_functor_sigma_id.
+      intros x.
+      rapply equiv_iff_hprop_uncurried.
+      split; only 1: apply T.
+      apply trivial_subgroup_rec.
+    + intros [x Hx] [y Hy].
+      by rapply path_sigma_hprop.
+  - unfold IsTrivialGroup.
+    intros e x h.
+    change ((x; h).1 = (1; idpath).1).
+    snrapply (pr1_path (u:=(_;_)) (v:=(_;_))).
+    1: apply subgroup_in_unit.
+    rhs_V nrapply (grp_homo_unit e^-1$).
+    apply moveL_equiv_V.
+    apply path_contr.
+Defined.
 
 (** Intersection of two subgroups *)
 Definition subgroup_intersection {G : Group} (H K : Subgroup G) : Subgroup G.