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✝

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

Shrinking F to Type w followed by universe lifting is the same as shrinking to Type (max w w').

@[simp]

theorem CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso_hom_app {C : Type u} [Category.{v, u} C] (F : Functor C (Type w')) [FunctorToTypes.Small.{w, w', v, u} F] [FunctorToTypes.Small.{max w w'', w', v, u} F] (X : C) (a✝ : ((shrink.{w, w', v, u} F).comp uliftFunctor.{w'', w}).obj X) : (shrinkCompUliftFunctorIso F).hom.app X a✝ = (equivShrink (F.obj X)) ((equivShrink (F.obj X)).symm a✝.down)

@[simp]

theorem CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso_inv_app_down {C : Type u} [Category.{v, u} C] (F : Functor C (Type w')) [FunctorToTypes.Small.{w, w', v, u} F] [FunctorToTypes.Small.{max w w'', w', v, u} F] (X : C) (a✝ : (shrink.{max w w'', w', v, u} F).obj X) : ((shrinkCompUliftFunctorIso F).inv.app X a✝).down = (equivShrink (F.obj 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_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)

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)

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.

theorem CategoryTheory.shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Opposite.unop Y ⟶ X) : (shrinkYoneda.{w, v, u}.obj X).map g (shrinkYonedaObjObjEquiv.symm f) = shrinkYonedaObjObjEquiv.symm (CategoryStruct.comp g.unop f)

theorem CategoryTheory.shrinkYonedaObjObjEquiv_symm_comp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) : shrinkYonedaObjObjEquiv.symm (CategoryStruct.comp g f) = (shrinkYoneda.{w, v, u}.obj X).map g.op (shrinkYonedaObjObjEquiv.symm f)

theorem CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X X' : C} {Y : Cᵒᵖ} (f : Opposite.unop Y ⟶ X) (g : X ⟶ X') : (shrinkYoneda.{w, v, u}.map g).app Y (shrinkYonedaObjObjEquiv.symm f) = shrinkYonedaObjObjEquiv.symm (CategoryStruct.comp f g)

theorem CategoryTheory.shrinkYonedaObjObjEquiv_map_app {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X X' : C} {Y : Cᵒᵖ} (f : (shrinkYoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') : shrinkYonedaObjObjEquiv ((shrinkYoneda.{w, v, u}.map g).app Y f) = CategoryStruct.comp (shrinkYonedaObjObjEquiv f) g

theorem CategoryTheory.shrinkYonedaObjObjEquiv_map_app_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X X' : C} {Y : Cᵒᵖ} (f : (shrinkYoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') {Z : C} (h : X' ⟶ Z) : CategoryStruct.comp (shrinkYonedaObjObjEquiv ((shrinkYoneda.{w, v, u}.map g).app Y f)) h = CategoryStruct.comp (shrinkYonedaObjObjEquiv f) (CategoryStruct.comp g h)

theorem CategoryTheory.shrinkYonedaObjObjEquiv_obj_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : (shrinkYoneda.{w, v, u}.obj X).obj Y) : shrinkYonedaObjObjEquiv ((shrinkYoneda.{w, v, u}.obj X).map g f) = CategoryStruct.comp g.unop (shrinkYonedaObjObjEquiv f)

theorem CategoryTheory.shrinkYonedaObjObjEquiv_obj_map_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : (shrinkYoneda.{w, v, u}.obj X).obj Y) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (shrinkYonedaObjObjEquiv ((shrinkYoneda.{w, v, u}.obj X).map g f)) h = CategoryStruct.comp g.unop (CategoryStruct.comp (shrinkYonedaObjObjEquiv f) h)

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)

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

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

noncomputable def CategoryTheory.shrinkYonedaIsoYoneda {C : Type u} [Category.{v, u} C] : shrinkYoneda.{v, v, u} ≅ yoneda

shrinkYoneda at the morphism universe level is yoneda.

@[simp]

theorem CategoryTheory.shrinkYonedaIsoYoneda_inv_app_app {C : Type u} [Category.{v, u} C] (X : C) (X✝ : Cᵒᵖ) (a✝ : (yoneda.obj X).obj X✝) : (shrinkYonedaIsoYoneda.inv.app X).app X✝ a✝ = shrinkYonedaObjObjEquiv.symm a✝

@[simp]

theorem CategoryTheory.shrinkYonedaIsoYoneda_hom_app_app {C : Type u} [Category.{v, u} C] (X : C) (X✝ : Cᵒᵖ) (a✝ : (shrinkYoneda.{v, v, u}.obj X).obj X✝) : (shrinkYonedaIsoYoneda.hom.app X).app X✝ a✝ = shrinkYonedaObjObjEquiv a✝

noncomputable def CategoryTheory.shrinkYonedaUliftFunctorIso {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] [LocallySmall.{max w w', v, u} C] : shrinkYoneda.{w, v, u}.comp ((Functor.whiskeringRight Cᵒᵖ (Type w) (Type (max w w'))).obj uliftFunctor.{w', w}) ≅ shrinkYoneda.{max w w', v, u}

shrinkYoneda is compatible with uliftFunctor.

noncomputable def CategoryTheory.uliftYonedaIsoShrinkYoneda {C : Type u} [Category.{v, u} C] : uliftYoneda.{w', v, u} ≅ shrinkYoneda.{max w' v, v, u}

uliftYoneda identifies to shrinkYoneda.

noncomputable def CategoryTheory.shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctor {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (Y : Cᵒᵖ) : shrinkYoneda.{w, v, u}.comp (((evaluation Cᵒᵖ (Type w)).obj Y).comp uliftFunctor.{v, w}) ≅ (coyoneda.obj Y).comp uliftFunctor.{w, v}

The functor shrinkYoneda.{w} followed by the evaluation at Y : Cᵒᵖ and uliftFunctor.{v} identifies to coyoneda.obj Y followed by uliftFunctor.{w}.

noncomputable def CategoryTheory.shrinkYonedaRepresentableBy {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) : (shrinkYoneda.{w, v, u}.obj X).RepresentableBy X

shrinkYoneda.obj X is represented by X.

@[simp]

theorem CategoryTheory.shrinkYonedaRepresentableBy_homEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) {X✝ : C} : (shrinkYonedaRepresentableBy X).homEquiv = shrinkYonedaObjObjEquiv.symm

instance CategoryTheory.instIsRepresentableObjFunctorOppositeTypeShrinkYoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : C) : (shrinkYoneda.{w, v, u}.obj X).IsRepresentable