Merge pull request #2029 from Alizter/ps/rr/remove_isunitpreserving_f…

…rom_grouphomomorphism

remove IsUnitPreserving from GroupHomomorphism

theories/Algebra/Groups/FreeGroup.v

@@ -428,7 +428,7 @@ Proof.
   intros k G g.
   specialize (k G).
   snrapply contr_equiv'.
-  1: exact (hfiber (fun f x => grp_homo_map F G f (i x)) g).
+  1: exact (hfiber (fun f x => grp_homo_map f (i x)) g).
   { rapply equiv_functor_sigma_id.
     intro y; symmetry.
     apply equiv_path_forall. }
@@ -478,7 +478,7 @@ Section FreeGroupGenerated.
     snrapply issurj_retr.
     - apply to_subgroup_generated.
     - apply ap10; cbn.
-      exact (ap (grp_homo_map F_S F_S) (is_retraction)).
+      exact (ap grp_homo_map is_retraction).
   Defined.
 
   (* Therefore, the inclusion map is an equivalence, since it is known to be an embedding. *)

theories/Algebra/Groups/Group.v

@@ -123,14 +123,51 @@ Defined.
 (** Group homomorphisms are maps between groups that preserve the group operation. They allow us to compare groups and map their structure to one another. This is useful for determining if two groups are really the same, in which case we say they are "isomorphic". *)
 
 (** A group homomorphism consists of a map between groups and a proof that the map preserves the group operation. *)
-Record GroupHomomorphism (G H : Group) := Build_GroupHomomorphism' {
+Record GroupHomomorphism (G H : Group) := Build_GroupHomomorphism {
   grp_homo_map :> group_type G -> group_type H;
-  grp_homo_ishomo :: IsMonoidPreserving grp_homo_map;
+  issemigrouppreserving_grp_homo :: IsSemiGroupPreserving grp_homo_map;
 }.
 
+Arguments grp_homo_map {G H}.
+Arguments Build_GroupHomomorphism {G H} _ _.
+Arguments issemigrouppreserving_grp_homo {G H} f _ : rename.
+
+(** ** Basic properties of group homomorphisms *)
+
+(** Group homomorphisms preserve group operations. This is an alias for [issemigrouppreserving_grp_homo] with the identity written explicitly. *)
+Definition grp_homo_op
+  : forall {G H : Group} (f : GroupHomomorphism G H) (x y : G), f (x * y) = f x * f y
+  := @issemigrouppreserving_grp_homo.
+#[export] Hint Immediate grp_homo_op : group_db.
+
+(** Group homomorphisms are unit preserving. *)
+Global Instance isunitpreserving_grp_homo {G H : Group}
+  (f : GroupHomomorphism G H)
+  : IsUnitPreserving f.
+Proof.
+  unfold IsUnitPreserving.
+  apply (group_cancelL (f mon_unit)).
+  rhs nrapply grp_unit_r.
+  rhs_V rapply (ap  _ (monoid_left_id _ mon_unit)).
+  symmetry.
+  nrapply issemigrouppreserving_grp_homo.
+Defined.
+
+(** Group homomorphisms preserve identities. This is an alias for the previous statement. *)
+Definition grp_homo_unit
+  : forall {G H : Group} (f : GroupHomomorphism G H), f mon_unit = mon_unit
+  := @isunitpreserving_grp_homo.
+#[export] Hint Immediate grp_homo_unit : group_db.
+
+(** Therefore, group homomorphisms are monoid homomorphisms. *)
+Global Instance ismonoidpreserving_grp_homo {G H : Group}
+  (f : GroupHomomorphism G H)
+  : IsMonoidPreserving f
+  := {}.
+
 (** Group homomorphisms are pointed maps. *)
 Definition pmap_GroupHomomorphism {G H : Group} (f : GroupHomomorphism G H) : G ->* H
-  := Build_pMap G H f (@monmor_unitmor _ _ _ _ _ _ _ (@grp_homo_ishomo G H f)).
+  := Build_pMap G H f (isunitpreserving_grp_homo f).
 Coercion pmap_GroupHomomorphism : GroupHomomorphism >-> pForall.
 
 Definition issig_GroupHomomorphism (G H : Group) : _ <~> GroupHomomorphism G H
@@ -153,24 +190,6 @@ Proof.
   intros f g; apply (istrunc_equiv_istrunc _ equiv_path_grouphomomorphism).
 Defined.
 
-(** ** Basic properties of group homomorphisms *)
-
-(** Group homomorphisms preserve identities. *)
-Definition grp_homo_unit {G H} (f : GroupHomomorphism G H)
-  : f (mon_unit) = mon_unit.
-Proof.
-  apply monmor_unitmor.
-Defined.
-#[export] Hint Immediate grp_homo_unit : group_db.
-
-(** Group homomorphisms preserve group operations. *)
-Definition grp_homo_op {G H} (f : GroupHomomorphism G H)
-  : forall x y : G, f (x * y) = f x * f y.
-Proof.
-  apply monmor_sgmor.
-Defined.
-#[export] Hint Immediate grp_homo_op : group_db.
-
 (** Group homomorphisms preserve inverses. *)
 Definition grp_homo_inv {G H} (f : GroupHomomorphism G H)
   : forall x, f (- x) = -(f x).
@@ -185,25 +204,9 @@ Proof.
 Defined.
 #[export] Hint Immediate grp_homo_inv : group_db.
 
-(** When building a group homomorphism we only need that it preserves the group operation, since we can prove that the identity is preserved. *)
-Definition Build_GroupHomomorphism {G H : Group}
-  (f : G -> H) {h : IsSemiGroupPreserving f}
-  : GroupHomomorphism G H.
-Proof.
-  srapply (Build_GroupHomomorphism' _ _ f).
-  split.
-  1: exact h.
-  unfold IsUnitPreserving.
-  apply (group_cancelL (f mon_unit)).
-  refine (_ @ (grp_unit_r _)^).
-  refine (_ @ ap _ (monoid_left_id _ mon_unit)).
-  symmetry.
-  apply h.
-Defined.
-
 (** The identity map is a group homomorphism. *)
 Definition grp_homo_id {G : Group} : GroupHomomorphism G G
-  := Build_GroupHomomorphism idmap.
+  := Build_GroupHomomorphism idmap _.
 
 (** The composition of the underlying functions of two group homomorphisms is also a group homomorphism. *)
 Definition grp_homo_compose {G H K : Group}
@@ -305,34 +308,37 @@ Global Instance transitive_groupisomorphism
 Definition equiv_path_group' {U : Univalence} {G H : Group}
   : GroupIsomorphism G H <~> G = H.
 Proof.
-  refine (equiv_compose'
-    (B := sig (fun f : G <~> H => IsMonoidPreserving f)) _ _).
-  { revert G H; apply (equiv_path_issig_contr issig_group).
-    + intros [G [? [? [? ?]]]].
-      exists 1%equiv.
-      exact _.
-    + intros [G [op [unit [neg ax]]]]; cbn.
-      contr_sigsig G (equiv_idmap G).
-      srefine (Build_Contr _ ((_;(_;(_;_)));_) _); cbn.
-      1: assumption.
-      1: exact _.
-      intros [[op' [unit' [neg' ax']]] eq].
-      apply path_sigma_hprop; cbn.
-      refine (@ap _ _ (fun x : { oun :
-        { oo : SgOp G & { u : MonUnit G & Negate G}}
-        & @IsGroup G oun.1 oun.2.1 oun.2.2}
-        => (x.1.1 ; x.1.2.1 ; x.1.2.2 ; x.2))
-        ((op;unit;neg);ax) ((op';unit';neg');ax') _).
-      apply path_sigma_hprop; cbn.
-      srefine (path_sigma' _ _ _).
-      1: funext x y; apply eq.
-      rewrite transport_const.
-      srefine (path_sigma' _ _ _).
-      1: apply eq.
-      rewrite transport_const.
-      funext x.
-      exact (preserves_negate (f:=idmap) _). }
-  make_equiv.
+  equiv_via {f : G <~> H & IsSemiGroupPreserving f}.
+  1: make_equiv.
+  revert G H; apply (equiv_path_issig_contr issig_group).
+  - intros [G [? [? [? ?]]]].
+    exists 1%equiv.
+    exact _.
+  - intros [G [op [unit [neg ax]]]]; cbn.
+    contr_sigsig G (equiv_idmap G).
+    srefine (Build_Contr _ ((_;(_;(_;_)));_) _); cbn.
+    1: assumption.
+    1: exact _.
+    intros [[op' [unit' [neg' ax']]] eq].
+    apply path_sigma_hprop; cbn.
+    refine (@ap _ _ (fun x : { oun :
+      { oo : SgOp G & { u : MonUnit G & Negate G}}
+      & @IsGroup G oun.1 oun.2.1 oun.2.2}
+      => (x.1.1 ; x.1.2.1 ; x.1.2.2 ; x.2))
+      ((op;unit;neg);ax) ((op';unit';neg');ax') _).
+    apply path_sigma_hprop; cbn.
+    srefine (path_sigma' _ _ _).
+    1: funext x y; apply eq.
+    rewrite transport_const.
+    pose (f := Build_GroupHomomorphism
+        (G:=Build_Group G op unit neg ax)
+        (H:=Build_Group G op' unit' neg' ax')
+        idmap eq).
+    srefine (path_sigma' _ _ _).
+    1: exact (grp_homo_unit f).
+    lhs nrapply transport_const.
+    funext x.
+    exact (grp_homo_inv f x).
 Defined.
 
 (** A version with nicer universe variables. *)

theories/Algebra/Groups/Subgroup.v

@@ -165,9 +165,9 @@ Coercion subgroup_group : Subgroup >-> Group.
 Definition subgroup_incl {G : Group} (H : Subgroup G)
   : subgroup_group H $-> G.
 Proof.
-  snrapply Build_GroupHomomorphism'.
+  snrapply Build_GroupHomomorphism.
   1: exact pr1.
-  repeat split.
+  hnf; reflexivity.
 Defined.
 
 Global Instance isembedding_subgroup_incl {G : Group} (H : Subgroup G)

theories/Algebra/Rings/Ring.v

@@ -176,7 +176,7 @@ Definition Build_RingHomomorphism' (A B : Ring) (map : GroupHomomorphism A B)
     (Aunit:=one) (Bunit:=one) map}
   : RingHomomorphism A B
   := Build_RingHomomorphism map
-      (Build_IsSemiRingPreserving _ (grp_homo_ishomo _ _ map) H).
+      (Build_IsSemiRingPreserving _ (ismonoidpreserving_grp_homo map) H).
 
 (** We can construct a ring isomorphism from a group isomorphism that preserves multiplication *)
 Definition Build_RingIsomorphism'' (A B : Ring) (e : GroupIsomorphism A B)