proposition: Lemma isembedding_grouphomomorphism {A B : Group} (f : A $-> B) : (forall a, f a = group_unit -> a = group_unit) <-> IsEmbedding f.
proof: Proof. split. - intros h b. apply hprop_allpath. intros [a0 p0] [a1 p1]. srapply path_sigma_hprop; simpl. apply grp_moveL_1M. apply h. rewrite grp_homo_op, grp_homo_inv. rewrite p0, p1. apply right_inverse. - intros E a p. rapply (isinj_embedding f). exact (p @ (grp_homo_unit f)^). Defined.
imports: Basics Types HProp HFiber HSet PathAny (notations) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.abstract_algebra (hints) Classes.interfaces.canonical_names Classes.interfaces.canonical_names (SgOp, sg_op, One, one, MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity, Negate, negate, Associative, simple_associativity, associativity, LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity) Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, negate_l, negate_r, IsSemiGroup(..), sg_set, sg_ass, IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup, IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor, IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit) Classes.theory.groups Pointed.Core WildCat Spaces.Nat.Core Truncations.Core