Documentation

Mathlib.CategoryTheory.Functor.KanExtension.Yoneda

F.op.lan is a pointwise left Kan extension #

Let F : C ⥤ D be a functor between locally w-small categories. Assume that F.op.lan : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w is defined. In this file, we show that F.op.lan is a pointwise left Kan extension of F ⋙ shrinkYoneda : C ⥤ Dᵒᵖ ⥤ Type w along the Yoneda embedding of C.

source
@[simp]
theorem CategoryTheory.Presheaf.shrinkYonedaEquiv_right_of_leftExtension_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (F : Functor C D) {X : C} {Y : F.op.LeftExtension (shrinkYoneda.{w, v₁, u₁}.obj X)} (φ : Functor.LeftExtension.mk (shrinkYoneda.{w, v₂, u₂}.obj (F.obj X)) (shrinkYonedaMap F X) ⟶ Y) :
shrinkYonedaEquiv (StructuredArrow.Hom.right φ) = shrinkYonedaEquiv (StructuredArrow.hom Y)
source
@[instance_reducible]
noncomputable instance CategoryTheory.Presheaf.instUniqueHomLeftExtensionOppositeOpObjFunctorTypeShrinkYonedaMkShrinkYonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (F : Functor C D) (X : C) (Y : F.op.LeftExtension (shrinkYoneda.{w, v₁, u₁}.obj X)) :
Unique (Functor.LeftExtension.mk (shrinkYoneda.{w, v₂, u₂}.obj (F.obj X)) (shrinkYonedaMap F X) ⟶ Y)
Equations
  • One or more equations did not get rendered due to their size.
source
instance CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeShrinkYonedaShrinkYonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (F : Functor C D) (X : C) :
(shrinkYoneda.{w, v₂, u₂}.obj (F.obj X)).IsLeftKanExtension (shrinkYonedaMap F X)

If F : C ⥤ D and X : C, the functor shrinkYoneda.obj (F.obj X) is a left Kan extension of shrinkYoneda.obj X along F.op.

source
noncomputable def CategoryTheory.Presheaf.compShrinkYonedaIsoShrinkYonedaCompLan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] :
F.comp shrinkYoneda.{w, v₂, u₂} ≅ shrinkYoneda.{w, v₁, u₁}.comp F.op.lan

F ⋙ shrinkYoneda is naturally isomorphic to shrinkYoneda ⋙ F.op.lan.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Presheaf.comp_whiskerLeft_compShrinkYonedaIsoShrinkYonedaCompLan_inv_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] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] (X : C) :
    CategoryStruct.comp (F.op.lanUnit.app (shrinkYoneda.{w, v₁, u₁}.obj X)) (F.op.whiskerLeft ((compShrinkYonedaIsoShrinkYonedaCompLan F).inv.app X)) = shrinkYonedaMap F X
    source
    @[simp]
    theorem CategoryTheory.Presheaf.comp_whiskerLeft_compShrinkYonedaIsoShrinkYonedaCompLan_inv_app_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] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] (X : C) {Z : Functor Cᵒᵖ (Type w)} (h : F.op.comp (shrinkYoneda.{w, v₂, u₂}.obj (F.obj X)) ⟶ Z) :
    CategoryStruct.comp (F.op.lanUnit.app (shrinkYoneda.{w, v₁, u₁}.obj X)) (CategoryStruct.comp (F.op.whiskerLeft ((compShrinkYonedaIsoShrinkYonedaCompLan F).inv.app X)) h) = CategoryStruct.comp (shrinkYonedaMap F X) h
    source
    @[simp]
    theorem CategoryTheory.Presheaf.comp_whiskerLeft_compShrinkYonedaIsoShrinkYonedaCompLan_hom_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] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] (X : C) :
    CategoryStruct.comp (shrinkYonedaMap F X) (F.op.whiskerLeft ((compShrinkYonedaIsoShrinkYonedaCompLan F).hom.app X)) = F.op.lanUnit.app (shrinkYoneda.{w, v₁, u₁}.obj X)
    source
    @[simp]
    theorem CategoryTheory.Presheaf.comp_whiskerLeft_compShrinkYonedaIsoShrinkYonedaCompLan_hom_app_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] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] (X : C) {Z : Functor Cᵒᵖ (Type w)} (h : F.op.comp (F.op.lan.obj (shrinkYoneda.{w, v₁, u₁}.obj X)) ⟶ Z) :
    CategoryStruct.comp (shrinkYonedaMap F X) (CategoryStruct.comp (F.op.whiskerLeft ((compShrinkYonedaIsoShrinkYonedaCompLan F).hom.app X)) h) = CategoryStruct.comp (F.op.lanUnit.app (shrinkYoneda.{w, v₁, u₁}.obj X)) h
    source
    @[simp]
    theorem CategoryTheory.Presheaf.compShrinkYonedaIsoShrinkYonedaCompLan_inv_app_app_eq_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] (X : C) :
    (ConcreteCategory.hom (((compShrinkYonedaIsoShrinkYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X)))) ((ConcreteCategory.hom ((F.op.lanUnit.app (shrinkYoneda.{w, v₁, u₁}.obj X)).app (Opposite.op X))) (shrinkYonedaObjObjEquiv.symm (CategoryStruct.id X))) = shrinkYonedaObjObjEquiv.symm (CategoryStruct.id (F.obj X))
    source
    noncomputable def CategoryTheory.Presheaf.isPointwiseLeftKanExtensionLanOp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] :
    (Functor.LeftExtension.mk F.op.lan (compShrinkYonedaIsoShrinkYonedaCompLan F).hom).IsPointwiseLeftKanExtension

    Let F : C ⥤ D be a functor between locally w-small categories. Assume that F.op.lan : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w is defined. Then, it is a pointwise left Kan extension of F ⋙ shrinkYoneda : C ⥤ Dᵒᵖ ⥤ Type w along the Yoneda embedding of C.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompShrinkYonedaIsoShrinkYonedaCompLan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [LocallySmall.{w, v₁, u₁} C] [LocallySmall.{w, v₂, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type w)), F.op.HasLeftKanExtension P] :
      F.op.lan.IsLeftKanExtension (compShrinkYonedaIsoShrinkYonedaCompLan F).hom
      source
      instance CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeYonedaYonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v₁, u_1} D] (F : Functor C D) (X : C) :
      (yoneda.obj (F.obj X)).IsLeftKanExtension (yonedaMap F X)

      If F : C ⥤ D and X : C, the functor yoneda.obj (F.obj X) is a left Kan extension of yoneda.obj X along F.op.

      source
      instance CategoryTheory.Presheaf.instIsLeftKanExtensionOppositeObjFunctorTypeUliftYonedaUliftYonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
      (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).IsLeftKanExtension (uliftYonedaMap F X)

      If F : C ⥤ D and X : C, the functor uliftYoneda.obj (F.obj X) is a left Kan extension of uliftYoneda.obj X along F.op.

      source
      noncomputable def CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] :
      F.comp uliftYoneda.{max w v₁, v₂, u₂} ≅ uliftYoneda.{max w v₂, v₁, u₁}.comp F.op.lan

      F ⋙ uliftYoneda is naturally isomorphic to uliftYoneda ⋙ F.op.lan.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] (X : C) :
        (ConcreteCategory.hom (((compULiftYonedaIsoULiftYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X)))) ((ConcreteCategory.hom ((F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).app (Opposite.op X))) { down := CategoryStruct.id X }) = { down := CategoryStruct.id (F.obj X) }
        source
        instance CategoryTheory.Presheaf.instIsLeftKanExtensionFunctorOppositeTypeLanOpHomCompULiftYonedaIsoULiftYonedaCompLan {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [∀ (P : Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] :
        F.op.lan.IsLeftKanExtension (compULiftYonedaIsoULiftYonedaCompLan F).hom