Preservation of Kan extensions #
Given functors F : A ⥤ B
, L : B ⥤ C
, and G : B ⥤ D
,
we introduce a typeclass G.PreservesLeftKanExtension F L
which encodes the fact that
the left Kan extension of F
along L
is preserved by the functor G
.
When the Kan extension is pointwise, it suffices that G
preserves (co)limits of the relevant
diagrams.
We introduce the dual typeclass G.PreservesRightKanExtension
.
G.PreservesLeftKanExtension F L
asserts that G
preserves all left Kan extensions
of F
along L
. See PreservesLeftKanExtension.mk_of_preserves_isLeftKanExtension
for a
constructor taking a single left Kan extension as input.
- preserves (F' : Functor C B) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] : (F'.comp G).IsLeftKanExtension (CategoryStruct.comp (whiskerRight α G) (L.associator F' G).hom)
Instances
Alternative constructor for PreservesLeftKanExtension
, phrased in terms of
LeftExtension.IsUniversal
instead. See PreservesLeftKanExtension.mk_of_preserves_isUniversal
for a similar constructor taking as input a single LeftExtension
.
Show that G
preserves left Kan extensions if it maps some left Kan extension to a left
Kan extension.
Show that G
preserves left Kan extensions if it maps some left Kan extension to a left
Kan extension, phrased in terms of IsUniversal
.
G.PreservesLeftKanExtensionAt F L c
asserts that G
preserves all pointwise left Kan
extensions of F
along L
at the point c
.
- preserves (E : L.LeftExtension F) : ∀ (a : E.IsPointwiseLeftKanExtensionAt c), Nonempty (((LeftExtension.postcompose₂ L F G).obj E).IsPointwiseLeftKanExtensionAt c)
G
preserves every pointwise extensions ofF
alongL
atc
.
Instances
G.PreservesLeftKanExtension F L
asserts that G
preserves all pointwise left Kan extensions
of F
along L
.
Equations
- G.PreservesPointwiseLeftKanExtension F L = ∀ (c : C), G.PreservesPointwiseLeftKanExtensionAt F L c
Instances For
Given a pointwise left Kan extension of F
along L
at c
, exhibits
(LeftExtension.whiskerRight L F G).obj E
as a pointwise left Kan extension of F ⋙ G
along
L
at c
.
Equations
Instances For
Given a pointwise left Kan extension of F
along L
, exhibits
(LeftExtension.whiskerRight L F G).obj E
as a pointwise left Kan extension of F ⋙ G
along
L
.
Equations
Instances For
The cocone at a point of the whiskering right by G
of an extension is isomorphic to the
action of G
on the cocone at that point for the original extension.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If G
preserves any pointwise left Kan extension of F
along L
at c
, then it preserves
all of them.
Extract an isomorphism (leftKanExtension L F) ⋙ G ≅ leftKanExtension L (F ⋙ G)
when G
preserves left Kan extensions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functor that preserves the colimit of CostructuredArrow.proj L c ⋙ F
preserves
the pointwise left Kan extension of F
along L
at c
.
If there is a pointwise left Kan extension of F
along L
, and if G
preserves them,
then G
preserves left Kan extensions of F
along L
.
Extract an isomorphism
(pointwiseLeftKanExtension L F) ⋙ G ≅ pointwiseLeftKanExtension L (F ⋙ G)
when G
preserves
left Kan extensions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
G.PreservesLeftKanExtensions L
means that G : B ⥤ D
preserves all left Kan extensions along
L : A ⥤ C
of every functor A ⥤ B
.
Equations
- G.PreservesLeftKanExtensions L = ∀ (F : CategoryTheory.Functor A B), G.PreservesLeftKanExtension F L
Instances For
G.PreservesPointwiseLeftKanExtensions L
means that G : B ⥤ D
preserves all pointwise left
Kan extensions along L : A ⥤ C
of every functor A ⥤ B
.
Equations
- G.PreservesPointwiseLeftKanExtensions L = ∀ (F : CategoryTheory.Functor A B), G.PreservesPointwiseLeftKanExtension F L
Instances For
Commuting a functor that preserves left Kan extensions with the lan
functor.
Equations
- G.lanCompIsoOfPreserves L = CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor A B) => G.leftKanExtensionCompIsoOfPreserves F L) ⋯
Instances For
G.PreservesRightKanExtension F L
asserts that G
preserves all right Kan extensions
of F
along L
. See PreservesRightKanExtension.mk_of_preserves_isRightKanExtension
for a
constructor taking a single right Kan extension as input.
- preserves (F' : Functor C B) (α : L.comp F' ⟶ F) [F'.IsRightKanExtension α] : (F'.comp G).IsRightKanExtension (CategoryStruct.comp (L.associator F' G).inv (whiskerRight α G))
Instances
Alternative constructor for PreservesRightKanExtension
, phrased in terms of
RightExtension.IsUniversal
instead. See PreservesRightKanExtension.mk_of_preserves_isUniversal
for a similar constructor taking as input a single RightExtension
.
Show that G
preserves right Kan extensions if it maps some right Kan extension to a right
Kan extension.
Show that G
preserves right Kan extensions if it maps some right Kan extension to a left
Kan extension, phrased in terms of IsUniversal
.
G.PreservesRightKanExtensionAt F L c
asserts that G
preserves all right pointwise right Kan
extensions of F
along L
at c
.
- preserves (E : L.RightExtension F) : ∀ (a : E.IsPointwiseRightKanExtensionAt c), Nonempty (((RightExtension.postcompose₂ L F G).obj E).IsPointwiseRightKanExtensionAt c)
G
preserves every pointwise extensions ofF
alongL
atc
.
Instances
G.PreservesRightKanExtensions L
asserts that G
preserves all pointwise right Kan
extensions of F
along L
for every F
.
Equations
- G.PreservesPointwiseRightKanExtension F L = ∀ (c : C), G.PreservesPointwiseRightKanExtensionAt F L c
Instances For
Given a pointwise right Kan extension of F
along L
at c
, exhibits
(RightExtension.whiskerRight L F G).obj E
as a pointwise right Kan extension of F ⋙ G
along
L
at c
.
Equations
Instances For
Given a pointwise right Kan extension of F
along L
, exhibits
(RightExtension.whiskerRight L F G).obj E
as a pointwise right Kan extension of F ⋙ G
at L
.
Equations
Instances For
The cone at a point of the whiskering right by G
of an extension is isomorphic to the
action of G
on the cone at that point for the original extension.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If G
preserves any pointwise right Kan extension of F
along L
at c
, then it preserves
all of them.
Extract an isomorphism rightKanExtension L F ⋙ G ≅ rightKanExtension L (F ⋙ G)
when G
preserves right Kan extensions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functor that preserves the limit of (StructuredArrow.proj L c ⋙ F)
preserves
the pointwise right Kan extension of F
along L
at c.
If there is a pointwise right Kan extension of F
along L
, and if G
preserves them,
then G
preserves right Kan extensions of F
along L
.
Extract an isomorphism
L.pointwiseRightKanExtension F ⋙ G ≅ L.pointwiseRightKanExtension (F ⋙ G)
when G
preserves
right Kan extensions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
G.PreservesRightKanExtensions L
means that G : B ⥤ D
preserves all right Kan extensions
along L : A ⥤ C
of every functor A ⥤ B
.
Equations
- G.PreservesRightKanExtensions L = ∀ (F : CategoryTheory.Functor A B), G.PreservesRightKanExtension F L
Instances For
G.PreservesPointwiseRightKanExtensions L
means that G : B ⥤ D
preserves all pointwise right
Kan extensions along L : A ⥤ C
of every functor A ⥤ B
.
Equations
- G.PreservesPointwiseRightKanExtensions L = ∀ (F : CategoryTheory.Functor A B), G.PreservesPointwiseRightKanExtension F L
Instances For
Commuting a functor that preserves right Kan extensions with the ran
functor.
Equations
- G.ranCompIsoOfPreserves L = CategoryTheory.NatIso.ofComponents (fun (F : CategoryTheory.Functor A B) => G.rightKanExtensionCompIsoOfPreserves F L) ⋯