Shrinking a functor to MonCat

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

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

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

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

Equations

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

@[simp]

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

@[simp]

theorem MonCat.shrinkFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C MonCat) [∀ (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)

noncomputable def MonCat.shrinkFunctorMap {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C MonCat} (τ : 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 MonCat.shrinkFunctor.{w} F ⟶ MonCat.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 MonCat.shrinkFunctorMap_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C MonCat} (τ : 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)