Enriched categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We set up the basic theory of V-enriched categories,
for V an arbitrary monoidal category.
We do not assume here that V is a concrete category,
so there does not need to be a "honest" underlying category!
Use X ⟶[V] Y to obtain the V object of morphisms from X to Y.
This file contains the definitions of V-enriched categories and
V-functors.
We don't yet define the V-object of natural transformations
between a pair of V-functors (this requires limits in V),
but we do provide a presheaf isomorphic to the Yoneda embedding of this object.
We verify that when V = Type v, all these notion reduce to the usual ones.
@[class]
structure
category_theory.enriched_category
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
(C : Type u₁) :
Type (max u₁ v w)
- hom : C → C → V
- id : Π (X : C), 𝟙_ V ⟶ category_theory.enriched_category.hom X X
- comp : Π (X Y Z : C), category_theory.enriched_category.hom X Y ⊗ category_theory.enriched_category.hom Y Z ⟶ category_theory.enriched_category.hom X Z
- id_comp : (∀ (X Y : C), (λ_ (category_theory.enriched_category.hom X Y)).inv ≫ (category_theory.enriched_category.id X ⊗ 𝟙 (category_theory.enriched_category.hom X Y)) ≫ category_theory.enriched_category.comp X X Y = 𝟙 (category_theory.enriched_category.hom X Y)) . "obviously"
- comp_id : (∀ (X Y : C), (ρ_ (category_theory.enriched_category.hom X Y)).inv ≫ (𝟙 (category_theory.enriched_category.hom X Y) ⊗ category_theory.enriched_category.id Y) ≫ category_theory.enriched_category.comp X Y Y = 𝟙 (category_theory.enriched_category.hom X Y)) . "obviously"
- assoc : (∀ (W X Y Z : C), (α_ (category_theory.enriched_category.hom W X) (category_theory.enriched_category.hom X Y) (category_theory.enriched_category.hom Y Z)).inv ≫ (category_theory.enriched_category.comp W X Y ⊗ 𝟙 (category_theory.enriched_category.hom Y Z)) ≫ category_theory.enriched_category.comp W Y Z = (𝟙 (category_theory.enriched_category.hom W X) ⊗ category_theory.enriched_category.comp X Y Z) ≫ category_theory.enriched_category.comp W X Z) . "obviously"
A V-category is a category enriched in a monoidal category V.
Note that we do not assume that V is a concrete category,
so there may not be an "honest" underlying category at all!
Instances of this typeclass
Instances of other typeclasses for category_theory.enriched_category
- category_theory.enriched_category.has_sizeof_inst
def
category_theory.e_id
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(X : C) :
The 𝟙_ V-shaped generalized element giving the identity in a V-enriched category.
Equations
def
category_theory.e_comp
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(X Y Z : C) :
The composition V-morphism for a V-enriched category.
Equations
- category_theory.e_comp V X Y Z = category_theory.enriched_category.comp X Y Z
@[simp]
theorem
category_theory.e_id_comp
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(X Y : C) :
(λ_ (category_theory.enriched_category.hom X Y)).inv ≫ (category_theory.e_id V X ⊗ 𝟙 (category_theory.enriched_category.hom X Y)) ≫ category_theory.e_comp V X X Y = 𝟙 (category_theory.enriched_category.hom X Y)
@[simp]
theorem
category_theory.e_id_comp_assoc
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(X Y : C)
{X' : V}
(f' : category_theory.enriched_category.hom X Y ⟶ X') :
(λ_ (category_theory.enriched_category.hom X Y)).inv ≫ (category_theory.e_id V X ⊗ 𝟙 (category_theory.enriched_category.hom X Y)) ≫ category_theory.e_comp V X X Y ≫ f' = f'
@[simp]
theorem
category_theory.e_comp_id
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(X Y : C) :
(ρ_ (category_theory.enriched_category.hom X Y)).inv ≫ (𝟙 (category_theory.enriched_category.hom X Y) ⊗ category_theory.e_id V Y) ≫ category_theory.e_comp V X Y Y = 𝟙 (category_theory.enriched_category.hom X Y)
@[simp]
theorem
category_theory.e_comp_id_assoc
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(X Y : C)
{X' : V}
(f' : category_theory.enriched_category.hom X Y ⟶ X') :
(ρ_ (category_theory.enriched_category.hom X Y)).inv ≫ (𝟙 (category_theory.enriched_category.hom X Y) ⊗ category_theory.e_id V Y) ≫ category_theory.e_comp V X Y Y ≫ f' = f'
@[simp]
theorem
category_theory.e_assoc_assoc
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(W X Y Z : C)
{X' : V}
(f' : category_theory.enriched_category.hom W Z ⟶ X') :
(α_ (category_theory.enriched_category.hom W X) (category_theory.enriched_category.hom X Y) (category_theory.enriched_category.hom Y Z)).inv ≫ (category_theory.e_comp V W X Y ⊗ 𝟙 (category_theory.enriched_category.hom Y Z)) ≫ category_theory.e_comp V W Y Z ≫ f' = (𝟙 (category_theory.enriched_category.hom W X) ⊗ category_theory.e_comp V X Y Z) ≫ category_theory.e_comp V W X Z ≫ f'
@[simp]
theorem
category_theory.e_assoc
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
(W X Y Z : C) :
(α_ (category_theory.enriched_category.hom W X) (category_theory.enriched_category.hom X Y) (category_theory.enriched_category.hom Y Z)).inv ≫ (category_theory.e_comp V W X Y ⊗ 𝟙 (category_theory.enriched_category.hom Y Z)) ≫ category_theory.e_comp V W Y Z = (𝟙 (category_theory.enriched_category.hom W X) ⊗ category_theory.e_comp V X Y Z) ≫ category_theory.e_comp V W X Z
@[nolint]
def
category_theory.transport_enrichment
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{W : Type v}
[category_theory.category W]
[category_theory.monoidal_category W]
(F : category_theory.lax_monoidal_functor V W)
(C : Type u₁) :
Type u₁
A type synonym for C, which should come equipped with a V-enriched category structure.
In a moment we will equip this with the W-enriched category structure
obtained by applying the functor F : lax_monoidal_functor V W to each hom object.
Equations
Instances for category_theory.transport_enrichment
@[protected, instance]
def
category_theory.transport_enrichment.enriched_category
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{W : Type v}
[category_theory.category W]
[category_theory.monoidal_category W]
(F : category_theory.lax_monoidal_functor V W) :
Equations
- category_theory.transport_enrichment.enriched_category F = {hom := λ (X Y : C), F.to_functor.obj (category_theory.enriched_category.hom X Y), id := λ (X : C), F.ε ≫ F.to_functor.map (category_theory.e_id V X), comp := λ (X Y Z : C), F.μ (category_theory.enriched_category.hom X Y) (category_theory.enriched_category.hom Y Z) ≫ F.to_functor.map (category_theory.e_comp V X Y Z), id_comp := _, comp_id := _, assoc := _}
def
category_theory.category_of_enriched_category_Type
(C : Type u₁)
[𝒞 : category_theory.enriched_category (Type v) C] :
Construct an honest category from a Type v-enriched category.
Equations
- category_theory.category_of_enriched_category_Type C = {to_category_struct := {to_quiver := {hom := category_theory.enriched_category.hom 𝒞}, id := λ (X : C), category_theory.e_id (Type v) X punit.star, comp := λ (X Y Z : C) (f : X ⟶ Y) (g : Y ⟶ Z), category_theory.e_comp (Type v) X Y Z (f, g)}, id_comp' := _, comp_id' := _, assoc' := _}
def
category_theory.enriched_category_Type_of_category
(C : Type u₁)
[𝒞 : category_theory.category C] :
Construct a Type v-enriched category from an honest category.
We verify that an enriched category in Type u is just the same thing as an honest category.
Equations
- category_theory.enriched_category_Type_equiv_category C = {to_fun := λ (𝒞 : category_theory.enriched_category (Type v) C), category_theory.category_of_enriched_category_Type C, inv_fun := λ (𝒞 : category_theory.category C), category_theory.enriched_category_Type_of_category C, left_inv := _, right_inv := _}
@[nolint]
def
category_theory.forget_enrichment
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
(C : Type u₁)
[category_theory.enriched_category W C] :
Type u₁
A type synonym for C, which should come equipped with a V-enriched category structure.
In a moment we will equip this with the (honest) category structure
so that X ⟶ Y is (𝟙_ W) ⟶ (X ⟶[W] Y).
We obtain this category by
transporting the enrichment in V along the lax monoidal functor coyoneda_tensor_unit,
then using the equivalence of Type-enriched categories with honest categories.
This is sometimes called the "underlying" category of an enriched category,
although some care is needed as the functor coyoneda_tensor_unit,
which always exists, does not necessarily coincide with
"the forgetful functor" from V to Type, if such exists.
When V is any of Type, Top, AddCommGroup, or Module R,
coyoneda_tensor_unit is just the usual forgetful functor, however.
For V = Algebra R, the usual forgetful functor is coyoneda of R[X], not of R.
(Perhaps we should have a typeclass for this situation: concrete_monoidal?)
Equations
Instances for category_theory.forget_enrichment
def
category_theory.forget_enrichment.of
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
(X : C) :
Typecheck an object of C as an object of forget_enrichment W C.
Equations
def
category_theory.forget_enrichment.to
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
(X : category_theory.forget_enrichment W C) :
C
Typecheck an object of forget_enrichment W C as an object of C.
Equations
@[simp]
theorem
category_theory.forget_enrichment.to_of
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
(X : C) :
@[simp]
theorem
category_theory.forget_enrichment.of_to
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
(X : category_theory.forget_enrichment W C) :
@[protected, instance]
def
category_theory.category_forget_enrichment
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C] :
def
category_theory.forget_enrichment.hom_of
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
{X Y : C}
(f : 𝟙_ W ⟶ category_theory.enriched_category.hom X Y) :
Typecheck a (𝟙_ W)-shaped W-morphism as a morphism in forget_enrichment W C.
Equations
def
category_theory.forget_enrichment.hom_to
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
{X Y : category_theory.forget_enrichment W C}
(f : X ⟶ Y) :
Typecheck a morphism in forget_enrichment W C as a (𝟙_ W)-shaped W-morphism.
Equations
@[simp]
theorem
category_theory.forget_enrichment.hom_to_hom_of
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
{X Y : C}
(f : 𝟙_ W ⟶ category_theory.enriched_category.hom X Y) :
@[simp]
theorem
category_theory.forget_enrichment.hom_of_hom_to
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
{X Y : category_theory.forget_enrichment W C}
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.forget_enrichment_id
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
(X : category_theory.forget_enrichment W C) :
The identity in the "underlying" category of an enriched category.
@[simp]
theorem
category_theory.forget_enrichment_id'
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
(X : C) :
@[simp]
theorem
category_theory.forget_enrichment_comp
{C : Type u₁}
(W : Type (v+1))
[category_theory.category W]
[category_theory.monoidal_category W]
[category_theory.enriched_category W C]
{X Y Z : category_theory.forget_enrichment W C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
category_theory.forget_enrichment.hom_to W (f ≫ g) = ((λ_ (𝟙_ W)).inv ≫ (category_theory.forget_enrichment.hom_to W f ⊗ category_theory.forget_enrichment.hom_to W g)) ≫ category_theory.e_comp W (category_theory.forget_enrichment.to W X) (category_theory.forget_enrichment.to W Y) (category_theory.forget_enrichment.to W Z)
Composition in the "underlying" category of an enriched category.
structure
category_theory.enriched_functor
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
(C : Type u₁)
[category_theory.enriched_category V C]
(D : Type u₂)
[category_theory.enriched_category V D] :
Type (max u₁ u₂ w)
- obj : C → D
- map : Π (X Y : C), category_theory.enriched_category.hom X Y ⟶ category_theory.enriched_category.hom (self.obj X) (self.obj Y)
- map_id' : (∀ (X : C), category_theory.e_id V X ≫ self.map X X = category_theory.e_id V (self.obj X)) . "obviously"
- map_comp' : (∀ (X Y Z : C), category_theory.e_comp V X Y Z ≫ self.map X Z = (self.map X Y ⊗ self.map Y Z) ≫ category_theory.e_comp V (self.obj X) (self.obj Y) (self.obj Z)) . "obviously"
A V-functor F between V-enriched categories
has a V-morphism from X ⟶[V] Y to F.obj X ⟶[V] F.obj Y,
satisfying the usual axioms.
Instances for category_theory.enriched_functor
- category_theory.enriched_functor.has_sizeof_inst
- category_theory.enriched_functor.inhabited
@[simp]
theorem
category_theory.enriched_functor.map_id
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
(self : category_theory.enriched_functor V C D)
(X : C) :
category_theory.e_id V X ≫ self.map X X = category_theory.e_id V (self.obj X)
@[simp]
theorem
category_theory.enriched_functor.map_comp
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
(self : category_theory.enriched_functor V C D)
(X Y Z : C) :
@[simp]
theorem
category_theory.enriched_functor.map_id_assoc
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
(self : category_theory.enriched_functor V C D)
(X : C)
{X' : V}
(f' : category_theory.enriched_category.hom (self.obj X) (self.obj X) ⟶ X') :
category_theory.e_id V X ≫ self.map X X ≫ f' = category_theory.e_id V (self.obj X) ≫ f'
@[simp]
theorem
category_theory.enriched_functor.map_comp_assoc
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
(self : category_theory.enriched_functor V C D)
(X Y Z : C)
{X' : V}
(f' : category_theory.enriched_category.hom (self.obj X) (self.obj Z) ⟶ X') :
@[simp]
theorem
category_theory.enriched_functor.id_obj
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
(C : Type u₁)
[category_theory.enriched_category V C]
(X : C) :
(category_theory.enriched_functor.id V C).obj X = X
def
category_theory.enriched_functor.id
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
(C : Type u₁)
[category_theory.enriched_category V C] :
The identity enriched functor.
Equations
- category_theory.enriched_functor.id V C = {obj := λ (X : C), X, map := λ (X Y : C), 𝟙 (category_theory.enriched_category.hom X Y), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.enriched_functor.id_map
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
(C : Type u₁)
[category_theory.enriched_category V C]
(X Y : C) :
(category_theory.enriched_functor.id V C).map X Y = 𝟙 (category_theory.enriched_category.hom X Y)
@[protected, instance]
def
category_theory.enriched_functor.inhabited
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C] :
Equations
def
category_theory.enriched_functor.comp
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.enriched_category V C]
[category_theory.enriched_category V D]
[category_theory.enriched_category V E]
(F : category_theory.enriched_functor V C D)
(G : category_theory.enriched_functor V D E) :
Composition of enriched functors.
@[simp]
theorem
category_theory.enriched_functor.comp_obj
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.enriched_category V C]
[category_theory.enriched_category V D]
[category_theory.enriched_category V E]
(F : category_theory.enriched_functor V C D)
(G : category_theory.enriched_functor V D E)
(X : C) :
(category_theory.enriched_functor.comp V F G).obj X = G.obj (F.obj X)
@[simp]
theorem
category_theory.enriched_functor.comp_map
(V : Type v)
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
{D : Type u₂}
{E : Type u₃}
[category_theory.enriched_category V C]
[category_theory.enriched_category V D]
[category_theory.enriched_category V E]
(F : category_theory.enriched_functor V C D)
(G : category_theory.enriched_functor V D E)
(X Y : C) :
def
category_theory.enriched_functor.forget
{W : Type (v+1)}
[category_theory.category W]
[category_theory.monoidal_category W]
{C : Type u₁}
{D : Type u₂}
[category_theory.enriched_category W C]
[category_theory.enriched_category W D]
(F : category_theory.enriched_functor W C D) :
An enriched functor induces an honest functor of the underlying categories,
by mapping the (𝟙_ W)-shaped morphisms.
Equations
- F.forget = {obj := λ (X : category_theory.forget_enrichment W C), category_theory.forget_enrichment.of W (F.obj (category_theory.forget_enrichment.to W X)), map := λ (X Y : category_theory.forget_enrichment W C) (f : X ⟶ Y), category_theory.forget_enrichment.hom_of W (category_theory.forget_enrichment.hom_to W f ≫ F.map (category_theory.forget_enrichment.to W X) (category_theory.forget_enrichment.to W Y)), map_id' := _, map_comp' := _}
We now turn to natural transformations between V-functors.
The mostly commonly encountered definition of an enriched natural transformation is a collection of morphisms
(𝟙_ W) ⟶ (F.obj X ⟶[V] G.obj X)
satisfying an appropriate analogue of the naturality square. (c.f. https://ncatlab.org/nlab/show/enriched+natural+transformation)
This is the same thing as a natural transformation F.forget ⟶ G.forget.
We formalize this as enriched_nat_trans F G, which is a Type.
However, there's also something much nicer: with appropriate additional hypotheses,
there is a V-object enriched_nat_trans_obj F G which contains more information,
and from which one can recover enriched_nat_trans F G ≃ (𝟙_ V) ⟶ enriched_nat_trans_obj F G.
Using these as the hom-objects, we can build a V-enriched category
with objects the V-functors.
For enriched_nat_trans_obj to exist, it suffices to have V braided and complete.
Before assuming V is complete, we assume it is braided and
define a presheaf enriched_nat_trans_yoneda F G
which is isomorphic to the Yoneda embedding of enriched_nat_trans_obj F G
whether or not that object actually exists.
This presheaf has components (enriched_nat_trans_yoneda F G).obj A
what we call the A-graded enriched natural transformations,
which are collections of morphisms
A ⟶ (F.obj X ⟶[V] G.obj X)
satisfying a similar analogue of the naturality square,
this time incorporating a half-braiding on A.
(We actually define enriched_nat_trans F G
as the special case A := 𝟙_ V with the trivial half-braiding,
and when defining enriched_nat_trans_yoneda F G we use the half-braidings
coming from the ambient braiding on V.)
theorem
category_theory.graded_nat_trans.ext_iff
{V : Type v}
{_inst_1 : category_theory.category V}
{_inst_2 : category_theory.monoidal_category V}
{C : Type u₁}
{_inst_3 : category_theory.enriched_category V C}
{D : Type u₂}
{_inst_4 : category_theory.enriched_category V D}
{A : category_theory.center V}
{F G : category_theory.enriched_functor V C D}
(x y : category_theory.graded_nat_trans A F G) :
theorem
category_theory.graded_nat_trans.ext
{V : Type v}
{_inst_1 : category_theory.category V}
{_inst_2 : category_theory.monoidal_category V}
{C : Type u₁}
{_inst_3 : category_theory.enriched_category V C}
{D : Type u₂}
{_inst_4 : category_theory.enriched_category V D}
{A : category_theory.center V}
{F G : category_theory.enriched_functor V C D}
(x y : category_theory.graded_nat_trans A F G)
(h : x.app = y.app) :
x = y
@[nolint, ext]
structure
category_theory.graded_nat_trans
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
(A : category_theory.center V)
(F G : category_theory.enriched_functor V C D) :
Type (max u₁ w)
- app : Π (X : C), A.fst ⟶ category_theory.enriched_category.hom (F.obj X) (G.obj X)
- naturality : ∀ (X Y : C), (A.snd.β (category_theory.enriched_category.hom X Y)).hom ≫ (F.map X Y ⊗ self.app Y) ≫ category_theory.e_comp V (F.obj X) (F.obj Y) (G.obj Y) = (self.app X ⊗ G.map X Y) ≫ category_theory.e_comp V (F.obj X) (G.obj X) (G.obj Y)
The type of A-graded natural transformations between V-functors F and G.
This is the type of morphisms in V from A to the V-object of natural transformations.
Instances for category_theory.graded_nat_trans
- category_theory.graded_nat_trans.has_sizeof_inst
@[simp]
theorem
category_theory.enriched_nat_trans_yoneda_map_app
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
[category_theory.braided_category V]
(F G : category_theory.enriched_functor V C D)
(A A' : Vᵒᵖ)
(f : A ⟶ A')
(σ : category_theory.graded_nat_trans ((category_theory.center.of_braided V).to_lax_monoidal_functor.to_functor.obj (opposite.unop A)) F G)
(X : C) :
@[simp]
theorem
category_theory.enriched_nat_trans_yoneda_obj
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
[category_theory.braided_category V]
(F G : category_theory.enriched_functor V C D)
(A : Vᵒᵖ) :
noncomputable
def
category_theory.enriched_nat_trans_yoneda
{V : Type v}
[category_theory.category V]
[category_theory.monoidal_category V]
{C : Type u₁}
[category_theory.enriched_category V C]
{D : Type u₂}
[category_theory.enriched_category V D]
[category_theory.braided_category V]
(F G : category_theory.enriched_functor V C D) :
A presheaf isomorphic to the Yoneda embedding of
the V-object of natural transformations from F to G.
Equations
- category_theory.enriched_nat_trans_yoneda F G = {obj := λ (A : Vᵒᵖ), category_theory.graded_nat_trans ((category_theory.center.of_braided V).to_lax_monoidal_functor.to_functor.obj (opposite.unop A)) F G, map := λ (A A' : Vᵒᵖ) (f : A ⟶ A') (σ : category_theory.graded_nat_trans ((category_theory.center.of_braided V).to_lax_monoidal_functor.to_functor.obj (opposite.unop A)) F G), {app := λ (X : C), f.unop ≫ σ.app X, naturality := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.enriched_functor_Type_equiv_functor_apply_map
{C : Type u₁}
[𝒞 : category_theory.enriched_category (Type v) C]
{D : Type u₂}
[𝒟 : category_theory.enriched_category (Type v) D]
(F : category_theory.enriched_functor (Type v) C D)
(X Y : C)
(f : X ⟶ Y) :
(⇑category_theory.enriched_functor_Type_equiv_functor F).map f = F.map X Y f
@[simp]
theorem
category_theory.enriched_functor_Type_equiv_functor_apply_obj
{C : Type u₁}
[𝒞 : category_theory.enriched_category (Type v) C]
{D : Type u₂}
[𝒟 : category_theory.enriched_category (Type v) D]
(F : category_theory.enriched_functor (Type v) C D)
(X : C) :
@[simp]
theorem
category_theory.enriched_functor_Type_equiv_functor_symm_apply_obj
{C : Type u₁}
[𝒞 : category_theory.enriched_category (Type v) C]
{D : Type u₂}
[𝒟 : category_theory.enriched_category (Type v) D]
(F : C ⥤ D)
(X : C) :
def
category_theory.enriched_functor_Type_equiv_functor
{C : Type u₁}
[𝒞 : category_theory.enriched_category (Type v) C]
{D : Type u₂}
[𝒟 : category_theory.enriched_category (Type v) D] :
category_theory.enriched_functor (Type v) C D ≃ C ⥤ D
We verify that an enriched functor between Type v enriched categories
is just the same thing as an honest functor.
Equations
- category_theory.enriched_functor_Type_equiv_functor = {to_fun := λ (F : category_theory.enriched_functor (Type v) C D), {obj := λ (X : C), F.obj X, map := λ (X Y : C) (f : X ⟶ Y), F.map X Y f, map_id' := _, map_comp' := _}, inv_fun := λ (F : C ⥤ D), {obj := λ (X : C), F.obj X, map := λ (X Y : C) (f : category_theory.enriched_category.hom X Y), F.map f, map_id' := _, map_comp' := _}, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.enriched_functor_Type_equiv_functor_symm_apply_map
{C : Type u₁}
[𝒞 : category_theory.enriched_category (Type v) C]
{D : Type u₂}
[𝒟 : category_theory.enriched_category (Type v) D]
(F : C ⥤ D)
(X Y : C)
(f : category_theory.enriched_category.hom X Y) :
noncomputable
def
category_theory.enriched_nat_trans_yoneda_Type_iso_yoneda_nat_trans
{C : Type v}
[category_theory.enriched_category (Type v) C]
{D : Type v}
[category_theory.enriched_category (Type v) D]
(F G : category_theory.enriched_functor (Type v) C D) :
We verify that the presheaf representing natural transformations
between Type v-enriched functors is actually represented by
the usual type of natural transformations!
Equations
- category_theory.enriched_nat_trans_yoneda_Type_iso_yoneda_nat_trans F G = category_theory.nat_iso.of_components (λ (α : (Type v)ᵒᵖ), {hom := λ (σ : (category_theory.enriched_nat_trans_yoneda F G).obj α) (x : opposite.unop α), {app := λ (X : C), σ.app X x, naturality' := _}, inv := λ (σ : (category_theory.yoneda.obj (⇑category_theory.enriched_functor_Type_equiv_functor F ⟶ ⇑category_theory.enriched_functor_Type_equiv_functor G)).obj α), {app := λ (X : C) (x : ((category_theory.center.of_braided (Type v)).to_lax_monoidal_functor.to_functor.obj (opposite.unop α)).fst), (σ x).app X, naturality := _}, hom_inv_id' := _, inv_hom_id' := _}) _