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.
The dual results for right Kan extensions are also obtained.
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 T and the postcomposition with w.
Equations
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
- h.compTwoSquare w X₃ = (E.isPointwiseLeftKanExtensionAtCompTwoSquareEquiv w X₃).symm (h (B.obj X₃))
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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Functor.RightExtension.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 : B.RightExtension F)
(w : TwoSquare T L R B)
:
T.RightExtension (L.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 B.RightExtension F → T.RightExtension (L ⋙ F)
obtained by the precomposition with L and the postcomposition with w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtCompTwoSquareEquiv
{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 : B.RightExtension F)
(w : TwoSquare T L R B)
(X₂ : C₂)
[(w.structuredArrowDownwards X₂).Initial]
:
If w : TwoSquare T L R B is a Guitart exact square, and E is a right extension
of F along B, then E is a pointwise right Kan extension of F along B at
R.obj X₃ iff E.compTwoSquare w is a pointwise right Kan extension
of L ⋙ F along T at X₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.RightExtension.nonempty_isPointwiseRightKanExtensionAt_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 : B.RightExtension F)
(w : TwoSquare T L R B)
(X₂ : C₂)
[(w.structuredArrowDownwards X₂).Initial]
:
Nonempty ((E.compTwoSquare w).IsPointwiseRightKanExtensionAt X₂) ↔ Nonempty (E.IsPointwiseRightKanExtensionAt (R.obj X₂))
noncomputable def
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.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 : B.RightExtension F}
(h : E.IsPointwiseRightKanExtension)
(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
right Kan extension of F along B, then E.compTwoSquare w is a pointwise right
Kan extension of L ⋙ F along T.
Equations
- h.compTwoSquare w X₂ = (E.isPointwiseRightKanExtensionAtCompTwoSquareEquiv w X₂).symm (h (R.obj X₂))
Instances For
noncomputable def
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionOfCompTwoSquare
{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 : B.RightExtension F)
(w : TwoSquare T L R B)
[w.GuitartExact]
[R.EssSurj]
(h : (E.compTwoSquare w).IsPointwiseRightKanExtension)
:
If w : TwoSquare T L R B is a Guitart exact square, with R essentially surjective,
and E is a right extension of F along B, then E is a pointwise
right Kan extension of F along R provided E.compTwoSquare w is a pointwise right
Kan extension of L ⋙ F along T.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionEquivOfGuitartExact
{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 : B.RightExtension F)
(w : TwoSquare T L R B)
[w.GuitartExact]
[R.EssSurj]
:
If w : TwoSquare T L R B is a Guitart exact square, with R essentially surjective,
and E is a right extension of F along B, then E is a pointwise right Kan extension
of F along B iff E.compTwoSquare w is a pointwise right Kan extension
of L ⋙ F along T.
Equations
- One or more equations did not get rendered due to their size.
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)
theorem
CategoryTheory.TwoSquare.hasPointwiseRightKanExtensionAt_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.structuredArrowDownwards X₂).Initial]
:
theorem
CategoryTheory.TwoSquare.hasPointwiseRightKanExtension_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]
[R.EssSurj]
(F : Functor C₃ D)
:
theorem
CategoryTheory.TwoSquare.hasPointwiseRightKanExtension
{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)
[B.HasPointwiseRightKanExtension F]
:
T.HasPointwiseRightKanExtension (L.comp F)
theorem
CategoryTheory.TwoSquare.hasRightKanExtension
{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)
[B.HasPointwiseRightKanExtension F]
:
T.HasRightKanExtension (L.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
- One or more equations did not get rendered due to their size.
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
(StructuredArrow.hom ((Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))
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) ↔ (StructuredArrow.right
((Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w)).IsLeftKanExtension
(StructuredArrow.hom ((Functor.LeftExtension.mk (R.lan.obj F) (R.lanUnit.app F)).compTwoSquare w))
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]
:
noncomputable def
CategoryTheory.TwoSquare.ranBaseChange
{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), T.HasRightKanExtension F]
[∀ (F : Functor C₃ D), B.HasRightKanExtension F]
:
B.ran.comp ((Functor.whiskeringLeft C₂ C₄ D).obj R) ⟶ ((Functor.whiskeringLeft C₁ C₃ D).obj L).comp T.ran
The base change natural transformation for left Kan extensions associated to a 2-square.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.TwoSquare.ranBaseChange_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), T.HasRightKanExtension F]
[∀ (F : Functor C₃ D), B.HasRightKanExtension F]
(F : Functor C₃ D)
:
w.ranBaseChange.app F = ((T.ranAdjunction D).homEquiv ((B.ran.comp ((Functor.whiskeringLeft C₂ C₄ D).obj R)).obj F)
(((Functor.whiskeringLeft C₁ C₃ D).obj L).obj F))
(CostructuredArrow.hom ((Functor.RightExtension.mk (B.ran.obj F) (B.ranCounit.app F)).compTwoSquare w))
theorem
CategoryTheory.TwoSquare.isIso_ranBaseChange_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), T.HasRightKanExtension F]
[∀ (F : Functor C₃ D), B.HasRightKanExtension F]
(F : Functor C₃ D)
:
IsIso (w.ranBaseChange.app F) ↔ (CostructuredArrow.left
((Functor.RightExtension.mk (B.ran.obj F) (B.ranCounit.app F)).compTwoSquare w)).IsRightKanExtension
(CostructuredArrow.hom ((Functor.RightExtension.mk (B.ran.obj F) (B.ranCounit.app F)).compTwoSquare w))
instance
CategoryTheory.TwoSquare.isIso_ranBaseChange_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), T.HasRightKanExtension F]
[∀ (F : Functor C₃ D), B.HasRightKanExtension F]
(F : Functor C₃ D)
[B.HasPointwiseRightKanExtension F]
[w.GuitartExact]
:
IsIso (w.ranBaseChange.app F)
instance
CategoryTheory.TwoSquare.instIsIsoFunctorRanBaseChangeOfGuitartExact
{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), T.HasRightKanExtension F]
[∀ (F : Functor C₃ D), B.HasPointwiseRightKanExtension F]
[w.GuitartExact]
: