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.
def
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Mon_Class A]
(X : C)
:
Mon_ D
A monoid object in a functor category sends any object to a monoid object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_one
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Mon_Class A]
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_X
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Mon_Class A]
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Mon_Class A]
(X : C)
:
def
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Mon_Class A]
:
A monoid object in a functor category induces a functor to the category of monoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Mon_Class A]
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Mon_Class A]
(X : C)
:
def
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
Functor translating a monoid object in a functor category to a functor into the category of monoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{X✝ Y✝ : Mon_ (Functor C D)}
(f : X✝ ⟶ Y✝)
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Mon_ (Functor C D))
:
def
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Mon_ D))
:
A functor to the category of monoid objects can be translated as a monoid object in the functor category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Mon_ D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Mon_ D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_X
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Mon_ D))
:
def
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
Functor translating a functor into the category of monoid objects to a monoid object in the functor category
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Mon_ D))
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{X✝ Y✝ : Functor C (Mon_ D)}
(α : X✝ ⟶ Y✝)
(X : C)
:
def
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
The unit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(X : Mon_ (Functor C D))
(x✝ : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(X : Mon_ (Functor C D))
(x✝ : C)
:
def
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
The counit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(X : Functor C (Mon_ D))
(X✝ : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(X : Functor C (Mon_ D))
(X✝ : C)
:
def
CategoryTheory.Monoidal.monFunctorCategoryEquivalence
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_functor
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
@[simp]
theorem
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_inverse
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
@[simp]
theorem
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_unitIso
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
@[simp]
theorem
CategoryTheory.Monoidal.monFunctorCategoryEquivalence_counitIso
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
def
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Comon_Class A]
(X : C)
:
Comon_ D
A comonoid object in a functor category sends any object to a comonoid object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_comul
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Comon_Class A]
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_X
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Comon_Class A]
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_counit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Comon_Class A]
(X : C)
:
def
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Comon_Class A]
:
A comonoid object in a functor category induces a functor to the category of comonoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Comon_Class A]
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Functor C D)
[Comon_Class A]
(X : C)
:
def
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
Functor translating a comonoid object in a functor category to a functor into the category of comonoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(A : Comon_ (Functor C D))
:
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
{X✝ Y✝ : Comon_ (Functor C D)}
(f : X✝ ⟶ Y✝)
(X : C)
:
def
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Comon_ D))
:
A functor to the category of comonoid objects can be translated as a comonoid object in the functor category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_X
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Comon_ D))
:
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Comon_ D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(F : Functor C (Comon_ D))
(X : C)
:
def
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
The counit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(X : Functor C (Comon_ D))
(X✝ : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
(X : Functor C (Comon_ D))
(X✝ : C)
:
def
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
When D is a monoidal category,
comonoid objects in C ⥤ D are the same thing
as functors from C into the comonoid objects of D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
theorem
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_functor
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
@[simp]
theorem
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_counitIso
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
:
@[simp]
def
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
Functor translating a commutative monoid object in a functor category to a functor into the category of commutative monoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_X
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(A : CommMon_ (Functor C D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
{X✝ Y✝ : CommMon_ (Functor C D)}
(f : X✝ ⟶ Y✝)
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(A : CommMon_ (Functor C D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(A : CommMon_ (Functor C D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(A : CommMon_ (Functor C D))
{X Y : C}
(a✝ : X ⟶ Y)
:
def
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
Functor translating a functor into the category of commutative monoid objects to a commutative monoid object in the functor category
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(F : Functor C (CommMon_ D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
{X✝ Y✝ : Functor C (CommMon_ D)}
(α : X✝ ⟶ Y✝)
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(F : Functor C (CommMon_ D))
(X : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(F : Functor C (CommMon_ D))
{X✝ Y✝ : C}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(F : Functor C (CommMon_ D))
(X : C)
:
def
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
The unit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(X : CommMon_ (Functor C D))
(x✝ : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(X : CommMon_ (Functor C D))
(x✝ : C)
:
def
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
The counit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(X : Functor C (CommMon_ D))
(X✝ : C)
:
@[simp]
theorem
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
(X : Functor C (CommMon_ D))
(X✝ : C)
:
def
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_functor
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
@[simp]
theorem
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_unitIso
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
@[simp]
theorem
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_inverse
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
:
@[simp]
theorem
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_counitIso
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
[MonoidalCategory D]
[BraidedCategory D]
: