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.

A dual API for pointwise right Kan extension is also formalized.

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

@[reducible, inline]

abbrev CategoryTheory.Functor.HasPointwiseRightKanExtensionAt {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 right Kan extension along L at Y. It means that the functor StructuredArrow.proj Y L ⋙ F : StructuredArrow Y L ⥤ H has a limit.

Equations

• L.HasPointwiseRightKanExtensionAt F Y = CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)

@[reducible, inline]

abbrev CategoryTheory.Functor.HasPointwiseRightKanExtension {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 right Kan extension along L: it means that it has a pointwise right Kan extension at any object.

Equations

• L.HasPointwiseRightKanExtension F = ∀ (Y : D), L.HasPointwiseRightKanExtensionAt F 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)

@[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

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 of this cocone is E.right.obj Y

Equations

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

@[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

@[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

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.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_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} (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_3) u_1)

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)

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.

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.RightExtension.coneAt_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.RightExtension F) (Y : D) : (E.coneAt Y).pt = E.left.obj Y

@[simp]

theorem CategoryTheory.Functor.RightExtension.coneAt_π_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.RightExtension F) (Y : D) (g : CategoryTheory.StructuredArrow Y L) : (E.coneAt Y).π.app g = CategoryTheory.CategoryStruct.comp (E.left.map g.hom) (E.hom.app g.right)

def CategoryTheory.Functor.RightExtension.coneAt {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.RightExtension F) (Y : D) : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F)

The cone for StructuredArrow.proj Y L ⋙ F attached to E : RightExtension L F. The point of this cone is E.left.obj Y

Equations

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

@[simp]

theorem CategoryTheory.Functor.RightExtension.coneAtFunctor_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.RightExtension F} {E' : L.RightExtension F} (φ : E ⟶ E') : ((CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).map φ).hom = φ.left.app Y

@[simp]

theorem CategoryTheory.Functor.RightExtension.coneAtFunctor_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.RightExtension F) : (CategoryTheory.Functor.RightExtension.coneAtFunctor L F Y).obj E = E.coneAt Y

def CategoryTheory.Functor.RightExtension.coneAtFunctor {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.RightExtension F) (CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj Y L).comp F))

The cones for StructuredArrow.proj Y L ⋙ F, as a functor from RightExtension L F.

Equations

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

def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt {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.RightExtension F) (Y : D) : Type (max (max (max u_1 u_5) u_3) u_6)

A right extension E : RightExtension L F is a pointwise right Kan extension at Y when E.coneAt Y is a limit cone.

Equations

• E.IsPointwiseRightKanExtensionAt Y = CategoryTheory.Limits.IsLimit (E.coneAt Y)

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt {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.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) : L.HasPointwiseRightKanExtensionAt F Y

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.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.RightExtension F) {X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] : CategoryTheory.IsIso (E.hom.app X)

@[reducible, inline]

abbrev CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension {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.RightExtension F) : Type (max (max (max (max u_2 u_6) u_5) u_3) u_1)

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

Equations

• E.IsPointwiseRightKanExtension = ((Y : D) → E.IsPointwiseRightKanExtensionAt Y)

def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtEquivOfIso {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.RightExtension F} {E' : L.RightExtension F} (e : E ≅ E') (Y : D) : E.IsPointwiseRightKanExtensionAt Y ≃ E'.IsPointwiseRightKanExtensionAt Y

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

Equations

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

def CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionEquivOfIso {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.RightExtension F} {E' : L.RightExtension F} (e : E ≅ E') : E.IsPointwiseRightKanExtension ≃ E'.IsPointwiseRightKanExtension

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

Equations

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

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension {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.RightExtension F} (h : E.IsPointwiseRightKanExtension) : L.HasPointwiseRightKanExtension F

def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.homTo {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.RightExtension F} (h : E.IsPointwiseRightKanExtension) (G : L.RightExtension F) : G ⟶ E

The (unique) morphism to a pointwise right Kan extension.

Equations

• h.homTo G = CategoryTheory.CostructuredArrow.homMk { app := fun (Y : D) => (h Y).lift (G.coneAt Y), naturality := ⋯ } ⋯

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.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.RightExtension F} (h : E.IsPointwiseRightKanExtension) {G : L.RightExtension F} {f₁ : G ⟶ E} {f₂ : G ⟶ E} : f₁ = f₂

def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.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.RightExtension F} (h : E.IsPointwiseRightKanExtension) : CategoryTheory.CostructuredArrow.IsUniversal E

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

Equations

• h.isUniversal = CategoryTheory.Limits.IsTerminal.ofUniqueHom h.homTo ⋯

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isRightKanExtension {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.RightExtension F} (h : E.IsPointwiseRightKanExtension) : E.left.IsRightKanExtension E.hom

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasRightKanExtension {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.RightExtension F} (h : E.IsPointwiseRightKanExtension) : L.HasRightKanExtension F

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.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.RightExtension F} (h : E.IsPointwiseRightKanExtension) [L.Full] [L.Faithful] : CategoryTheory.IsIso E.hom

@[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)

@[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 := ⋯ } }

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_6, u_2} D] [CategoryTheory.Category.{u_5, 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_6, u_2} D] [CategoryTheory.Category.{u_5, 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.

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtension_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.HasPointwiseRightKanExtension F] (Y : D) : (L.pointwiseRightKanExtension F).obj Y = CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F)

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtension_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.HasPointwiseRightKanExtension F] {Y₁ : D} {Y₂ : D} (f : Y₁ ⟶ Y₂) : (L.pointwiseRightKanExtension F).map f = CategoryTheory.Limits.limit.lift ((CategoryTheory.StructuredArrow.proj Y₂ L).comp F) { pt := CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F), π := { app := fun (g : CategoryTheory.StructuredArrow Y₂ L) => CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj Y₁ L).comp F) ((CategoryTheory.StructuredArrow.map f).obj g), naturality := ⋯ } }

noncomputable def CategoryTheory.Functor.pointwiseRightKanExtension {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.HasPointwiseRightKanExtension F] : CategoryTheory.Functor D H

The constructed pointwise right Kan extension when HasPointwiseRightKanExtension L F holds.

Equations

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

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCounit_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.HasPointwiseRightKanExtension F] (X : C) : (L.pointwiseRightKanExtensionCounit F).app X = CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj (L.obj X) L).comp F) (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))

noncomputable def CategoryTheory.Functor.pointwiseRightKanExtensionCounit {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.HasPointwiseRightKanExtension F] : L.comp (L.pointwiseRightKanExtension F) ⟶ F

The counit of the constructed pointwise right Kan extension when HasPointwiseRightKanExtension L F holds.

Equations

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

noncomputable def CategoryTheory.Functor.pointwiseRightKanExtensionIsPointwiseRightKanExtension {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.HasPointwiseRightKanExtension F] : (CategoryTheory.Functor.RightExtension.mk (L.pointwiseRightKanExtension F) (L.pointwiseRightKanExtensionCounit F)).IsPointwiseRightKanExtension

The functor pointwiseRightKanExtension L F is a pointwise right Kan extension of F along L.

Equations

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

noncomputable def CategoryTheory.Functor.pointwiseRightKanExtensionIsUniversal {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.HasPointwiseRightKanExtension F] : CategoryTheory.CostructuredArrow.IsUniversal (CategoryTheory.Functor.RightExtension.mk (L.pointwiseRightKanExtension F) (L.pointwiseRightKanExtensionCounit F))

The functor pointwiseRightKanExtension L F is a right Kan extension of F along L.

Equations

• L.pointwiseRightKanExtensionIsUniversal F = (L.pointwiseRightKanExtensionIsPointwiseRightKanExtension F).isUniversal

instance CategoryTheory.Functor.instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit {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) [L.HasPointwiseRightKanExtension F] : (L.pointwiseRightKanExtension F).IsRightKanExtension (L.pointwiseRightKanExtensionCounit F)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instHasRightKanExtension {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) [L.HasPointwiseRightKanExtension F] : L.HasRightKanExtension F

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension {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.HasPointwiseRightKanExtension F] (F' : CategoryTheory.Functor D H) (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] : (CategoryTheory.Functor.RightExtension.mk F' α).IsPointwiseRightKanExtension

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

Equations

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