Pointwise Kan extensions

In this file, we define the notion of pointwise (left) Kan extension. Given two functors L : C ⥤ D and F : C ⥤ H, and E : LeftExtension L F, we introduce a cocone E.coconeAt Y for the functor CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H the point of which is E.right.obj Y, and the type E.IsPointwiseLeftKanExtensionAt Y which expresses that E.coconeAt Y is colimit. When this holds for all Y : D, we may say that E is a pointwise left Kan extension (E.IsPointwiseLeftKanExtension).

Conversely, when CostructuredArrow.proj L Y ⋙ F has a colimit, we say that F has a pointwise left Kan extension at Y : D (HasPointwiseLeftKanExtensionAt L F Y), and if this holds for all Y : D, we construct a functor pointwiseLeftKanExtension L F : D ⥤ H and show it is a pointwise Kan extension.

TODO

• obtain similar results for right Kan extensions
• refactor the file CategoryTheory.Limits.KanExtension using this new general API

References

• https://ncatlab.org/nlab/show/Kan+extension

@[reducible, inline]

abbrev CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) : Prop

The condition that a functor F has a pointwise left Kan extension along L at Y. It means that the functor CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H has a colimit.

Equations

• L.HasPointwiseLeftKanExtensionAt F Y = CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)

@[reducible, inline]

abbrev CategoryTheory.Functor.HasPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) : Prop

The condition that a functor F has a pointwise left Kan extension along L: it means that it has a pointwise left Kan extension at any object.

Equations

• L.HasPointwiseLeftKanExtension F = ∀ (Y : D), L.HasPointwiseLeftKanExtensionAt F Y

@[simp]

theorem CategoryTheory.Functor.LeftExtension.coconeAt_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D) : (E.coconeAt Y).pt = E.right.obj Y

@[simp]

theorem CategoryTheory.Functor.LeftExtension.coconeAt_ι_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D) (g : CategoryTheory.CostructuredArrow L Y) : (E.coconeAt Y).ι.app g = CategoryTheory.CategoryStruct.comp (E.hom.app g.left) (E.right.map g.hom)

def CategoryTheory.Functor.LeftExtension.coconeAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D) : CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj L Y).comp F)

The cocone for CostructuredArrow.proj L Y ⋙ F attached to E : LeftExtension L F. The point is this cocone is E.right.obj Y

Equations

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

def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D) : Type (max (max (max u_1 u_5) u_3) u_6)

A left extension E : LeftExtension L F is a pointwise left Kan extension at Y when E.coconeAt Y is a colimit cocone.

Equations

• E.IsPointwiseLeftKanExtensionAt Y = CategoryTheory.Limits.IsColimit (E.coconeAt Y)

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) : L.HasPointwiseLeftKanExtensionAt F Y

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isIso_hom_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {X : C} (h : E.IsPointwiseLeftKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] : CategoryTheory.IsIso (E.hom.app X)

@[reducible, inline]

abbrev CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) : Type (max (max (max (max u_2 u_6) u_5) u_1) u_3)

A left extension E : LeftExtension L F is a pointwise left Kan extension when it is a pointwise left Kan extension at any object.

Equations

• E.IsPointwiseLeftKanExtension = ((Y : D) → E.IsPointwiseLeftKanExtensionAt Y)

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) : L.HasPointwiseLeftKanExtension F

def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.homFrom {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) (G : L.LeftExtension F) : E ⟶ G

The (unique) morphism from a pointwise left Kan extension.

Equations

• h.homFrom G = CategoryTheory.StructuredArrow.homMk { app := fun (Y : D) => (h Y).desc (G.coconeAt Y), naturality := ⋯ } ⋯

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hom_ext {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) {G : L.LeftExtension F} {f₁ : E ⟶ G} {f₂ : E ⟶ G} : f₁ = f₂

def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isUniversal {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) : CategoryTheory.StructuredArrow.IsUniversal E

A pointwise left Kan extension is universal, i.e. it is a left Kan extension.

Equations

• h.isUniversal = CategoryTheory.Limits.IsInitial.ofUniqueHom h.homFrom ⋯

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) : E.right.IsLeftKanExtension E.hom

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_6, u_2} D] [CategoryTheory.Category.{u_5, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) : L.HasLeftKanExtension F

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) [L.Full] [L.Faithful] : CategoryTheory.IsIso E.hom

@[simp]

theorem CategoryTheory.Functor.LeftExtension.coconeAtFunctor_obj {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) (E : L.LeftExtension F) : (CategoryTheory.Functor.LeftExtension.coconeAtFunctor L F Y).obj E = E.coconeAt Y

@[simp]

theorem CategoryTheory.Functor.LeftExtension.coconeAtFunctor_map_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) {E : L.LeftExtension F} {E' : L.LeftExtension F} (φ : E ⟶ E') : ((CategoryTheory.Functor.LeftExtension.coconeAtFunctor L F Y).map φ).hom = φ.right.app Y

def CategoryTheory.Functor.LeftExtension.coconeAtFunctor {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (Y : D) : CategoryTheory.Functor (L.LeftExtension F) (CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj L Y).comp F))

The cocones for CostructuredArrow.proj L Y ⋙ F, as a functor from LeftExtension L F.

Equations

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

def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtEquivOfIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {E' : L.LeftExtension F} (e : E ≅ E') (Y : D) : E.IsPointwiseLeftKanExtensionAt Y ≃ E'.IsPointwiseLeftKanExtensionAt Y

If two left extensions E and E' are isomorphic, E is a pointwise left Kan extension at Y iff E' is.

Equations

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

def CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfIso {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {E' : L.LeftExtension F} (e : E ≅ E') : E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension

If two left extensions E and E' are isomorphic, E is a pointwise left Kan extension iff E' is.

Equations

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

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtension_map {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] {Y₁ : D} {Y₂ : D} (f : Y₁ ⟶ Y₂) : (L.pointwiseLeftKanExtension F).map f = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj L Y₁).comp F) { pt := CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F), ι := { app := fun (g : CategoryTheory.CostructuredArrow L Y₁) => CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y₂).comp F) ((CategoryTheory.CostructuredArrow.map f).obj g), naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtension_obj {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] (Y : D) : (L.pointwiseLeftKanExtension F).obj Y = CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)

noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : CategoryTheory.Functor D H

The constructed pointwise left Kan extension when HasPointwiseLeftKanExtension L F holds.

Equations

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

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtensionUnit_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] (X : C) : (L.pointwiseLeftKanExtensionUnit F).app X = CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L (L.obj X)).comp F) (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))

noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtensionUnit {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : F ⟶ L.comp (L.pointwiseLeftKanExtension F)

The unit of the constructed pointwise left Kan extension when HasPointwiseLeftKanExtension L F holds.

Equations

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

noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : (CategoryTheory.Functor.LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).IsPointwiseLeftKanExtension

The functor pointwiseLeftKanExtension L F is a pointwise left Kan extension of F along L.

Equations

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

noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtensionIsUniversal {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F))

The functor pointwiseLeftKanExtension L F is a left Kan extension of F along L.

Equations

• L.pointwiseLeftKanExtensionIsUniversal F = (L.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension F).isUniversal

instance CategoryTheory.Functor.instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : (L.pointwiseLeftKanExtension F).IsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instHasLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [L.HasPointwiseLeftKanExtension F] : L.HasLeftKanExtension F

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Category.{u_6, u_3} H] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} [L.HasPointwiseLeftKanExtension F] (F' : CategoryTheory.Functor D H) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] : (CategoryTheory.Functor.LeftExtension.mk F' α).IsPointwiseLeftKanExtension

If F admits a pointwise left Kan extension along L, then any left Kan extension of F along L is a pointwise left Kan extension.

Equations

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