Shrinking a functor to GrpCat

For a functor C ⥤ GrpCat.{w'} with w-small image, we shrink to a functor C ⥤ GrpCat.{w}.

instance instSmallCompGrpCatForgetMonoidHomCarrierOfSmallObj {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat) [∀ (X : C), Small.{w, w'} ↑(F.obj X)] : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} (F.comp (CategoryTheory.forget GrpCat))

noncomputable def GrpCat.shrinkFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat) [∀ (X : C), Small.{w, w'} ↑(F.obj X)] : CategoryTheory.Functor C GrpCat

A functor F : C ⥤ GrpCat.{w'} factors through GrpCat.{w} if all the monoids are w-small.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GrpCat.shrinkFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat) [∀ (X : C), Small.{w, w'} ↑(F.obj X)] {X Y : C} (f : X ⟶ Y) : (shrinkFunctor.{w, w', v, u} F).map f = ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (F.map f))).comp Shrink.mulEquiv.toMonoidHom)

@[simp]

theorem GrpCat.shrinkFunctor_obj_coe {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat) [∀ (X : C), Small.{w, w'} ↑(F.obj X)] (X : C) : ↑((shrinkFunctor.{w, w', v, u} F).obj X) = Shrink.{w, w'} ↑(F.obj X)

noncomputable def GrpCat.shrinkFunctorMap {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C GrpCat} (τ : F ⟶ G) [∀ (X : C), Small.{w, w'} ↑(F.obj X)] [∀ (X : C), Small.{w, w'} ↑(G.obj X)] : shrinkFunctor.{w, w', v, u} F ⟶ shrinkFunctor.{w, w', v, u} G

The natural transformation GrpCat.shrinkFunctor.{w} F ⟶ GrpCat.shrinkFunctor.{w} G induces by a natural transformation τ : F ⟶ G between w-small functors to monoids.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GrpCat.shrinkFunctorMap_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C GrpCat} (τ : F ⟶ G) [∀ (X : C), Small.{w, w'} ↑(F.obj X)] [∀ (X : C), Small.{w, w'} ↑(G.obj X)] (X : C) : (shrinkFunctorMap τ).app X = ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom)