Kernel pairs of homomorphisms of group objects

For a homomorphism f : G ⟶ H from a group object to a monoid object, with kernel i : K ⟶ G, the square with upper map (k, g) ↦ i(k) * g and left map (k, g) ↦ g is cartesian. Thus the kernel pair of f is K × G, even when f is not an epimorphism. This is the geometric identity used to transfer properties of a kernel to a faithfully flat homomorphism of group schemes.

The kernel is specified by its pullback square over the identity, so the result also applies to an unbundled group object and a chosen model of its kernel. Neither commutativity nor a group structure on the chosen kernel or on the target is needed.

theorem TauCeti.isPullback_mul_of_isPullback_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {K G H : C} [CategoryTheory.GrpObj G] [CategoryTheory.MonObj H] (f : G ⟶ H) [CategoryTheory.IsMonHom f] (i : K ⟶ G) (h : CategoryTheory.IsPullback i (CategoryTheory.SemiCartesianMonoidalCategory.toUnit K) f CategoryTheory.MonObj.one) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst K G) i * CategoryTheory.SemiCartesianMonoidalCategory.snd K G) (CategoryTheory.SemiCartesianMonoidalCategory.snd K G) f f

The kernel pair of a monoid homomorphism from a group object is the product of its kernel with its source, with the two projections given by multiplication and the second projection.