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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : 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

def CategoryTheory.Functor.LeftExtension.coconeAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} (E : L.LeftExtension F) (Y : D) : Limits.Cocone ((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.coconeAt_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} (E : L.LeftExtension F) (Y : D) (g : CostructuredArrow L Y) : (E.coconeAt Y).ι.app g = CategoryStruct.comp (E.hom.app g.left) (E.right.map g.hom)

def CategoryTheory.Functor.LeftExtension.coconeAtFunctor {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (Y : D) : Functor (L.LeftExtension F) (Limits.Cocone ((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.

@[simp]

theorem CategoryTheory.Functor.LeftExtension.coconeAtFunctor_map_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (Y : D) {E E' : L.LeftExtension F} (φ : E ⟶ E') : ((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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (Y : D) (E : L.LeftExtension F) : (coconeAtFunctor L F Y).obj E = E.coconeAt Y

def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} (E : L.LeftExtension F) {X : C} (h : E.IsPointwiseLeftKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] : IsIso (E.hom.app X)

noncomputable def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.isoColimit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) [Limits.HasColimit ((CostructuredArrow.proj L Y).comp F)] : E.right.obj Y ≅ Limits.colimit ((CostructuredArrow.proj L Y).comp F)

A pointwise left Kan extension of F along L applied to an object Y is isomorphic to colimit (CostructuredArrow.proj L Y ⋙ F).

Equations

• h.isoColimit = CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso h (CategoryTheory.Limits.colimit.isColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F))

@[simp]

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) [Limits.HasColimit ((CostructuredArrow.proj L Y).comp F)] (g : CostructuredArrow L Y) : CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj L Y).comp F) g) h.isoColimit.inv = CategoryStruct.comp (E.hom.app g.left) (E.right.map g.hom)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_inv_assoc {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) [Limits.HasColimit ((CostructuredArrow.proj L Y).comp F)] (g : CostructuredArrow L Y) {Z : H} (h✝ : E.right.obj Y ⟶ Z) : CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj L Y).comp F) g) (CategoryStruct.comp h.isoColimit.inv h✝) = CategoryStruct.comp (E.hom.app g.left) (CategoryStruct.comp (E.right.map g.hom) h✝)

@[simp]

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) [Limits.HasColimit ((CostructuredArrow.proj L Y).comp F)] (g : CostructuredArrow L Y) : CategoryStruct.comp (E.hom.app g.left) (CategoryStruct.comp (E.right.map g.hom) h.isoColimit.hom) = Limits.colimit.ι ((CostructuredArrow.proj L Y).comp F) g

@[simp]

theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom_assoc {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) [Limits.HasColimit ((CostructuredArrow.proj L Y).comp F)] (g : CostructuredArrow L Y) {Z : H} (h✝ : Limits.colimit ((CostructuredArrow.proj L Y).comp F) ⟶ Z) : CategoryStruct.comp (E.hom.app g.left) (CategoryStruct.comp (E.right.map g.hom) (CategoryStruct.comp h.isoColimit.hom h✝)) = CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj L Y).comp F) g) h✝

@[reducible, inline]

abbrev CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) {G : L.LeftExtension F} {f₁ f₂ : E ⟶ G} : f₁ = f₂

def CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isUniversal {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) : 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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.LeftExtension F} (h : E.IsPointwiseLeftKanExtension) [L.Full] [L.Faithful] : IsIso E.hom

def CategoryTheory.Functor.RightExtension.coneAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} (E : L.RightExtension F) (Y : D) : Limits.Cone ((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.coneAt_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} (E : L.RightExtension F) (Y : D) (g : StructuredArrow Y L) : (E.coneAt Y).π.app g = CategoryStruct.comp (E.left.map g.hom) (E.hom.app g.right)

def CategoryTheory.Functor.RightExtension.coneAtFunctor {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (Y : D) : Functor (L.RightExtension F) (Limits.Cone ((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.

@[simp]

theorem CategoryTheory.Functor.RightExtension.coneAtFunctor_obj {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (Y : D) (E : L.RightExtension F) : (coneAtFunctor L F Y).obj E = E.coneAt Y

@[simp]

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

def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} (E : L.RightExtension F) {X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] : IsIso (E.hom.app X)

noncomputable def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [Limits.HasLimit ((StructuredArrow.proj Y L).comp F)] : E.left.obj Y ≅ Limits.limit ((StructuredArrow.proj Y L).comp F)

A pointwise right Kan extension of F along L applied to an object Y is isomorphic to limit (StructuredArrow.proj Y L ⋙ F).

Equations

• h.isoLimit = CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso h (CategoryTheory.Limits.limit.isLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F))

@[simp]

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [Limits.HasLimit ((StructuredArrow.proj Y L).comp F)] (g : StructuredArrow Y L) : CategoryStruct.comp h.isoLimit.hom (Limits.limit.π ((StructuredArrow.proj Y L).comp F) g) = CategoryStruct.comp (E.left.map g.hom) (E.hom.app g.right)

@[simp]

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_hom_π_assoc {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [Limits.HasLimit ((StructuredArrow.proj Y L).comp F)] (g : StructuredArrow Y L) {Z : H} (h✝ : F.obj ((StructuredArrow.proj Y L).obj g) ⟶ Z) : CategoryStruct.comp h.isoLimit.hom (CategoryStruct.comp (Limits.limit.π ((StructuredArrow.proj Y L).comp F) g) h✝) = CategoryStruct.comp (E.left.map g.hom) (CategoryStruct.comp (E.hom.app g.right) h✝)

@[simp]

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [Limits.HasLimit ((StructuredArrow.proj Y L).comp F)] (g : StructuredArrow Y L) : CategoryStruct.comp h.isoLimit.inv (CategoryStruct.comp (E.left.map g.hom) (E.hom.app g.right)) = Limits.limit.π ((StructuredArrow.proj Y L).comp F) g

@[simp]

theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit_inv_π_assoc {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) [Limits.HasLimit ((StructuredArrow.proj Y L).comp F)] (g : StructuredArrow Y L) {Z : H} (h✝ : ((fromPUnit F).obj E.right).obj g.right ⟶ Z) : CategoryStruct.comp h.isoLimit.inv (CategoryStruct.comp (E.left.map g.hom) (CategoryStruct.comp (E.hom.app g.right) h✝)) = CategoryStruct.comp (Limits.limit.π ((StructuredArrow.proj Y L).comp F) g) h✝

@[reducible, inline]

abbrev CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} (h : E.IsPointwiseRightKanExtension) {G : L.RightExtension F} {f₁ f₂ : G ⟶ E} : f₁ = f₂

def CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isUniversal {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} (h : E.IsPointwiseRightKanExtension) : 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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] {L : Functor C D} {F : 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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} {E : L.RightExtension F} (h : E.IsPointwiseRightKanExtension) [L.Full] [L.Faithful] : IsIso E.hom

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

@[simp]

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

noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtensionUnit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : 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.

@[simp]

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

noncomputable def CategoryTheory.Functor.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseLeftKanExtension F] : (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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseLeftKanExtension F] : StructuredArrow.IsUniversal (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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseLeftKanExtension F] : (L.pointwiseLeftKanExtension F).IsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F)

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

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

An auxiliary cocone used in the lemma pointwiseLeftKanExtension_desc_app

Equations

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

@[simp]

theorem CategoryTheory.Functor.costructuredArrowMapCocone_ι_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (G : Functor D H) (α : F ⟶ L.comp G) (Y : D) (f : CostructuredArrow L Y) : (L.costructuredArrowMapCocone F G α Y).ι.app f = CategoryStruct.comp (α.app f.left) (G.map f.hom)

@[simp]

theorem CategoryTheory.Functor.costructuredArrowMapCocone_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (G : Functor D H) (α : F ⟶ L.comp G) (Y : D) : (L.costructuredArrowMapCocone F G α Y).pt = G.obj Y

@[simp]

theorem CategoryTheory.Functor.pointwiseLeftKanExtension_desc_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] [Category.{u_5, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseLeftKanExtension F] (G : Functor D H) (α : F ⟶ L.comp G) (Y : D) : ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y = Limits.colimit.desc ((CostructuredArrow.proj L Y).comp F) (L.costructuredArrowMapCocone F G α Y)

noncomputable def CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} [L.HasPointwiseLeftKanExtension F] (F' : Functor D H) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] : (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.

noncomputable def CategoryTheory.Functor.pointwiseRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] : 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.pointwiseRightKanExtension_obj {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] (Y : D) : (L.pointwiseRightKanExtension F).obj Y = Limits.limit ((StructuredArrow.proj Y L).comp F)

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtension_map {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] {Y₁ Y₂ : D} (f : Y₁ ⟶ Y₂) : (L.pointwiseRightKanExtension F).map f = Limits.limit.lift ((StructuredArrow.proj Y₂ L).comp F) { pt := Limits.limit ((StructuredArrow.proj Y₁ L).comp F), π := { app := fun (g : StructuredArrow Y₂ L) => Limits.limit.π ((StructuredArrow.proj Y₁ L).comp F) ((StructuredArrow.map f).obj g), naturality := ⋯ } }

noncomputable def CategoryTheory.Functor.pointwiseRightKanExtensionCounit {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : 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.

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtensionCounit_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] (X : C) : (L.pointwiseRightKanExtensionCounit F).app X = Limits.limit.π ((StructuredArrow.proj (L.obj X) L).comp F) (StructuredArrow.mk (CategoryStruct.id (L.obj X)))

noncomputable def CategoryTheory.Functor.pointwiseRightKanExtensionIsPointwiseRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] : (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} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] : CostructuredArrow.IsUniversal (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} [Category.{u_4, u_1} C] [Category.{u_6, u_2} D] [Category.{u_5, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] : (L.pointwiseRightKanExtension F).IsRightKanExtension (L.pointwiseRightKanExtensionCounit F)

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

def CategoryTheory.Functor.structuredArrowMapCone {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (G : Functor D H) (α : L.comp G ⟶ F) (Y : D) : Limits.Cone ((StructuredArrow.proj Y L).comp F)

An auxiliary cocone used in the lemma pointwiseRightKanExtension_lift_app

Equations

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

@[simp]

theorem CategoryTheory.Functor.structuredArrowMapCone_pt {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (G : Functor D H) (α : L.comp G ⟶ F) (Y : D) : (L.structuredArrowMapCone F G α Y).pt = G.obj Y

@[simp]

theorem CategoryTheory.Functor.structuredArrowMapCone_π_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] (L : Functor C D) (F : Functor C H) (G : Functor D H) (α : L.comp G ⟶ F) (Y : D) (f : StructuredArrow Y L) : (L.structuredArrowMapCone F G α Y).π.app f = CategoryStruct.comp (G.map f.hom) (α.app f.right)

@[simp]

theorem CategoryTheory.Functor.pointwiseRightKanExtension_lift_app {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_6, u_1} C] [Category.{u_4, u_2} D] [Category.{u_5, u_3} H] (L : Functor C D) (F : Functor C H) [L.HasPointwiseRightKanExtension F] (G : Functor D H) (α : L.comp G ⟶ F) (Y : D) : ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y = Limits.limit.lift ((StructuredArrow.proj Y L).comp F) (L.structuredArrowMapCone F G α Y)

noncomputable def CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsRightKanExtension {C : Type u_1} {D : Type u_2} {H : Type u_3} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] [Category.{u_6, u_3} H] {L : Functor C D} {F : Functor C H} [L.HasPointwiseRightKanExtension F] (F' : Functor D H) (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] : (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.