1 Category theory
1.1 Over category
If \(a : F \vdash G\) is an adjunction between \(F : C \to D\) and \(G : D \to C\) and \(X : C\), then there is an adjunction between \(F / X : C / X \to D / F(X)\) and \(G / X : D / F(X) \to C / X\).
See https://ncatlab.org/nlab/show/sliced+adjoint+functors+–+section.
Let \(J\) be a shape (i.e. a category). Let \(\widetilde J\) denote the category which is the same as \(J\), but has an extra object \(*\) which is terminal. If \(F : C \to D\) is a functor preserving limits of shape \(\widetilde J\), then the obvious functor \(C / X \to D / F(X)\) preserves limits of shape \(J\).
Extend a functor \(K\colon J \to C / X\) to a functor \(\widetilde K\colon \widetilde J \to C\), by letting \(\widetilde K (*) = X\).
If \(F : C \to D\) is a full functor between cartesian-monoidal categories, then \(F / X : C / X \hom D / F(X)\) has the same essential image as \(F\).
Transfer all diagrams.
1.2 Objects
1.2.1 Group objects
If a finite-products-preserving functor \(F : C \to D\) is fully faithful, then so is \(\operatorname{Grp}(F) : \operatorname{Grp}C \to \operatorname{Grp}D\).
Faithfulness is immediate.
For fullness, assume \(f : F(G) \to F(H)\) is a morphism. By fullness of \(F\), find \(g : G \to H\) such that \(F(g) = f\). \(g\) is a morphism because we can pull back each diagram from \(D\) to \(C\) along \(F\) which is faithful.
If \(e : C \backsimeq D\) is an equivalence of cartesian-monoidal categories, then \(\operatorname{Grp}(e) : \operatorname{Grp}(C) \backsimeq \operatorname{Grp}(D)\) too is an equivalence of categories.
Transfer all diagrams.
If \(F : C \to D\) is a fully faithful functor between cartesian-monoidal categories, then \(\operatorname{Grp}(F) : \operatorname{Grp}(C) \hom \operatorname{Grp}(D)\) has the same essential image as \(F\).
Transfer all diagrams.
If \(F : C \to D\) is a fully faithful functor between cartesian-monoidal categories and \(X, G \in C\) are an object and a group object respectively, then \(\operatorname{Grp}(F) : (X \hom G) \hom \backcong (F(X) \hom F(G))\) is a group isomorphism.
Toddlers and streets.
1.2.2 Module objects
Let \(M, N\) be two monoid objects in a monoidal category \(C\). Let \(f : M \to N\) be a monoid morphism. If \(X\) is a \(N\)-module object, then it is also a \(M\)-module object.
Define the multiplication \(\mu _M : M \otimes X \to X\) as \(f \otimes \mathbb 1 \gg \mu _N\). All proofs follow easily.