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
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)
Instances For
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
Instances For
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)
Instances For
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
Instances For
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.
Instances For
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.
Instances For
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)
Instances For
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)
Instances For
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.
Instances For
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.
Instances For
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 := ⋯ } ⋯
Instances For
A pointwise left Kan extension is universal, i.e. it is a left Kan extension.
Equations
- h.isUniversal = CategoryTheory.Limits.IsInitial.ofUniqueHom h.homFrom ⋯
Instances For
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.
Instances For
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.
Instances For
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)
Instances For
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)
Instances For
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.
Instances For
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.
Instances For
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 := ⋯ } ⋯
Instances For
A pointwise right Kan extension is universal, i.e. it is a right Kan extension.
Equations
- h.isUniversal = CategoryTheory.Limits.IsTerminal.ofUniqueHom h.homTo ⋯
Instances For
The constructed pointwise left Kan extension when HasPointwiseLeftKanExtension L F
holds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
The functor pointwiseLeftKanExtension L F
is a left Kan extension of F
along L
.
Equations
- L.pointwiseLeftKanExtensionIsUniversal F = (L.pointwiseLeftKanExtensionIsPointwiseLeftKanExtension F).isUniversal
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
An auxiliary cocone used in the lemma pointwiseLeftKanExtension_desc_app
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
The constructed pointwise right Kan extension
when HasPointwiseRightKanExtension L F
holds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
The functor pointwiseRightKanExtension L F
is a right Kan extension of F
along L
.
Equations
- L.pointwiseRightKanExtensionIsUniversal F = (L.pointwiseRightKanExtensionIsPointwiseRightKanExtension F).isUniversal
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
An auxiliary cocone used in the lemma pointwiseRightKanExtension_lift_app
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.