associativity of ideal product

theories/Algebra/Groups/Subgroup.v

@@ -188,6 +188,22 @@ Proof.
   apply negate_mon_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.
+Proof.
+  snrapply Build_Subgroup'.
+  - exact (S o f).
+  - hnf; exact _.
+  - nrefine (transport S (grp_homo_unit f)^ _).
+    apply subgroup_in_unit.
+  - hnf; intros x y Sfx Sfy.
+    nrefine (transport S (grp_homo_op f _ _)^ _).
+    nrapply subgroup_in_op; only 1: assumption.
+    nrefine (transport S (grp_homo_inv f _)^ _).
+    by apply subgroup_in_inv.
+Defined.
+
 (** Every group is a (maximal) subgroup of itself *)
 Definition maximal_subgroup {G} : Subgroup G.
 Proof.
@@ -537,20 +553,28 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H :
   : subgroup_generated X
   := (g; tr (sgt_in H)).
 
+(** If generators are contained in another subgroup [H], then the subgroup they generate is contained in [H]. *)
+Definition subgroup_generated_subset_subgroup {G : Group} (X : G -> Type)
+  (H : Subgroup G)
+  (gen_in : forall g, X g -> H g)
+  : forall g, subgroup_generated X g -> H g.
+Proof.
+  intro g.
+  rapply Trunc_rec.
+  intro p; induction p as [g i | | g h p1 IHp1 p2 IHp2].
+  - apply gen_in, i.
+  - apply issubgroup_in_unit.
+  - by apply issubgroup_in_op_inv.
+Defined.
+
 (** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *)
 Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type)
   (f : G $-> H) (preserves : forall g, X g -> Y (f g))
   : forall g, subgroup_generated X g -> subgroup_generated Y (f g).
 Proof.
-  intro g.
-  apply Trunc_functor.
-  intro p.
-  induction p as [g i | | g h p1 IHp1 p2 IHp2].
-  - apply sgt_in, preserves, i.
-  - rewrite grp_homo_unit.
-    apply sgt_unit.
-  - rewrite grp_homo_op, grp_homo_inv.
-    by apply sgt_op.
+  apply (subgroup_generated_subset_subgroup X (subgroup_preimage f (subgroup_generated Y))).
+  intros g p; cbn.
+  apply tr, sgt_in, preserves, p.
 Defined.
 
 (** The product of two subgroups. *)