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.

@[implicit_reducible]

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✝) : (shrink.{w, w', v, u} F).map f = TypeCat.ofHom (⇑(equivShrink (F.obj Y✝)) ∘ ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(equivShrink (F.obj X✝)).symm)

@[implicit_reducible]

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) : (shrinkMap τ).app X = TypeCat.ofHom (⇑(equivShrink (G.obj X)) ∘ ⇑(ConcreteCategory.hom (τ.app X)) ∘ ⇑(equivShrink (F.obj X)).symm)

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) : (shrinkCompUliftFunctorIso F).hom.app X = ((Equiv.ulift.trans (equivShrink (F.obj X)).symm).trans (equivShrink (F.obj X))).toIso.hom

@[simp]

theorem CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso_inv_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) : (shrinkCompUliftFunctorIso F).inv.app X = ((Equiv.ulift.trans (equivShrink (F.obj X)).symm).trans (equivShrink (F.obj X))).toIso.inv

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.

theorem CategoryTheory.shrinkYoneda_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) : (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj X).map g)) f = shrinkYonedaObjObjEquiv.symm (CategoryStruct.comp g.unop (shrinkYonedaObjObjEquiv f))

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) : (ConcreteCategory.hom ((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) = (ConcreteCategory.hom ((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') : (ConcreteCategory.hom ((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 ((ConcreteCategory.hom ((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 ((ConcreteCategory.hom ((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 ((ConcreteCategory.hom ((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 ((ConcreteCategory.hom ((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) : (ConcreteCategory.hom (P.map g.op)) (shrinkYonedaEquiv f) = (ConcreteCategory.hom (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 α β) = (ConcreteCategory.hom (β.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) : (ConcreteCategory.hom (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 ((ConcreteCategory.hom (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 ((ConcreteCategory.hom (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) : (ConcreteCategory.hom ((shrinkYonedaEquiv.symm s).app (Opposite.op Y))) (shrinkYonedaObjObjEquiv.symm f) = (ConcreteCategory.hom (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 {C : Type u} [Category.{v, u} C] (X : C) : shrinkYonedaIsoYoneda.inv.app X = (NatIso.ofComponents (fun (Y : Cᵒᵖ) => shrinkYonedaObjObjEquiv.toIso) ⋯).inv

@[simp]

theorem CategoryTheory.shrinkYonedaIsoYoneda_hom_app {C : Type u} [Category.{v, u} C] (X : C) : shrinkYonedaIsoYoneda.hom.app X = (NatIso.ofComponents (fun (Y : Cᵒᵖ) => shrinkYonedaObjObjEquiv.toIso) ⋯).hom

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

instance CategoryTheory.instSmallObjOppositeFunctorTypeCoyoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : Cᵒᵖ) : FunctorToTypes.Small.{w, v, v, u} (coyoneda.obj X)

@[reducible, inline]

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

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

theorem CategoryTheory.shrinkCoyoneda_obj {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : Cᵒᵖ} : shrinkCoyoneda.{w, v, u}.obj X = FunctorToTypes.shrink.{w, v, v, u} (coyoneda.obj X)

theorem CategoryTheory.shrinkCoyoneda_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ} {f : X ⟶ Y} : shrinkCoyoneda.{w, v, u}.map f = FunctorToTypes.shrinkMap (coyoneda.map f)

@[reducible, inline]

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

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

theorem CategoryTheory.shrinkCoyoneda_obj_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y) : (ConcreteCategory.hom ((shrinkCoyoneda.{w, v, u}.obj X).map g)) f = shrinkCoyonedaObjObjEquiv.symm (CategoryStruct.comp (shrinkCoyonedaObjObjEquiv f) g)

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

theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_symm_comp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) : shrinkCoyonedaObjObjEquiv.symm (CategoryStruct.comp g f) = (ConcreteCategory.hom ((shrinkCoyoneda.{w, v, u}.obj (Opposite.op Y')).map f)) (shrinkCoyonedaObjObjEquiv.symm g)

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

theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_map_app {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ} {Y : C} (f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') : shrinkCoyonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkCoyoneda.{w, v, u}.map g).app Y)) f) = CategoryStruct.comp g.unop (shrinkCoyonedaObjObjEquiv f)

theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_map_app_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X X' : Cᵒᵖ} {Y : C} (f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X') {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (shrinkCoyonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkCoyoneda.{w, v, u}.map g).app Y)) f)) h = CategoryStruct.comp g.unop (CategoryStruct.comp (shrinkCoyonedaObjObjEquiv f) h)

theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_obj_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y) : shrinkCoyonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkCoyoneda.{w, v, u}.obj X).map g)) f) = CategoryStruct.comp (shrinkCoyonedaObjObjEquiv f) g

theorem CategoryTheory.shrinkCoyonedaObjObjEquiv_obj_map_assoc {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {Y Y' : C} (g : Y ⟶ Y') (f : (shrinkCoyoneda.{w, v, u}.obj X).obj Y) {Z : C} (h : Y' ⟶ Z) : CategoryStruct.comp (shrinkCoyonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkCoyoneda.{w, v, u}.obj X).map g)) f)) h = CategoryStruct.comp (shrinkCoyonedaObjObjEquiv f) (CategoryStruct.comp g h)

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

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

theorem CategoryTheory.map_shrinkCoyonedaEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ} {P : Functor C (Type w)} (f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X) : (ConcreteCategory.hom (P.map g.unop)) (shrinkCoyonedaEquiv f) = (ConcreteCategory.hom (f.app (Opposite.unop Y))) (shrinkCoyonedaObjObjEquiv.symm g.unop)

theorem CategoryTheory.shrinkCoyonedaEquiv_shrinkCoyoneda_map {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map f) = shrinkCoyonedaObjObjEquiv.symm f.unop

theorem CategoryTheory.shrinkCoyonedaEquiv_comp {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {P Q : Functor C (Type w)} (α : shrinkCoyoneda.{w, v, u}.obj X ⟶ P) (β : P ⟶ Q) : shrinkCoyonedaEquiv (CategoryStruct.comp α β) = (ConcreteCategory.hom (β.app (Opposite.unop X))) (shrinkCoyonedaEquiv α)

theorem CategoryTheory.shrinkCoyonedaEquiv_naturality {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ} {P : Functor C (Type w)} (f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X) : (ConcreteCategory.hom (P.map g.unop)) (shrinkCoyonedaEquiv f) = shrinkCoyonedaEquiv (CategoryStruct.comp (shrinkCoyoneda.{w, v, u}.map g) f)

theorem CategoryTheory.shrinkCoyonedaEquiv_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) : shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t) = CategoryStruct.comp (shrinkCoyoneda.{w, v, u}.map f.op) (shrinkCoyonedaEquiv.symm t)

theorem CategoryTheory.shrinkCoyonedaEquiv_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 (shrinkCoyonedaEquiv.symm ((ConcreteCategory.hom (P.map f)) t)) h = CategoryStruct.comp (shrinkCoyoneda.{w, v, u}.map f.op) (CategoryStruct.comp (shrinkCoyonedaEquiv.symm t) h)

theorem CategoryTheory.shrinkCoyonedaEquiv_symm_app_shrinkCoyonedaObjObjEquiv_symm {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] {X : Cᵒᵖ} {P : Functor C (Type w)} (s : P.obj (Opposite.unop X)) {Y : Cᵒᵖ} (f : Y ⟶ X) : (ConcreteCategory.hom ((shrinkCoyonedaEquiv.symm s).app (Opposite.unop Y))) (shrinkCoyonedaObjObjEquiv.symm f.unop) = (ConcreteCategory.hom (P.map f.unop)) s

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

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

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

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

noncomputable def CategoryTheory.shrinkCoyonedaIsoCoyoneda {C : Type u} [Category.{v, u} C] : shrinkCoyoneda.{v, v, u} ≅ coyoneda

shrinkCoyoneda at the morphism universe level is coyoneda.

@[simp]

theorem CategoryTheory.shrinkCoyonedaIsoCoyoneda_inv_app {C : Type u} [Category.{v, u} C] (X : Cᵒᵖ) : shrinkCoyonedaIsoCoyoneda.inv.app X = (NatIso.ofComponents (fun (Y : C) => shrinkCoyonedaObjObjEquiv.toIso) ⋯).inv

@[simp]

theorem CategoryTheory.shrinkCoyonedaIsoCoyoneda_hom_app {C : Type u} [Category.{v, u} C] (X : Cᵒᵖ) : shrinkCoyonedaIsoCoyoneda.hom.app X = (NatIso.ofComponents (fun (Y : C) => shrinkCoyonedaObjObjEquiv.toIso) ⋯).hom

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

shrinkCoyoneda is compatible with uliftFunctor.

noncomputable def CategoryTheory.uliftYonedaIsoShrinkCoyoneda {C : Type u} [Category.{v, u} C] : uliftCoyoneda.{w', v, u} ≅ shrinkCoyoneda.{max w' v, v, u}

uliftCoyoneda identifies to shrinkCoyoneda.

noncomputable def CategoryTheory.shrinkCoyonedaCompEvaluationCompUliftFunctorIsoUliftFunctor {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (Y : C) : shrinkCoyoneda.{w, v, u}.comp (((evaluation C (Type w)).obj Y).comp uliftFunctor.{v, w}) ≅ (yoneda.obj Y).comp uliftFunctor.{w, v}

The functor shrinkCoyoneda.{w} followed by the evaluation at Y : C and uliftFunctor.{v} identifies to yoneda.obj Y followed by uliftFunctor.{w}.

noncomputable def CategoryTheory.shrinkCoyonedaCorepresentableBy {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : Cᵒᵖ) : (shrinkCoyoneda.{w, v, u}.obj X).CorepresentableBy (Opposite.unop X)

shrinkCoyoneda.obj X is corepresented by X.

@[simp]

theorem CategoryTheory.shrinkCoyonedaCorepresentableBy_homEquiv {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : Cᵒᵖ) {Y✝ : C} : (shrinkCoyonedaCorepresentableBy X).homEquiv = shrinkCoyonedaObjObjEquiv.symm

instance CategoryTheory.instIsCorepresentableObjOppositeFunctorTypeShrinkCoyoneda {C : Type u} [Category.{v, u} C] [LocallySmall.{w, v, u} C] (X : Cᵒᵖ) : (shrinkCoyoneda.{w, v, u}.obj X).IsCorepresentable