The Yoneda functor for locally small categories

Let C be a locally w-small category. We define the Yoneda embedding shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w. (See the file CategoryTheory.Yoneda for the other variants yoneda and uliftYoneda.)

@[reducible, inline]

abbrev CategoryTheory.FunctorToTypes.Small {C : Type u} [Category.{v, u} C] (F : Functor C (Type w')) : Prop

A functor to types F : C ⥤ Type w' is w-small if for any X : C, the type F.obj X is w-small.

noncomputable def CategoryTheory.FunctorToTypes.shrink {C : Type u} [Category.{v, u} C] (F : Functor C (Type w')) [FunctorToTypes.Small.{w, w', v, u} F] : Functor C (Type w)

If a functor F : C ⥤ Type w' is w-small, this is the functor C ⥤ Type w obtained by shrinking F.obj X for all X : C.

@[simp]

theorem CategoryTheory.FunctorToTypes.shrink_obj {C : Type u} [Category.{v, u} C] (F : Functor C (Type w')) [FunctorToTypes.Small.{w, w', v, u} F] (X : C) : (shrink.{w, w', v, u} F).obj X = Shrink.{w, w'} (F.obj X)

@[simp]

theorem CategoryTheory.FunctorToTypes.shrink_map {C : Type u} [Category.{v, u} C] (F : Functor C (Type w')) [FunctorToTypes.Small.{w, w', v, u} F] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (a✝ : Shrink.{w, w'} (F.obj X✝)) : (shrink.{w, w', v, u} F).map f a✝ = (⇑(equivShrink (F.obj Y✝)) ∘ F.map f ∘ ⇑(equivShrink (F.obj X✝)).symm) a✝

noncomputable def CategoryTheory.FunctorToTypes.shrinkMap {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w')} (τ : F ⟶ G) [FunctorToTypes.Small.{w, w', v, u} F] [FunctorToTypes.Small.{w, w', v, u} G] : shrink.{w, w', v, u} F ⟶ shrink.{w, w', v, u} G

The natural transformation shrink.{w} F ⟶ shrink.{w} G induces by a natural transformation τ : F ⟶ G between w-small functors to types.

@[simp]

theorem CategoryTheory.FunctorToTypes.shrinkMap_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w')} (τ : F ⟶ G) [FunctorToTypes.Small.{w, w', v, u} F] [FunctorToTypes.Small.{w, w', v, u} G] (X : C) (a✝ : (shrink.{w, w', v, u} F).obj X) : (shrinkMap τ).app X a✝ = (⇑(equivShrink (G.obj X)) ∘ τ.app X ∘ ⇑(equivShrink (F.obj X)).symm) a✝

instance CategoryTheory.instSmallOppositeObjFunctorTypeYoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) : FunctorToTypes.Small.{w, v, v, u} (yoneda.obj X)

noncomputable def CategoryTheory.shrinkYoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] : Functor C (Functor Cᵒᵖ (Type w))

The Yoneda embedding C ⥤ Cᵒᵖ ⥤ Type w for a locally w-small category C.

theorem CategoryTheory.shrinkYoneda_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : shrinkYoneda.{w, v, u}.map f = FunctorToTypes.shrinkMap (yoneda.map f)

theorem CategoryTheory.shrinkYoneda_obj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) : shrinkYoneda.{w, v, u}.obj X = FunctorToTypes.shrink.{w, v, v, u} (yoneda.obj X)

noncomputable def CategoryTheory.shrinkYonedaObjObjEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : C} {Y : Cᵒᵖ} : (shrinkYoneda.{w, v, u}.obj X).obj Y ≃ (Opposite.unop Y ⟶ X)

The type (shrinkYoneda.obj X).obj Y is equivalent to Y.unop ⟶ X.

noncomputable def CategoryTheory.shrinkYonedaEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : C} {P : Functor Cᵒᵖ (Type w)} : (shrinkYoneda.{w, v, u}.obj X ⟶ P) ≃ P.obj (Opposite.op X)

The type of natural transformations shrinkYoneda.{w}.obj X ⟶ P with X : C and P : Cᵒᵖ ⥤ Type w is equivalent to P.obj (op X).

theorem CategoryTheory.map_shrinkYonedaEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : C} {P : Functor Cᵒᵖ (Type w)} (f : shrinkYoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X) : P.map g.op (shrinkYonedaEquiv f) = f.app (Opposite.op Y) (shrinkYonedaObjObjEquiv.symm g)

theorem CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) : shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map f) = shrinkYonedaObjObjEquiv.symm f

theorem CategoryTheory.shrinkYonedaEquiv_comp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : C} {P Q : Functor Cᵒᵖ (Type w)} (α : shrinkYoneda.{w, v, u}.obj X ⟶ P) (β : P ⟶ Q) : shrinkYonedaEquiv (CategoryStruct.comp α β) = β.app (Opposite.op X) (shrinkYonedaEquiv α)

theorem CategoryTheory.shrinkYonedaEquiv_naturality {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : C} {P : Functor Cᵒᵖ (Type w)} (f : shrinkYoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X) : P.map g.op (shrinkYonedaEquiv f) = shrinkYonedaEquiv (CategoryStruct.comp (shrinkYoneda.{w, v, u}.map g) f)

theorem CategoryTheory.shrinkYonedaEquiv_symm_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) {P : Functor Cᵒᵖ (Type w)} (t : P.obj X) : shrinkYonedaEquiv.symm (P.map f t) = CategoryStruct.comp (shrinkYoneda.{w, v, u}.map f.unop) (shrinkYonedaEquiv.symm t)

theorem CategoryTheory.shrinkYonedaEquiv_symm_map_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) {P : Functor Cᵒᵖ (Type w)} (t : P.obj X) {Z : Functor Cᵒᵖ (Type w)} (h : P ⟶ Z) : CategoryStruct.comp (shrinkYonedaEquiv.symm (P.map f t)) h = CategoryStruct.comp (shrinkYoneda.{w, v, u}.map f.unop) (CategoryStruct.comp (shrinkYonedaEquiv.symm t) h)

noncomputable def CategoryTheory.fullyFaithfulShrinkYoneda (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] : shrinkYoneda.{w, v, u}.FullyFaithful

The functor shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w for a locally w-small category C is fully faithful.

instance CategoryTheory.instFaithfulFunctorOppositeTypeShrinkYoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] : shrinkYoneda.{w, v, u}.Faithful

instance CategoryTheory.instFullFunctorOppositeTypeShrinkYoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] : shrinkYoneda.{w, v, u}.Full