Guitart exact squares and Kan extensions #
Given a Guitart exact square w : T ⋙ R ⟶ L ⋙ B,
T
C₁ ⥤ C₂
L | | R
v v
C₃ ⥤ C₄
B
we show that an extension F' : C₄ ⥤ D of F : C₂ ⥤ D along R
is a pointwise left Kan extension at B.obj X₃ iff
the composition T ⋙ F' is a pointwise left Kan extension at X₃
of B ⋙ F'.
Given a square w : TwoSquare T L R B (consisting of a natural transformation
T ⋙ R ⟶ L ⋙ B), this is the obvious map R.LeftExtension F → L.LeftExtension (T ⋙ F)
obtained by the precomposition with B and the postcomposition with w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If w : TwoSquare T L R B is a Guitart exact square, and E is a left extension
of F along R, then E is a pointwise left Kan extension of F along R at
B.obj X₃ iff E.compTwoSquare w is a pointwise left Kan extension
of T ⋙ F along L at X₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If w : TwoSquare T L R B is a Guitart exact square, and E is a pointwise
left Kan extension of F along R, then E.compTwoSquare w is a pointwise left
Kan extension of T ⋙ F along L.
Equations
- h.compTwoSquare w X₃ = (E.isPointwiseLeftKanExtensionAtCompTwoSquareEquiv w X₃).symm (h (B.obj X₃))
Instances For
If w : TwoSquare T L R B is a Guitart exact square, with B essentially surjective,
and E is a left extension of F along R, then E is a pointwise
left Kan extension of F along R provided E.compTwoSquare w is a pointwise left
Kan extension of T ⋙ F along L.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If w : TwoSquare T L R B is a Guitart exact square, with B essentially surjective,
and E is a left extension of F along R, then E is a pointwise left Kan extension
of F along R iff E.compTwoSquare w is a pointwise left Kan extension
of T ⋙ F along L.
Equations
- One or more equations did not get rendered due to their size.