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

@[inline, reducible]

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

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

@[inline, reducible]

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

• CategoryTheory.Functor.HasPointwiseLeftKanExtension L F = ∀ (Y : D), CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt L 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 : CategoryTheory.Functor.LeftExtension L F) (Y : D) : (CategoryTheory.Functor.LeftExtension.coconeAt E 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 : CategoryTheory.Functor.LeftExtension L F) (Y : D) (g : CategoryTheory.CostructuredArrow L Y) : (CategoryTheory.Functor.LeftExtension.coconeAt E 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 : CategoryTheory.Functor.LeftExtension L F) (Y : D) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj L Y) 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 : CategoryTheory.Functor.LeftExtension L 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

• CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt E Y = CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.LeftExtension.coconeAt E 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 : CategoryTheory.Functor.LeftExtension L F} {Y : D} (h : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt E Y) : CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt L F Y

@[inline, reducible]

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 : CategoryTheory.Functor.LeftExtension L 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

• CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension E = ((Y : D) → CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt E 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 : CategoryTheory.Functor.LeftExtension L F} (h : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension E) : CategoryTheory.Functor.HasPointwiseLeftKanExtension L 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 : CategoryTheory.Functor.LeftExtension L F} (h : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension E) (G : CategoryTheory.Functor.LeftExtension L F) : E ⟶ G

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

Equations

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

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 : CategoryTheory.Functor.LeftExtension L F} (h : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension E) {G : CategoryTheory.Functor.LeftExtension L 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 : CategoryTheory.Functor.LeftExtension L F} (h : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension E) : CategoryTheory.StructuredArrow.IsUniversal E

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

Equations

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

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 : CategoryTheory.Functor.LeftExtension L F} (h : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension E) : CategoryTheory.Functor.IsLeftKanExtension E.right 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 : CategoryTheory.Functor.LeftExtension L F} (h : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension E) : CategoryTheory.Functor.HasLeftKanExtension L F

@[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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] (Y : D) : (CategoryTheory.Functor.pointwiseLeftKanExtension L F).obj Y = CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj L Y) F)

@[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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] {Y₁ : D} {Y₂ : D} (f : Y₁ ⟶ Y₂) : (CategoryTheory.Functor.pointwiseLeftKanExtension L F).map f = CategoryTheory.Limits.colimit.desc (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj L Y₁) F) { pt := CategoryTheory.Limits.colimit (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj L Y₂) F), ι := { app := fun (g : CategoryTheory.CostructuredArrow L Y₁) => CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj L Y₂) F) ((CategoryTheory.CostructuredArrow.map f).obj g), naturality := ⋯ } }

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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L 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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] (X : C) : (CategoryTheory.Functor.pointwiseLeftKanExtensionUnit L F).app X = CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (CategoryTheory.CostructuredArrow.proj L (L.obj X)) 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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] : F ⟶ CategoryTheory.Functor.comp L (CategoryTheory.Functor.pointwiseLeftKanExtension L 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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] : CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.pointwiseLeftKanExtension L F) (CategoryTheory.Functor.pointwiseLeftKanExtensionUnit L F))

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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] : CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.pointwiseLeftKanExtension L F) (CategoryTheory.Functor.pointwiseLeftKanExtensionUnit L F))

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

Equations

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

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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] : CategoryTheory.Functor.IsLeftKanExtension (CategoryTheory.Functor.pointwiseLeftKanExtension L F) (CategoryTheory.Functor.pointwiseLeftKanExtensionUnit L 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) [CategoryTheory.Functor.HasPointwiseLeftKanExtension L F] : CategoryTheory.Functor.HasLeftKanExtension L F

Equations

• ⋯ = ⋯