Merge pull request #2030 from Alizter/ps/rr/revise_definition_of_norm…

…al_subgroup

revise definition of normal subgroup

theories/Algebra/AbGroups/AbelianGroup.v

@@ -80,11 +80,8 @@ Coercion abgroup_subgroup : Subgroup >-> AbGroup.
 Global Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G)
   : IsNormalSubgroup H.
 Proof.
-  intros x y; unfold in_cosetL, in_cosetR.
-  refine (_ oE equiv_subgroup_inverse _ _).
-  rewrite negate_sg_op.
-  rewrite negate_involutive.
-  by rewrite (commutativity (-y) x).
+  intros x y h.
+  by rewrite ab_comm.
 Defined.
 
 (** ** Quotients of abelian groups *)

theories/Algebra/Groups/Group.v

@@ -983,3 +983,16 @@ Proof.
   rhs nrapply grp_homo_op.
   exact (ap011 _ p q).
 Defined.
+
+(** The group movement lemmas can be extended to when there is a homomorphism involved.  For now, we only include these two. *)
+Definition grp_homo_moveL_1V {A B : Group} (f : GroupHomomorphism A B) (x y : A)
+  : f (x * y) = group_unit <~> (f x = - f y)
+  := grp_moveL_1V oE equiv_concat_l (grp_homo_op f x y)^ _.
+
+Definition grp_homo_moveL_1M  {A B : Group} (f : GroupHomomorphism A B) (x y : A)
+  : f (x * -y) = group_unit <~> (f x = f y).
+Proof.
+  refine (grp_moveL_1M oE equiv_concat_l _^ _).
+  lhs nrapply grp_homo_op.
+  apply ap, grp_homo_inv.
+Defined.

theories/Algebra/Groups/Kernel.v

@@ -11,19 +11,17 @@ Local Open Scope mc_mult_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)).
+  - srapply (Build_Subgroup' (fun x => f x = group_unit)); cbn beta.
     1: apply grp_homo_unit.
-    intros x y p q; cbn in p, q; cbn.
-    refine (grp_homo_op _ _ _ @ ap011 _ p _ @ _).
-    1: apply grp_homo_inv.
-    rewrite q; apply right_inverse.
-  - intros x y; cbn.
-    rewrite 2 grp_homo_op.
-    rewrite 2 grp_homo_inv.
-    refine (_^-1 oE grp_moveL_M1).
-    refine (_ oE equiv_path_inverse _ _).
-    apply grp_moveR_1M.
-  Defined.
+    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)^.
+Defined.
 
 (** ** Corecursion principle for group kernels *)
 

theories/Algebra/Groups/Subgroup.v

@@ -337,39 +337,93 @@ Proof.
   all: by intro.
 Defined.
 
-(** A subgroup is normal if being in a left coset is equivalent to being in a right coset represented by the same element. *)
+(** A normal subgroup is a subgroup closed under conjugation. *)
 Class IsNormalSubgroup {G : Group} (N : Subgroup G)
-  := isnormal : forall {x y}, in_cosetL N x y <~> in_cosetR N x y.
+  := isnormal : forall {x y}, N (x * y) -> N (y * x).
 
 Record NormalSubgroup (G : Group) := {
   normalsubgroup_subgroup : Subgroup G ;
   normalsubgroup_isnormal : IsNormalSubgroup normalsubgroup_subgroup ;
 }.
 
+Arguments Build_NormalSubgroup G N _ : rename.
+
 Coercion normalsubgroup_subgroup : NormalSubgroup >-> Subgroup.
 Global Existing Instance normalsubgroup_isnormal.
 
-(* Inverses are then respected *)
-Definition in_cosetL_inverse {G : Group} {N : NormalSubgroup G}
-  : forall x y : G, in_cosetL N (-x) (-y) <~> in_cosetL N x y.
+Definition equiv_symmetric_in_normalsubgroup {G : Group}
+  (N : NormalSubgroup G)
+  : forall x y, N (x * y) <~> N (y * x).
 Proof.
   intros x y.
-  unfold in_cosetL.
-  rewrite negate_involutive.
-  symmetry; apply isnormal.
+  rapply equiv_iff_hprop.
+  all: apply isnormal.
 Defined.
 
-Definition in_cosetR_inverse {G : Group} {N : NormalSubgroup G}
-  : forall x y : G, in_cosetR N (-x) (-y) <~> in_cosetR N x y.
+(** 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).
 Proof.
-  intros x y.
-  refine (_ oE (in_cosetR_unit _ _)^-1).
-  refine (_ oE isnormal^-1).
-  refine (_ oE in_cosetL_unit _ _).
-  refine (_ oE isnormal).
+  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.
+Defined.
+
+(** We can show a subgroup is normal if it is invariant under conjugation. *)
+Definition Build_IsNormalSubgroup' (G : Group) (N : Subgroup G)
+  (isnormal : forall x y, N x -> N (y * x * -y))
+  : IsNormalSubgroup N.
+Proof.
+  intros x y n.
+  nrefine (transport N (grp_unit_r _) _).
+  nrefine (transport (fun z => N (_ * z)) (grp_inv_r y) _).
+  nrefine (transport N (grp_assoc _ _ _)^ _).
+  nrefine (transport (fun z => N (z * _)) (grp_assoc _ _ _) _).
+  by apply isnormal.
+Defined.
+
+(** Under funext, being a normal subgroup is a hprop. *)
+Global Instance ishprop_isnormalsubgroup `{Funext} {G : Group} (N : Subgroup G)
+  : IsHProp (IsNormalSubgroup N).
+Proof. 
+  unfold IsNormalSubgroup; exact _.
+Defined.
+
+(** Our definition of normal subgroup and the usual definition are therefore equivalent. *)
+Definition equiv_isnormal_conjugate `{Funext} {G : Group} (N : Subgroup G)
+  : IsNormalSubgroup N <~> (forall x y, N x -> N (y * x * -y)).
+Proof.
+  rapply equiv_iff_hprop.
+  - intros is_normal x y.
+    exact (isnormal_conjugate (Build_NormalSubgroup G N is_normal)).
+  - intros is_normal'.
+    by snrapply Build_IsNormalSubgroup'.
+Defined.
+
+(** Left and right cosets are equivalent in normal subgroups. *)
+Definition equiv_in_cosetL_in_cosetR_normalsubgroup {G : Group}
+  (N : NormalSubgroup G) (x y : G)
+  : in_cosetL N x y <~> in_cosetR N x y
+  := equiv_in_cosetR_symm _ _ oE equiv_symmetric_in_normalsubgroup _ _ _.
+
+(** Inverses are then respected *)
+Definition in_cosetL_inverse {G : Group} {N : NormalSubgroup G} (x y : G)
+  : in_cosetL N (-x) (-y) <~> in_cosetL N x y.
+Proof.
+  refine (_ oE equiv_in_cosetL_in_cosetR_normalsubgroup _ _ _); cbn.
   by rewrite negate_involutive.
 Defined.
 
+Definition in_cosetR_inverse {G : Group} {N : NormalSubgroup G} (x y : G)
+  : in_cosetR N (-x) (-y) <~> in_cosetR N x y.
+Proof.
+  refine (_ oE equiv_in_cosetL_in_cosetR_normalsubgroup _ _ _); cbn.
+  by rewrite grp_inv_inv.
+Defined.
+
 (** This lets us prove that left and right coset relations are congruences. *)
 Definition in_cosetL_cong {G : Group} {N : NormalSubgroup G}
   (x x' y y' : G)
@@ -378,13 +432,12 @@ Proof.
   cbn; intros p q.
   (** rewrite goal before applying subgroup_op *)
   rewrite negate_sg_op, <- simple_associativity.
-  apply symmetric_in_cosetL; cbn.
-  rewrite simple_associativity.
-  apply isnormal; cbn.
-  rewrite <- simple_associativity.
+  apply isnormal.
+  rewrite simple_associativity, <- simple_associativity.
   apply subgroup_in_op.
-  1: assumption.
-  by apply isnormal, symmetric_in_cosetL.
+  1: exact p.
+  apply isnormal.
+  exact q.
 Defined.
 
 Definition in_cosetR_cong  {G : Group} {N : NormalSubgroup G}
@@ -394,13 +447,12 @@ Proof.
   cbn; intros p q.
   (** rewrite goal before applying subgroup_op *)
   rewrite negate_sg_op, simple_associativity.
-  apply symmetric_in_cosetR; cbn.
-  rewrite <- simple_associativity.
-  apply isnormal; cbn.
-  rewrite simple_associativity.
+  apply isnormal.
+  rewrite <- simple_associativity, simple_associativity.
   apply subgroup_in_op.
-  2: assumption.
-  by apply isnormal, symmetric_in_cosetR.
+  2: exact q.
+  apply isnormal.
+  exact p.
 Defined.
 
 (** The property of being the trivial subgroup is useful. *)