Monomorphisms of group objects over a base

A morphism of group objects in a slice category is a monomorphism whenever its underlying morphism in the original category is a monomorphism. This follows by reflecting monomorphisms through the two faithful forgetful functors. In particular, closed immersions of group schemes are monomorphisms without any affineness assumption.

@[instance 900]

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

A morphism of group objects over a base is monic if its underlying morphism is monic.