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:
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
category_theory.monoidal.Mon_functor_category_equivalence.functor_obj_obj_X
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(A : Mon_ (C ⥤ D))
(X : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.functor_map_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(A B : Mon_ (C ⥤ D))
(f : A ⟶ B)
(X : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.functor_obj_map_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(A : Mon_ (C ⥤ D))
(X Y : C)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.functor_obj_obj_one
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(A : Mon_ (C ⥤ D))
(X : C) :
def
category_theory.monoidal.Mon_functor_category_equivalence.functor
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
Functor translating a monoid object in a functor category to a functor into the category of monoid objects.
Equations
- category_theory.monoidal.Mon_functor_category_equivalence.functor = {obj := λ (A : Mon_ (C ⥤ D)), {obj := λ (X : C), {X := A.X.obj X, one := A.one.app X, mul := A.mul.app X, one_mul' := _, mul_one' := _, mul_assoc' := _}, map := λ (X Y : C) (f : X ⟶ Y), {hom := A.X.map f, one_hom' := _, mul_hom' := _}, map_id' := _, map_comp' := _}, map := λ (A B : Mon_ (C ⥤ D)) (f : A ⟶ B), {app := λ (X : C), {hom := f.hom.app X, one_hom' := _, mul_hom' := _}, naturality' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.functor_obj_obj_mul
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(A : Mon_ (C ⥤ D))
(X : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.inverse_map_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F G : C ⥤ Mon_ D)
(α : F ⟶ G)
(X : C) :
def
category_theory.monoidal.Mon_functor_category_equivalence.inverse
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
Functor translating a functor into the category of monoid objects to a monoid object in the functor category
Equations
- category_theory.monoidal.Mon_functor_category_equivalence.inverse = {obj := λ (F : C ⥤ Mon_ D), {X := {obj := λ (X : C), (F.obj X).X, map := λ (X Y : C) (f : X ⟶ Y), (F.map f).hom, map_id' := _, map_comp' := _}, one := {app := λ (X : C), (F.obj X).one, naturality' := _}, mul := {app := λ (X : C), (F.obj X).mul, naturality' := _}, one_mul' := _, mul_one' := _, mul_assoc' := _}, map := λ (F G : C ⥤ Mon_ D) (α : F ⟶ G), {hom := {app := λ (X : C), (α.app X).hom, naturality' := _}, one_hom' := _, mul_hom' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.inverse_obj_X_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C ⥤ Mon_ D)
(X Y : C)
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.inverse_obj_one_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C ⥤ Mon_ D)
(X : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.inverse_obj_X_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C ⥤ Mon_ D)
(X : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.inverse_obj_mul_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C ⥤ Mon_ D)
(X : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.unit_iso_hom_app_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(X : Mon_ (C ⥤ D))
(_x : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.unit_iso_inv_app_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(X : Mon_ (C ⥤ D))
(_x : C) :
def
category_theory.monoidal.Mon_functor_category_equivalence.unit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
The unit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.
Equations
- category_theory.monoidal.Mon_functor_category_equivalence.unit_iso = category_theory.nat_iso.of_components (λ (A : Mon_ (C ⥤ D)), {hom := {hom := {app := λ (_x : C), 𝟙 (((𝟭 (Mon_ (C ⥤ D))).obj A).X.obj _x), naturality' := _}, one_hom' := _, mul_hom' := _}, inv := {hom := {app := λ (_x : C), 𝟙 (((category_theory.monoidal.Mon_functor_category_equivalence.functor ⋙ category_theory.monoidal.Mon_functor_category_equivalence.inverse).obj A).X.obj _x), naturality' := _}, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) category_theory.monoidal.Mon_functor_category_equivalence.unit_iso._proof_9
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.counit_iso_inv_app_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(X : C ⥤ Mon_ D)
(X_1 : C) :
def
category_theory.monoidal.Mon_functor_category_equivalence.counit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
The counit for the equivalence Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D.
Equations
- category_theory.monoidal.Mon_functor_category_equivalence.counit_iso = category_theory.nat_iso.of_components (λ (A : C ⥤ Mon_ D), category_theory.nat_iso.of_components (λ (X : C), {hom := {hom := 𝟙 (((category_theory.monoidal.Mon_functor_category_equivalence.inverse ⋙ category_theory.monoidal.Mon_functor_category_equivalence.functor).obj A).obj X).X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 (((𝟭 (C ⥤ Mon_ D)).obj A).obj X).X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) _) category_theory.monoidal.Mon_functor_category_equivalence.counit_iso._proof_8
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence.counit_iso_hom_app_app_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(X : C ⥤ Mon_ D)
(X_1 : C) :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence_counit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence_functor
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
def
category_theory.monoidal.Mon_functor_category_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category 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
- category_theory.monoidal.Mon_functor_category_equivalence = {functor := category_theory.monoidal.Mon_functor_category_equivalence.functor _inst_3, inverse := category_theory.monoidal.Mon_functor_category_equivalence.inverse _inst_3, unit_iso := category_theory.monoidal.Mon_functor_category_equivalence.unit_iso _inst_3, counit_iso := category_theory.monoidal.Mon_functor_category_equivalence.counit_iso _inst_3, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence_unit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :
@[simp]
theorem
category_theory.monoidal.Mon_functor_category_equivalence_inverse
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D] :