Monomorphisms of group objects

A morphism of group objects is a monomorphism whenever its underlying morphism is a monomorphism. The faithful forgetful functor reflects monomorphisms, so subobject constructions can use monicity in the ambient category.

@[instance 900]

instance CategoryTheory.Grp.mono_of_mono_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H : Grp C} (f : G ⟶ H) [Mono f.hom.hom] : Mono f

A morphism of group objects is monic if its underlying morphism is monic.