Mon_ (C ⥤ D) ≌ C ⥤ Mon_ D #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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_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_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) :
@[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_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_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_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) :
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 := F ⋙ Mon_.forget D, 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
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C ⥤ Mon_ D) :
@[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_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) :
@[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) :
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.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) :
@[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] :
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 C D = {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_inverse
(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_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_functor
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D] :
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence.functor_map_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
(A B : CommMon_ (C ⥤ D))
(f : A ⟶ B)
(X : C) :
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence.functor_obj_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
(A : CommMon_ (C ⥤ D))
{X Y : C}
(ᾰ : X ⟶ Y) :
def
category_theory.monoidal.CommMon_functor_category_equivalence.functor
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
Functor translating a commutative monoid object in a functor category to a functor into the category of commutative monoid objects.
Equations
- category_theory.monoidal.CommMon_functor_category_equivalence.functor = {obj := λ (A : CommMon_ (C ⥤ D)), {obj := λ (X : C), {to_Mon_ := {X := (((category_theory.monoidal.Mon_functor_category_equivalence C D).functor.obj A.to_Mon_).obj X).X, one := (((category_theory.monoidal.Mon_functor_category_equivalence C D).functor.obj A.to_Mon_).obj X).one, mul := (((category_theory.monoidal.Mon_functor_category_equivalence C D).functor.obj A.to_Mon_).obj X).mul, one_mul' := _, mul_one' := _, mul_assoc' := _}, mul_comm' := _}, map := ((category_theory.monoidal.Mon_functor_category_equivalence C D).functor.obj A.to_Mon_).map, map_id' := _, map_comp' := _}, map := λ (A B : CommMon_ (C ⥤ D)) (f : A ⟶ B), {app := λ (X : C), ((category_theory.monoidal.Mon_functor_category_equivalence C D).functor.map f).app X, naturality' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence.functor_obj_obj_to_Mon_
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
(A : CommMon_ (C ⥤ D))
(X : C) :
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence.inverse_obj_to_Mon_
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
(F : C ⥤ CommMon_ D) :
def
category_theory.monoidal.CommMon_functor_category_equivalence.inverse
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
Functor translating a functor into the category of commutative monoid objects to a commutative monoid object in the functor category
Equations
- category_theory.monoidal.CommMon_functor_category_equivalence.inverse = {obj := λ (F : C ⥤ CommMon_ D), {to_Mon_ := {X := ((category_theory.monoidal.Mon_functor_category_equivalence C D).inverse.obj (F ⋙ CommMon_.forget₂_Mon_ D)).X, one := ((category_theory.monoidal.Mon_functor_category_equivalence C D).inverse.obj (F ⋙ CommMon_.forget₂_Mon_ D)).one, mul := ((category_theory.monoidal.Mon_functor_category_equivalence C D).inverse.obj (F ⋙ CommMon_.forget₂_Mon_ D)).mul, one_mul' := _, mul_one' := _, mul_assoc' := _}, mul_comm' := _}, map := λ (F G : C ⥤ CommMon_ D) (α : F ⟶ G), (category_theory.monoidal.Mon_functor_category_equivalence C D).inverse.map (category_theory.whisker_right α (CommMon_.forget₂_Mon_ D)), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence.inverse_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
(F G : C ⥤ CommMon_ D)
(α : F ⟶ G) :
@[simp]
theorem
category_theory.monoidal.CommMon_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]
[category_theory.braided_category D]
(X : CommMon_ (C ⥤ D))
(_x : C) :
@[simp]
theorem
category_theory.monoidal.CommMon_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]
[category_theory.braided_category D]
(X : CommMon_ (C ⥤ D))
(_x : C) :
def
category_theory.monoidal.CommMon_functor_category_equivalence.unit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
The unit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.
Equations
- category_theory.monoidal.CommMon_functor_category_equivalence.unit_iso = category_theory.nat_iso.of_components (λ (A : CommMon_ (C ⥤ D)), {hom := {hom := {app := λ (_x : C), 𝟙 (((𝟭 (CommMon_ (C ⥤ D))).obj A).to_Mon_.X.obj _x), naturality' := _}, one_hom' := _, mul_hom' := _}, inv := {hom := {app := λ (_x : C), 𝟙 (((category_theory.monoidal.CommMon_functor_category_equivalence.functor ⋙ category_theory.monoidal.CommMon_functor_category_equivalence.inverse).obj A).to_Mon_.X.obj _x), naturality' := _}, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) category_theory.monoidal.CommMon_functor_category_equivalence.unit_iso._proof_9
def
category_theory.monoidal.CommMon_functor_category_equivalence.counit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
The counit for the equivalence CommMon_ (C ⥤ D) ≌ C ⥤ CommMon_ D.
Equations
- category_theory.monoidal.CommMon_functor_category_equivalence.counit_iso = category_theory.nat_iso.of_components (λ (A : C ⥤ CommMon_ D), category_theory.nat_iso.of_components (λ (X : C), {hom := {hom := 𝟙 (((category_theory.monoidal.CommMon_functor_category_equivalence.inverse ⋙ category_theory.monoidal.CommMon_functor_category_equivalence.functor).obj A).obj X).to_Mon_.X, one_hom' := _, mul_hom' := _}, inv := {hom := 𝟙 (((𝟭 (C ⥤ CommMon_ D)).obj A).obj X).to_Mon_.X, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) _) category_theory.monoidal.CommMon_functor_category_equivalence.counit_iso._proof_8
@[simp]
theorem
category_theory.monoidal.CommMon_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]
[category_theory.braided_category D]
(X : C ⥤ CommMon_ D)
(X_1 : C) :
@[simp]
theorem
category_theory.monoidal.CommMon_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]
[category_theory.braided_category D]
(X : C ⥤ CommMon_ D)
(X_1 : C) :
def
category_theory.monoidal.CommMon_functor_category_equivalence
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category 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
- category_theory.monoidal.CommMon_functor_category_equivalence C D = {functor := category_theory.monoidal.CommMon_functor_category_equivalence.functor _inst_4, inverse := category_theory.monoidal.CommMon_functor_category_equivalence.inverse _inst_4, unit_iso := category_theory.monoidal.CommMon_functor_category_equivalence.unit_iso _inst_4, counit_iso := category_theory.monoidal.CommMon_functor_category_equivalence.counit_iso _inst_4, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence_functor
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence_inverse
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence_counit_iso
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
@[simp]
theorem
category_theory.monoidal.CommMon_functor_category_equivalence_unit_iso
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :