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'.
When suitable (pointwise) left Kan extensions exist, we also show that
the natural transformation of functors (C₂ ⥤ D) ⥤ C₃ ⥤ D
(whiskeringLeft C₁ C₂ D).obj T ⋙ L.lan ⟶ R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B
induced by a Guitart exact square w is an isomorphism.
References #
- https://ncatlab.org/nlab/show/exact+square
@[reducible, inline]
abbrev
CategoryTheory.Functor.LeftExtension.compTwoSquare
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{F : Functor C₂ D}
(E : R.LeftExtension F)
(w : TwoSquare T L R B)
:
L.LeftExtension (T.comp 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
Instances For
noncomputable def
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionAtCompTwoSquareEquiv
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{F : Functor C₂ D}
(E : R.LeftExtension F)
(w : TwoSquare T L R B)
(X₃ : C₃)
[(w.costructuredArrowRightwards X₃).Final]
:
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
Instances For
theorem
CategoryTheory.Functor.LeftExtension.nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{F : Functor C₂ D}
(E : R.LeftExtension F)
(w : TwoSquare T L R B)
(X₃ : C₃)
[(w.costructuredArrowRightwards X₃).Final]
:
Nonempty ((E.compTwoSquare w).IsPointwiseLeftKanExtensionAt X₃) ↔ Nonempty (E.IsPointwiseLeftKanExtensionAt (B.obj X₃))
noncomputable def
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.compTwoSquare
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{F : Functor C₂ D}
{E : R.LeftExtension F}
(h : E.IsPointwiseLeftKanExtension)
(w : TwoSquare T L R B)
[w.GuitartExact]
:
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
Instances For
noncomputable def
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionOfCompTwoSquare
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{F : Functor C₂ D}
(E : R.LeftExtension F)
(w : TwoSquare T L R B)
[w.GuitartExact]
[B.EssSurj]
(h : (E.compTwoSquare w).IsPointwiseLeftKanExtension)
:
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
Instances For
noncomputable def
CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionEquivOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{F : Functor C₂ D}
(E : R.LeftExtension F)
(w : TwoSquare T L R B)
[w.GuitartExact]
[B.EssSurj]
:
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
Instances For
theorem
CategoryTheory.TwoSquare.hasPointwiseLeftKanExtensionAt_iff
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
(F : Functor C₂ D)
(X₃ : C₃)
[(w.costructuredArrowRightwards X₃).Final]
:
theorem
CategoryTheory.TwoSquare.hasPointwiseLeftKanExtension_iff
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[w.GuitartExact]
[B.EssSurj]
(F : Functor C₂ D)
:
theorem
CategoryTheory.TwoSquare.hasPointwiseLeftKanExtension
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[w.GuitartExact]
(F : Functor C₂ D)
[R.HasPointwiseLeftKanExtension F]
:
L.HasPointwiseLeftKanExtension (T.comp F)
theorem
CategoryTheory.TwoSquare.hasLeftKanExtension
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[w.GuitartExact]
(F : Functor C₂ D)
[R.HasPointwiseLeftKanExtension F]
:
L.HasLeftKanExtension (T.comp F)
noncomputable def
CategoryTheory.TwoSquare.lanBaseChange
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[∀ (F : Functor C₁ D), L.HasLeftKanExtension F]
[∀ (F : Functor C₂ D), R.HasLeftKanExtension F]
:
((Functor.whiskeringLeft C₁ C₂ D).obj T).comp L.lan ⟶ R.lan.comp ((Functor.whiskeringLeft C₃ C₄ D).obj B)
The base change natural transformation for left Kan extensions associated to a 2-square.
Equations
Instances For
theorem
CategoryTheory.TwoSquare.lanBaseChange_app
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[∀ (F : Functor C₁ D), L.HasLeftKanExtension F]
[∀ (F : Functor C₂ D), R.HasLeftKanExtension F]
(F : Functor C₂ D)
:
w.lanBaseChange.app F = ((L.lanAdjunction D).homEquiv (((Functor.whiskeringLeft C₁ C₂ D).obj T).obj F)
((R.lan.comp ((Functor.whiskeringLeft C₃ C₄ D).obj B)).obj F)).symm
((Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w).hom
theorem
CategoryTheory.TwoSquare.isIso_lanBaseChange_app_iff
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[∀ (F : Functor C₁ D), L.HasLeftKanExtension F]
[∀ (F : Functor C₂ D), R.HasLeftKanExtension F]
(F : Functor C₂ D)
:
IsIso (w.lanBaseChange.app F) ↔ ((Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w).right.IsLeftKanExtension
((Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w).hom
instance
CategoryTheory.TwoSquare.isIso_lanBaseChange_app
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[∀ (F : Functor C₁ D), L.HasLeftKanExtension F]
[∀ (F : Functor C₂ D), R.HasLeftKanExtension F]
(F : Functor C₂ D)
[R.HasPointwiseLeftKanExtension F]
[w.GuitartExact]
:
IsIso (w.lanBaseChange.app F)
instance
CategoryTheory.TwoSquare.instIsIsoFunctorLanBaseChangeOfGuitartExact
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
{D : Type u₅}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
[Category.{v₅, u₅} D]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
(w : TwoSquare T L R B)
[∀ (F : Functor C₁ D), L.HasLeftKanExtension F]
[∀ (F : Functor C₂ D), R.HasPointwiseLeftKanExtension F]
[w.GuitartExact]
: