The restricted Yoneda functor

If F : C ⥤ D is a functor and D is a locally w-small category, we define a functor Presheaf.restrictedShrinkYoneda : D ⥤ Cᵒᵖ ⥤ Type w which sends Y : D and X : Cᵒᵖ to a type that is equivalent to F.obj X.unop ⟶ Y. (We also provide restrictedYoneda and restrictedULiftYoneda variants.)

References

• S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic

@[implicit_reducible]

noncomputable def CategoryTheory.Presheaf.restrictedShrinkYoneda {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [LocallySmall.{w, v', u'} D] (F : Functor C D) : Functor D (Functor Cᵒᵖ (Type w))

Given a functor F : C ⥤ D where D is locally w-small, this is the bifunctor D ⥤ Cᵒᵖ ⥤ Type w which sends Y : D and X : C to (shrinkYoneda.{w}.obj Y).obj (op (F.obj X)), which is a type that is equivalent to F.obj X ⟶ Y.

Equations

• CategoryTheory.Presheaf.restrictedShrinkYoneda F = CategoryTheory.shrinkYoneda.{?u.5, ?u.3, ?u.1}.comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type ?u.5)).obj F.op)

@[simp]

theorem CategoryTheory.Presheaf.restrictedShrinkYoneda_map_app {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [LocallySmall.{w, v', u'} D] (F : Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) : ((restrictedShrinkYoneda F).map f).app X = (shrinkYoneda.{w, v', u'}.map f).app (Opposite.op (F.obj (Opposite.unop X)))

@[simp]

theorem CategoryTheory.Presheaf.restrictedShrinkYoneda_obj_obj {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [LocallySmall.{w, v', u'} D] (F : Functor C D) (X : D) (X✝ : Cᵒᵖ) : ((restrictedShrinkYoneda F).obj X).obj X✝ = (shrinkYoneda.{w, v', u'}.obj X).obj (Opposite.op (F.obj (Opposite.unop X✝)))

@[simp]

theorem CategoryTheory.Presheaf.restrictedShrinkYoneda_obj_map {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [LocallySmall.{w, v', u'} D] (F : Functor C D) (X : D) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : ((restrictedShrinkYoneda F).obj X).map f = (shrinkYoneda.{w, v', u'}.obj X).map (F.map f.unop).op

@[implicit_reducible]

def CategoryTheory.Presheaf.restrictedYoneda {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) : Functor D (Functor Cᵒᵖ (Type v'))

Given a functor F : C ⥤ D where the morphisms in D are in Type v', this is the bifunctor D ⥤ Cᵒᵖ ⥤ Type v' which sends Y : D and X : C to F.obj X ⟶ Y.

Equations

• CategoryTheory.Presheaf.restrictedYoneda F = CategoryTheory.yoneda.comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type ?u.3)).obj F.op)

@[simp]

theorem CategoryTheory.Presheaf.restrictedYoneda_obj_obj {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) (X : D) (X✝ : Cᵒᵖ) : ((restrictedYoneda F).obj X).obj X✝ = (F.obj (Opposite.unop X✝) ⟶ X)

@[simp]

theorem CategoryTheory.Presheaf.restrictedYoneda_map_app {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) : ((restrictedYoneda F).map f).app X = TypeCat.ofHom fun (g : F.obj (Opposite.unop X) ⟶ X✝) => CategoryStruct.comp g f

@[simp]

theorem CategoryTheory.Presheaf.restrictedYoneda_obj_map {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) (X : D) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : ((restrictedYoneda F).obj X).map f = TypeCat.ofHom fun (g : F.obj (Opposite.unop X✝) ⟶ X) => CategoryStruct.comp (F.map f.unop) g

@[implicit_reducible]

def CategoryTheory.Presheaf.restrictedULiftYoneda {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) : Functor D (Functor Cᵒᵖ (Type (max w v')))

Given a functor F : C ⥤ D where the morphisms in D are in Type v', this is the bifunctor D ⥤ Cᵒᵖ ⥤ Type max w v' which sends Y : D and X : C to (uliftYoneda.{w}.obj Y).obj (op (F.obj X)), which is a type that is equivalent to F.obj X ⟶ Y.

Equations

• CategoryTheory.Presheaf.restrictedULiftYoneda F = CategoryTheory.uliftYoneda.{?u.5, ?u.3, ?u.1}.comp ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max ?u.5 ?u.3))).obj F.op)

@[simp]

theorem CategoryTheory.Presheaf.restrictedULiftYoneda_obj_obj {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) (X : D) (X✝ : Cᵒᵖ) : ((restrictedULiftYoneda F).obj X).obj X✝ = ULift.{w, v'} (F.obj (Opposite.unop X✝) ⟶ X)

@[simp]

theorem CategoryTheory.Presheaf.restrictedULiftYoneda_obj_map {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) (X : D) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : ((restrictedULiftYoneda F).obj X).map f = TypeCat.ofHom fun (x : ULift.{w, v'} (F.obj (Opposite.unop X✝) ⟶ X)) => { down := CategoryStruct.comp (F.map f.unop) x.down }

@[simp]

theorem CategoryTheory.Presheaf.restrictedULiftYoneda_map_app {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (X : Cᵒᵖ) : ((restrictedULiftYoneda F).map f).app X = TypeCat.ofHom fun (x : ULift.{w, v'} (F.obj (Opposite.unop X) ⟶ X✝)) => { down := CategoryStruct.comp x.down f }

theorem CategoryTheory.Presheaf.map_comp_uliftYonedaEquiv_down {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) {E : D} {X Y : C} (f : X ⟶ Y) (g : uliftYoneda.{max w v', v, u}.obj Y ⟶ (restrictedULiftYoneda F).obj E) : CategoryStruct.comp (F.map f) (uliftYonedaEquiv g).down = (uliftYonedaEquiv (CategoryStruct.comp (uliftYoneda.{max v' w, v, u}.map f) g)).down

theorem CategoryTheory.Presheaf.map_comp_uliftYonedaEquiv_down_assoc {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) {E : D} {X Y : C} (f : X ⟶ Y) (g : uliftYoneda.{max w v', v, u}.obj Y ⟶ (restrictedULiftYoneda F).obj E) {Z : D} (h : E ⟶ Z) : CategoryStruct.comp (F.map f) (CategoryStruct.comp (uliftYonedaEquiv g).down h) = CategoryStruct.comp (uliftYonedaEquiv (CategoryStruct.comp (uliftYoneda.{max v' w, v, u}.map f) g)).down h

@[reducible, inline]

noncomputable abbrev CategoryTheory.Presheaf.restrictedULiftYonedaIso {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) : restrictedULiftYoneda F ≅ restrictedShrinkYoneda F

Given a functor F : C ⥤ D, this is the isomorphism between restrictedULiftYoneda.{w} F and restrictedShrinkYoneda.{max w v'} F when the types of morphisms in D are in Type v'.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Presheaf.restrictedYonedaIso {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] (F : Functor C D) : restrictedYoneda F ≅ restrictedShrinkYoneda F

Given a functor F : C ⥤ D, this is the isomorphism between restrictedYoneda F and restrictedShrinkYoneda.{v'} F when the types of morphisms in D are in Type v'.

Equations

• One or more equations did not get rendered due to their size.