Merge branch 'master' into ps/rr/conjugation_of_group_elements

theories/Algebra/AbGroups/AbelianGroup.v

@@ -179,6 +179,13 @@ Proof.
   all: intro A; apply ispointedcat_group.
 Defined.
 
+(** [abgroup_group] is a functor *)
+Global Instance is0functor_abgroup_group : Is0Functor abgroup_group
+  := is0functor_induced _.
+
+Global Instance is1functor_abgroup_group : Is1Functor abgroup_group
+  := is1functor_induced _.
+
 (** Image of group homomorphisms between abelian groups *)
 Definition abgroup_image {A B : AbGroup} (f : A $-> B) : AbGroup
   := Build_AbGroup (grp_image f) _.

theories/Algebra/Groups/Group.v

@@ -453,6 +453,18 @@ Section GroupEquations.
   (** The inverse of the unit is the unit. *)
   Definition grp_inv_unit : mon_unit^ = mon_unit := inverse_mon_unit (G :=G).
 
+  Definition grp_inv_V_gg : x^ * (x * y) = y
+    := grp_assoc _ _ _ @ ap (.* y) (grp_inv_l x) @ grp_unit_l y.
+
+  Definition grp_inv_g_Vg : x * (x^ * y) = y
+    := grp_assoc _ _ _ @ ap (.* y) (grp_inv_r x) @ grp_unit_l y.
+
+  Definition grp_inv_gg_V : (x * y) * y^ = x
+    := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_r y) @ grp_unit_r x.
+
+  Definition grp_inv_gV_g : (x * y^) * y = x
+    := (grp_assoc _ _ _)^ @ ap (x *.) (grp_inv_l y) @ grp_unit_r x.
+
 End GroupEquations.
 
 (** ** Cancelation lemmas *)
@@ -508,20 +520,29 @@ Section GroupMovement.
 
   (** *** Moving elements equal to unit. *)
 
-  Definition grp_moveL_1M : x * y^ = mon_unit <~> x = y
+  Definition grp_moveL_1M : x * y^ = 1 <~> x = y
     := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gM.
 
-  Definition grp_moveL_1V : x * y = mon_unit <~> x = y^
-    := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV.
-
-  Definition grp_moveL_M1 : y^ * x = mon_unit <~> x = y
+  Definition grp_moveL_M1 : y^ * x = 1 <~> x = y
     := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Mg.
+
+  Definition grp_moveL_1V : x * y = 1 <~> x = y^
+    := equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV.
+
+  Definition grp_moveL_V1 : y * x = 1 <~> x = y^
+    := equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Vg.
 
-  Definition grp_moveR_1M : mon_unit = y * x^ <~> x = y
-    := (equiv_concat_l (grp_unit_l _) _)^-1%equiv oE grp_moveR_gM.
+  Definition grp_moveR_1M : 1 = y * x^ <~> x = y
+    := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gM.
+
+  Definition grp_moveR_M1 : 1 = x^ * y <~> x = y
+    := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Mg.
+
+  Definition grp_moveR_1V : 1 = y * x <~> x^ = y
+    := (equiv_concat_l (grp_unit_l _) _)^-1 oE grp_moveR_gV.
 
-  Definition grp_moveR_M1 : mon_unit = x^ * y <~> x = y
-    := (equiv_concat_l (grp_unit_r _) _)^-1%equiv oE grp_moveR_Mg.
+  Definition grp_moveR_V1 : mon_unit = x * y <~> x^ = y
+    := (equiv_concat_l (grp_unit_r _) _)^-1 oE grp_moveR_Vg.
 
   (** *** Cancelling elements equal to unit. *)
 

theories/Algebra/Groups/Kernel.v

@@ -57,7 +57,7 @@ Defined.
 
 (** ** Characterisation of group embeddings *)
 Proposition equiv_kernel_isembedding `{Univalence} {A B : Group} (f : A $-> B)
-  : (grp_kernel f = trivial_subgroup :> Subgroup A) <~> IsEmbedding f.
+  : (grp_kernel f = trivial_subgroup A :> Subgroup A) <~> IsEmbedding f.
 Proof.
   refine (_ oE (equiv_path_subgroup' _ _)^-1%equiv).
   apply equiv_iff_hprop_uncurried.

theories/Algebra/Groups/ShortExactSequence.v

@@ -52,6 +52,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 :> Subgroup _)
+      <~> (grp_kernel f = trivial_subgroup A :> Subgroup _)
   := (equiv_kernel_isembedding f)^-1%equiv
        oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).

theories/Algebra/Groups/Subgroup.v

@@ -178,7 +178,7 @@ Definition issig_subgroup {G : Group} : _ <~> Subgroup G
   := ltac:(issig).
 
 (** Trivial subgroup *)
-Definition trivial_subgroup {G} : Subgroup G.
+Definition trivial_subgroup G : Subgroup G.
 Proof.
   rapply (Build_Subgroup' (fun x => x = mon_unit)).
   1: reflexivity.
@@ -205,12 +205,16 @@ Proof.
 Defined.
 
 (** Every group is a (maximal) subgroup of itself *)
-Definition maximal_subgroup {G} : Subgroup G.
+Definition maximal_subgroup G : Subgroup G.
 Proof.
   rapply (Build_Subgroup G (fun x => Unit)).
   split; auto; exact _.
 Defined.
 
+(** We wish to coerce a group to its maximal subgroup. However, if we don't explicitly print [maximal_subgroup] things can get confusing, so we mark it as a coercion to be printed. *)
+Coercion maximal_subgroup : Group >-> Subgroup.
+Add Printing Coercion maximal_subgroup.
+
 (** Paths between subgroups correspond to homotopies between the underlying predicates. *) 
 Proposition equiv_path_subgroup `{F : Funext} {G : Group} (H K : Subgroup G)
   : (H == K) <~> (H = K).
@@ -368,7 +372,7 @@ Coercion normalsubgroup_subgroup : NormalSubgroup >-> Subgroup.
 Global Existing Instance normalsubgroup_isnormal.
 
 Definition equiv_symmetric_in_normalsubgroup {G : Group}
-  (N : NormalSubgroup G)
+  (N : Subgroup G) `{!IsNormalSubgroup N}
   : forall x y, N (x * y) <~> N (y * x).
 Proof.
   intros x y.
@@ -377,15 +381,12 @@ Proof.
 Defined.
 
 (** Our definiiton of normal subgroup implies the usual definition of invariance under conjugation. *)
-Definition isnormal_conjugate {G : Group} (N : NormalSubgroup G) {x y : G}
-  : N x -> N (y * x * y^).
+Definition isnormal_conj {G : Group} (N : Subgroup G)
+  `{!IsNormalSubgroup N} {x y : G}
+  : N x <~> N (y * x * y^).
 Proof.
-  intros n.
-  apply isnormal.
-  nrefine (transport N (grp_assoc _ _ _)^ _).
-  nrefine (transport (fun y => N (y * x)) (grp_inv_l _)^ _).
-  nrefine (transport N (grp_unit_l _)^ _).
-  exact n.
+  srefine (equiv_symmetric_in_normalsubgroup N _ _ oE _).
+  by rewrite grp_inv_V_gg.
 Defined.
 
 (** We can show a subgroup is normal if it is invariant under conjugation. *)
@@ -414,7 +415,7 @@ Definition equiv_isnormal_conjugate `{Funext} {G : Group} (N : Subgroup G)
 Proof.
   rapply equiv_iff_hprop.
   - intros is_normal x y.
-    exact (isnormal_conjugate (Build_NormalSubgroup G N is_normal)).
+    rapply isnormal_conj.
   - intros is_normal'.
     by snrapply Build_IsNormalSubgroup'.
 Defined.
@@ -473,7 +474,7 @@ Defined.
 
 (** The property of being the trivial subgroup is useful. *)
 Definition IsTrivialSubgroup {G : Group} (H : Subgroup G) : Type :=
-  forall x, H x <-> trivial_subgroup x.
+  forall x, H x <-> trivial_subgroup G x.
 Existing Class IsTrivialSubgroup.
 
 Global Instance istrivialsubgroup_trivial_subgroup {G : Group}

theories/Algebra/Rings/Ideal.v

@@ -143,7 +143,7 @@ End IdealElements.
 
 (** The trivial subgroup is a left ideal. *)
 Global Instance isleftideal_trivial_subgroup (R : Ring)
-  : IsLeftIdeal (R := R) trivial_subgroup.
+  : IsLeftIdeal (trivial_subgroup R).
 Proof.
   intros r x p.
   rhs_V nrapply (rng_mult_zero_r).
@@ -152,12 +152,12 @@ Defined.
 
 (** The trivial subgroup is a right ideal. *)
 Global Instance isrightideal_trivial_subgroup (R : Ring)
-  : IsRightIdeal (R := R) trivial_subgroup
+  : IsRightIdeal (trivial_subgroup R)
   := isleftideal_trivial_subgroup _.
 
 (** The trivial subgroup is an ideal. *)
 Global Instance isideal_trivial_subgroup (R : Ring)
-  : IsIdeal (R := R) trivial_subgroup
+  : IsIdeal (trivial_subgroup R)
   := {}.
 
 (** We call the trivial subgroup the "zero ideal". *)
@@ -167,17 +167,17 @@ Definition ideal_zero (R : Ring) : Ideal R := Build_Ideal R _ _.
 
 (** The maximal subgroup is a left ideal. *)
 Global Instance isleftideal_maximal_subgroup (R : Ring)
-  : IsLeftIdeal (R := R) maximal_subgroup
+  : IsLeftIdeal (maximal_subgroup R)
   := ltac:(done).
 
 (** The maximal subgroup is a right ideal. *)
 Global Instance isrightideal_maximal_subgroup (R : Ring)
-  : IsRightIdeal (R := R) maximal_subgroup
+  : IsRightIdeal (maximal_subgroup R)
   := isleftideal_maximal_subgroup _.
 
 (** The maximal subgroup is an ideal.  *)
 Global Instance isideal_maximal_subgroup (R : Ring)
-  : IsIdeal (R:=R) maximal_subgroup
+  : IsIdeal (maximal_subgroup R)
   := {}.
 
 (** We call the maximal subgroup the "unit ideal". *)