# Documentation

Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

# Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D#

When D is a monoidal category, monoid objects in C ⥤ D are the same thing as functors from C into the monoid objects of D.

This is formalised as:

• monFunctorCategoryEquivalence : Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D

The intended application is that as Ring ≌ Mon_ Ab (not yet constructed!), we have presheaf Ring X ≌ presheaf (Mon_ Ab) X ≌ Mon_ (presheaf Ab X), and we can model a module over a presheaf of rings as a module object in presheaf Ab X.

## Future work #

Presumably this statement is not specific to monoids, and could be generalised to any internal algebraic objects, if the appropriate framework was available.

@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Functor.obj_obj_mul {C : Type u₁} [] {D : Type u₂} [] (A : ) (X : C) :
= A.mul.app X
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Functor.obj_obj_X {C : Type u₁} [] {D : Type u₂} [] (A : ) (X : C) :
= A.X.obj X
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Functor.obj_obj_one {C : Type u₁} [] {D : Type u₂} [] (A : ) (X : C) :
= A.one.app X
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Functor.obj_map_hom {C : Type u₁} [] {D : Type u₂} [] (A : ) :
∀ {X Y : C} (f : X Y), = A.X.map f

A monoid object in a functor category induces a functor to the category of monoid objects.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom {C : Type u₁} [] {D : Type u₂} [] :
∀ {X Y : } (f : X Y) (X_1 : C), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj {C : Type u₁} [] {D : Type u₂} [] (A : ) :
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.obj A =

Functor translating a monoid object in a functor category to a functor into the category of monoid objects.

Instances For
@[simp]
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Inverse.obj_mul_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
= (F.obj X).mul
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Inverse.obj_one_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
= (F.obj X).one

A functor to the category of monoid objects can be translated as a monoid object in the functor category.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_obj {C : Type u₁} [] {D : Type u₂} [] (F : ) :
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.obj F =
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app {C : Type u₁} [] {D : Type u₂} [] :
∀ {X Y : } (α : X Y) (X_1 : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom

Functor translating a functor into the category of monoid objects to a monoid object in the functor category

Instances For
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app {C : Type u₁} [] {D : Type u₂} [] (X : ) :
∀ (x : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x = CategoryTheory.CategoryStruct.id (X.X.obj x)
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app {C : Type u₁} [] {D : Type u₂} [] (X : ) :
∀ (x : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x = CategoryTheory.CategoryStruct.id (X.X.obj x)
def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso {C : Type u₁} [] {D : Type u₂} [] :
CategoryTheory.Functor.comp CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse

The unit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom {C : Type u₁} [] {D : Type u₂} [] (X : ) (X : C) :
((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.hom.app X).app X).hom = CategoryTheory.CategoryStruct.id (X.obj X).X
@[simp]
theorem CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom {C : Type u₁} [] {D : Type u₂} [] (X : ) (X : C) :
((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.inv.app X).app X).hom = CategoryTheory.CategoryStruct.id (X.obj X).X
def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso {C : Type u₁} [] {D : Type u₂} [] :
CategoryTheory.Functor.comp CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor

The counit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_counitIso (C : Type u₁) [] (D : Type u₂) [] :
().counitIso = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso
@[simp]
theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_functor (C : Type u₁) [] (D : Type u₂) [] :
().functor = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor
@[simp]
theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_inverse (C : Type u₁) [] (D : Type u₂) [] :
().inverse = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse
@[simp]
theorem CategoryTheory.Monoidal.monFunctorCategoryEquivalence_unitIso (C : Type u₁) [] (D : Type u₂) [] :
().unitIso = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso

When D is a monoidal category, monoid objects in C ⥤ D are the same thing as functors from C into the monoid objects of D.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mul {C : Type u₁} [] {D : Type u₂} [] (A : ) (X : C) :
((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).mul = A.mul.app X
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom {C : Type u₁} [] {D : Type u₂} [] (A : ) :
∀ {X Y : C} (a : X Y), ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).map a).hom = A.X.map a
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_X {C : Type u₁} [] {D : Type u₂} [] (A : ) (X : C) :
((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).X = A.X.obj X
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_one {C : Type u₁} [] {D : Type u₂} [] (A : ) (X : C) :
((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).one = A.one.app X
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom {C : Type u₁} [] {D : Type u₂} [] :
∀ {X Y : } (f : X Y) (X_1 : C), ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1

Functor translating a commutative monoid object in a functor category to a functor into the category of commutative monoid objects.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map {C : Type u₁} [] {D : Type u₂} [] (F : ) :
∀ {X Y : C} (f : X Y), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.map f = (F.map f).hom
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mul_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
(CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).mul.app X = (F.obj X).mul
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_app {C : Type u₁} [] {D : Type u₂} [] :
∀ {X Y : } (α : X Y) (X_1 : C), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_obj {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
(CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.obj X = (().obj (F.obj X)).X
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_one_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
(CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).one.app X = (F.obj X).one

Functor translating a functor into the category of commutative monoid objects to a commutative monoid object in the functor category

Instances For
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_app {C : Type u₁} [] {D : Type u₂} [] (X : ) :
∀ (x : C), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x = CategoryTheory.CategoryStruct.id (().obj ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj X).obj x)).X
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_app {C : Type u₁} [] {D : Type u₂} [] (X : ) :
∀ (x : C), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x = CategoryTheory.CategoryStruct.id (X.X.obj x)
def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso {C : Type u₁} [] {D : Type u₂} [] :
CategoryTheory.Functor.comp CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse

The unit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom {C : Type u₁} [] {D : Type u₂} [] (X : ) (X : C) :
((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.hom.app X).app X).hom = CategoryTheory.CategoryStruct.id (().obj (X.obj X)).X
@[simp]
theorem CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom {C : Type u₁} [] {D : Type u₂} [] (X : ) (X : C) :
((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.inv.app X).app X).hom = CategoryTheory.CategoryStruct.id (X.obj X).X
def CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso {C : Type u₁} [] {D : Type u₂} [] :
CategoryTheory.Functor.comp CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor

The counit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.

Instances For
@[simp]
theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_counitIso (C : Type u₁) [] (D : Type u₂) [] :
().counitIso = CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso
@[simp]
theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_inverse (C : Type u₁) [] (D : Type u₂) [] :
= CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse
@[simp]
theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_unitIso (C : Type u₁) [] (D : Type u₂) [] :
= CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso
@[simp]
theorem CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_functor (C : Type u₁) [] (D : Type u₂) [] :
= CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor

When D is a braided monoidal category, commutative monoid objects in C ⥤ D are the same thing as functors from C into the commutative monoid objects of D.

Instances For