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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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.