Pointwise left Kan extension along the Yoneda embedding

Let A : C ⥤ D be a functor between locally w-small categories. In this file, we give a criterion Presheaf.isPointwiseLeftKanExtensionAlongShrinkYoneda to identify pointwise left Kan extensions of A along the Yoneda embedding (i.e. given by a natural transformation α : A ⟶ shrinkYoneda.{w} ⋙ L where L : (Cᵒᵖ ⥤ Type w) ⥤ D.): the natural transformation α should be an isomorphism and L should preserves colimits (at least those expressing presheaves as colimits of representable presheaves). Under such assumptions, we show that L has a right adjoint restrictedShrinkYoneda.{w} A : D ⥤ Cᵒᵖ ⥤ Type w, see Presheaf.restrictedShrinkYonedaAdjunction.

References

• S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic
• https://ncatlab.org/nlab/show/Yoneda+extension

noncomputable def CategoryTheory.Presheaf.isPointwiseLeftKanExtensionAlongShrinkYoneda {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [IsIso α] [∀ (P : Functor Cᵒᵖ (Type w)), Limits.PreservesColimit ((Functor.Elements.π P).leftOp.comp shrinkYoneda.{w, v₁, u₁}) L] : (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtension

Given functors A : C ⥤ D and L : (Cᵒᵖ ⥤ Type w) ⥤ D A left extension given by a natural transformation α : A ⟶ shrinkYoneda.{w} ⋙ L is a pointwise left Kan extension when α is an isomorphism and L preserves suitable colimits (more precisely, the expression of any presheaf P : Cᵒᵖ ⥤ Type w as a colimit of representable presheaves).

Equations

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

noncomputable def CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E : D} : (L.obj P ⟶ E) ≃ (P ⟶ (restrictedShrinkYoneda A).obj E)

Auxiliary definition for Presheaf.restrictedShrinkYonedaAdjunction.

Equations

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

@[simp]

theorem CategoryTheory.Presheaf.comp_restrictedShrinkYonedaHomEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E : D} (f : P ⟶ (restrictedShrinkYoneda A).obj E) {X : C} (g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ P) : CategoryStruct.comp (α.app X) (CategoryStruct.comp (L.map g) ((restrictedShrinkYonedaHomEquiv α).symm f)) = shrinkYonedaObjObjEquiv ((ConcreteCategory.hom (f.app (Opposite.op X))) (shrinkYonedaEquiv g))

@[simp]

theorem CategoryTheory.Presheaf.comp_restrictedShrinkYonedaHomEquiv_symm_apply_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E : D} (f : P ⟶ (restrictedShrinkYoneda A).obj E) {X : C} (g : shrinkYoneda.{w, v₁, u₁}.obj X ⟶ P) {Z : D} (h : E ⟶ Z) : CategoryStruct.comp (α.app X) (CategoryStruct.comp (L.map g) (CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α).symm f) h)) = CategoryStruct.comp (shrinkYonedaObjObjEquiv ((ConcreteCategory.hom (f.app (Opposite.op X))) (shrinkYonedaEquiv g))) h

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E : D} (f : L.obj P ⟶ E) {X : Cᵒᵖ} (x : P.obj X) : (ConcreteCategory.hom (((restrictedShrinkYonedaHomEquiv α) f).app X)) x = shrinkYonedaObjObjEquiv.symm (CategoryStruct.comp (α.app (Opposite.unop X)) (CategoryStruct.comp (L.map (shrinkYonedaEquiv.symm x)) f))

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_symm_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P P' : Functor Cᵒᵖ (Type w)} {E : D} (f : P ⟶ P') (g : P' ⟶ (restrictedShrinkYoneda A).obj E) : (restrictedShrinkYonedaHomEquiv α).symm (CategoryStruct.comp f g) = CategoryStruct.comp (L.map f) ((restrictedShrinkYonedaHomEquiv α).symm g)

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_symm_naturality_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P P' : Functor Cᵒᵖ (Type w)} {E : D} (f : P ⟶ P') (g : P' ⟶ (restrictedShrinkYoneda A).obj E) {Z : D} (h : E ⟶ Z) : CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α).symm (CategoryStruct.comp f g)) h = CategoryStruct.comp (L.map f) (CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α).symm g) h)

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_naturality_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P P' : Functor Cᵒᵖ (Type w)} {E : D} (f : P ⟶ P') (g : L.obj P' ⟶ E) : (restrictedShrinkYonedaHomEquiv α) (CategoryStruct.comp (L.map f) g) = CategoryStruct.comp f ((restrictedShrinkYonedaHomEquiv α) g)

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_naturality_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P P' : Functor Cᵒᵖ (Type w)} {E : D} (f : P ⟶ P') (g : L.obj P' ⟶ E) {Z : Functor Cᵒᵖ (Type w)} (h : (restrictedShrinkYoneda A).obj E ⟶ Z) : CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α) (CategoryStruct.comp (L.map f) g)) h = CategoryStruct.comp f (CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α) g) h)

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_symm_naturality_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E E' : D} (f : P ⟶ (restrictedShrinkYoneda A).obj E) (g : E ⟶ E') : (restrictedShrinkYonedaHomEquiv α).symm (CategoryStruct.comp f ((restrictedShrinkYoneda A).map g)) = CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α).symm f) g

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_symm_naturality_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E E' : D} (f : P ⟶ (restrictedShrinkYoneda A).obj E) (g : E ⟶ E') {Z : D} (h : E' ⟶ Z) : CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α).symm (CategoryStruct.comp f ((restrictedShrinkYoneda A).map g))) h = CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α).symm f) (CategoryStruct.comp g h)

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_naturality_right {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E E' : D} (f : L.obj P ⟶ E) (g : E ⟶ E') : (restrictedShrinkYonedaHomEquiv α) (CategoryStruct.comp f g) = CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α) f) ((restrictedShrinkYoneda A).map g)

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaHomEquiv_naturality_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type w)} {E E' : D} (f : L.obj P ⟶ E) (g : E ⟶ E') {Z : Functor Cᵒᵖ (Type w)} (h : (restrictedShrinkYoneda A).obj E' ⟶ Z) : CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α) (CategoryStruct.comp f g)) h = CategoryStruct.comp ((restrictedShrinkYonedaHomEquiv α) f) (CategoryStruct.comp ((restrictedShrinkYoneda A).map g) h)

noncomputable def CategoryTheory.Presheaf.restrictedShrinkYonedaAdjunction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] : L ⊣ restrictedShrinkYoneda A

Let α : A ⟶ shrinkYoneda.{w} ⋙ L be a pointwise left Kan extension of A : C ⥤ D along the Yoneda embedding. Then, L admits restrictedShrinkYoneda.{w} A as a right adjoint.

Equations

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

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaAdjunction_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] (P : Functor Cᵒᵖ (Type w)) (E : D) : (restrictedShrinkYonedaAdjunction α).homEquiv P E = restrictedShrinkYonedaHomEquiv α

theorem CategoryTheory.Presheaf.restrictedShrinkYonedaAdjunction_unit_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] (P : Functor Cᵒᵖ (Type w)) {X : Cᵒᵖ} (x : P.obj X) : (ConcreteCategory.hom (((restrictedShrinkYonedaAdjunction α).unit.app P).app X)) x = shrinkYonedaObjObjEquiv.symm (CategoryStruct.comp (α.app (Opposite.unop X)) (L.map (shrinkYonedaEquiv.symm x)))

theorem CategoryTheory.Presheaf.preservesColimitsOfSize_of_isLeftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] : Limits.PreservesColimitsOfSize.{v₃, u₃, max u₁ w, v₂, max (max u₁ v₁) (w + 1), u₂} L

Any left Kan extension along the Yoneda embedding preserves colimits.

instance CategoryTheory.Presheaf.instPreservesColimitsOfSizeFunctorOppositeTypeLeftKanExtensionShrinkYoneda {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {A : Functor C D} [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] : Limits.PreservesColimitsOfSize.{v₃, u₃, max w u₁, v₂, max (max (w + 1) u₁) v₁, u₂} (shrinkYoneda.{w, v₁, u₁}.leftKanExtension A)

See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.

instance CategoryTheory.Presheaf.isIso_of_isLeftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] [L.IsLeftKanExtension α] : IsIso α

theorem CategoryTheory.Presheaf.isLeftKanExtension_along_shrinkYoneda_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} (α : A ⟶ shrinkYoneda.{w, v₁, u₁}.comp L) [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] : L.IsLeftKanExtension α ↔ IsIso α ∧ Limits.PreservesColimitsOfSize.{v₁, max w u₁, max u₁ w, v₂, max (max u₁ v₁) (w + 1), u₂} L

theorem CategoryTheory.Presheaf.isLeftKanExtension_along_shrinkYoneda_of_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type w)) D} {A : Functor C D} [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension A] (e : shrinkYoneda.{w, v₁, u₁}.comp L ≅ A) [Limits.PreservesColimitsOfSize.{v₁, max w u₁, max u₁ w, v₂, max (max u₁ v₁) (w + 1), u₂} L] : L.IsLeftKanExtension e.inv

instance CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeIdCompShrinkYonedaOfHasPointwiseLeftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (L : Functor (Functor Cᵒᵖ (Type w)) D) [Limits.PreservesColimitsOfSize.{v₁, max w u₁, max u₁ w, v₂, max (max u₁ v₁) (w + 1), u₂} L] [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension (shrinkYoneda.{w, v₁, u₁}.comp L)] : L.IsLeftKanExtension (CategoryStruct.id (shrinkYoneda.{w, v₁, u₁}.comp L))

theorem CategoryTheory.Presheaf.isLeftAdjoint_of_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (L : Functor (Functor C (Type w)) D) [Limits.PreservesColimitsOfSize.{v₁, max w u₁, max u₁ w, v₂, max (max u₁ v₁) (w + 1), u₂} L] [shrinkYoneda.{w, v₁, u₁}.HasPointwiseLeftKanExtension (shrinkYoneda.{w, v₁, u₁}.comp ((opOpEquivalence C).congrLeft.functor.comp L))] : L.IsLeftAdjoint

theorem CategoryTheory.Presheaf.hasPointwiseLeftKanExtension_shrinkYoneda_of_uliftYoneda {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (A : Functor C D) [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] : shrinkYoneda.{max w v₁ v₂, v₁, u₁}.HasPointwiseLeftKanExtension A

theorem CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) : L.IsLeftKanExtension α ↔ IsIso α ∧ Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂, max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂} L

theorem CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_of_preservesColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} (e : uliftYoneda.{max w v₂, v₁, u₁}.comp L ≅ A) [Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂, max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂} L] : L.IsLeftKanExtension e.inv

instance CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeIdCompUliftYonedaOfPreservesColimitsOfSizeOfHasPointwiseLeftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D) [Limits.PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂, max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂} L] [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension (uliftYoneda.{max w v₂, v₁, u₁}.comp L)] : L.IsLeftKanExtension (CategoryStruct.id (uliftYoneda.{max w v₂, v₁, u₁}.comp L))

noncomputable def CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α] : L ⊣ restrictedULiftYoneda A

Let α : A ⟶ uliftYoneda ⋙ L be a pointwise left Kan extension of A : C ⥤ D along the Yoneda embedding. Then, L admits restrictedULiftYoneda.{max w v₁} A as a right adjoint.

Equations

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

theorem CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction_unit_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α] (P : Functor Cᵒᵖ (Type (max w v₁ v₂))) {X : Cᵒᵖ} (x : P.obj X) : (ConcreteCategory.hom (((restrictedULiftYonedaAdjunction α).unit.app P).app X)) x = { down := CategoryStruct.comp (α.app (Opposite.unop X)) (L.map (uliftYonedaEquiv.symm x)) }

@[simp]

theorem CategoryTheory.Presheaf.restrictedULiftYonedaAdjunction_homEquiv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α] {P : Functor Cᵒᵖ (Type (max w v₁ v₂))} {Y : D} (f : L.obj P ⟶ Y) {Z : Cᵒᵖ} (z : P.obj Z) : (ConcreteCategory.hom ((((restrictedULiftYonedaAdjunction α).homEquiv P Y) f).app Z)) z = { down := CategoryStruct.comp (α.app (Opposite.unop Z)) (CategoryStruct.comp (L.map (uliftYonedaEquiv.symm z)) f) }

instance CategoryTheory.Presheaf.instIsIsoFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {L : Functor (Functor Cᵒᵖ (Type (max w v₁ v₂))) D} {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] (α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁}.comp L) [L.IsLeftKanExtension α] : IsIso α

instance CategoryTheory.Presheaf.preservesColimitsOfSize_leftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A : Functor C D} [uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] : Limits.PreservesColimitsOfSize.{v₃, u₃, max (max (max v₂ w) u₁) v₁, v₂, max (max (max (v₂ + 1) (w + 1)) u₁) (v₁ + 1), u₂} (uliftYoneda.{max w v₂, v₁, u₁}.leftKanExtension A)

See Property 2 of https://ncatlab.org/nlab/show/Yoneda+extension#properties.