Skip to content

feat(CategoryTheory): right Kan extensions and Guitart exact squares #43063

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
joelriou wants to merge 5 commits into
base: master
Choose a base branch
from
Open

feat(CategoryTheory): right Kan extensions and Guitart exact squares #43063

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
5c2c29c
feat(CategoryTheory): Guitart exact squares and right Kan extensions
joelriou Aug 23, 2026
0ff177f
Update Mathlib/CategoryTheory/GuitartExact/KanExtension.lean
joelriou Aug 29, 2026
c3ed253
Update Mathlib/CategoryTheory/GuitartExact/KanExtension.lean
joelriou Aug 29, 2026
b43db4a
remove some set_option
joelriou Aug 29, 2026
a1d55d6
Merge remote-tracking branch 'origin/master' into derivability-struct…
joelriou Aug 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
148 changes: 142 additions & 6 deletions Mathlib/CategoryTheory/GuitartExact/KanExtension.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,8 @@ 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
Expand All @@ -55,10 +57,10 @@ variable {T : C₁ ⥤ C₂} {L : C₁ ⥤ C₃} {R : C₂ ⥤ C₄} {B : C₃

/-- 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`. -/
obtained by the precomposition with `T` and the postcomposition with `w`. -/
abbrev compTwoSquare (w : TwoSquare T L R B) : L.LeftExtension (T ⋙ F) :=
LeftExtension.mk (B ⋙ E.right)
(whiskerLeft _ E.hom ≫ (associator _ _ _).inv ≫
(whiskerLeft T E.hom ≫ (associator _ _ _).inv ≫
whiskerRight w.natTrans _ ≫ (associator _ _ _).hom)

set_option backward.isDefEq.respectTransparency.types false in
Expand Down Expand Up @@ -116,6 +118,74 @@ noncomputable def isPointwiseLeftKanExtensionEquivOfGuitartExact

end Functor.LeftExtension

namespace Functor.RightExtension

variable {T : C₁ ⥤ C₂} {L : C₁ ⥤ C₃} {R : C₂ ⥤ C₄} {B : C₃ ⥤ C₄}
{F : C₃ ⥤ D} (E : B.RightExtension 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`. -/
abbrev compTwoSquare (w : TwoSquare T L R B) : T.RightExtension (L ⋙ F) :=
RightExtension.mk (R ⋙ E.left)
((associator _ _ _).inv ≫ whiskerRight w.natTrans _ ≫
(associator _ _ _).hom ≫ whiskerLeft L E.hom)

set_option backward.defeqAttrib.useBackward true in
set_option backward.isDefEq.respectTransparency.types false in
/-- 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₃`. -/
noncomputable def isPointwiseRightKanExtensionAtCompTwoSquareEquiv
(w : TwoSquare T L R B) (X₂ : C₂) [Initial (w.structuredArrowDownwards X₂)] :
(E.compTwoSquare w).IsPointwiseRightKanExtensionAt X₂ ≃
E.IsPointwiseRightKanExtensionAt (R.obj X₂) := by
refine Equiv.trans ?_ (Initial.isLimitWhiskerEquiv (w.structuredArrowDownwards X₂) _)
exact IsLimit.equivIsoLimit (Cone.ext (Iso.refl _))

lemma nonempty_isPointwiseRightKanExtensionAt_compTwoSquare_iff
(w : TwoSquare T L R B) (X₂ : C₂) [Initial (w.structuredArrowDownwards X₂)] :
Nonempty ((E.compTwoSquare w).IsPointwiseRightKanExtensionAt X₂) ↔
Nonempty (E.IsPointwiseRightKanExtensionAt (R.obj X₂)) :=
(E.isPointwiseRightKanExtensionAtCompTwoSquareEquiv w _).nonempty_congr

variable {E} in
/-- 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`. -/
noncomputable def IsPointwiseRightKanExtension.compTwoSquare
(h : E.IsPointwiseRightKanExtension) (w : TwoSquare T L R B) [w.GuitartExact] :
(E.compTwoSquare w).IsPointwiseRightKanExtension :=
fun X₂ ↦ (E.isPointwiseRightKanExtensionAtCompTwoSquareEquiv w X₂).symm (h _)

/-- 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`. -/
noncomputable def isPointwiseRightKanExtensionOfCompTwoSquare
(w : TwoSquare T L R B) [w.GuitartExact] [R.EssSurj]
(h : (E.compTwoSquare w).IsPointwiseRightKanExtension) :
E.IsPointwiseRightKanExtension :=
fun X₄ ↦ E.isPointwiseRightKanExtensionAtOfIso'
(E.isPointwiseRightKanExtensionAtCompTwoSquareEquiv w _ (h (R.objPreimage X₄)))
(R.objObjPreimageIso X₄)

/-- 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`. -/
noncomputable def isPointwiseRightKanExtensionEquivOfGuitartExact
(w : TwoSquare T L R B) [w.GuitartExact] [R.EssSurj] :
(E.compTwoSquare w).IsPointwiseRightKanExtension ≃
E.IsPointwiseRightKanExtension where
toFun h := E.isPointwiseRightKanExtensionOfCompTwoSquare w h
invFun h := h.compTwoSquare w
left_inv _ := by subsingleton
right_inv _ := by subsingleton

end Functor.RightExtension

namespace TwoSquare

variable {T : C₁ ⥤ C₂} {L : C₁ ⥤ C₃} {R : C₂ ⥤ C₄} {B : C₃ ⥤ C₄}
Expand Down Expand Up @@ -152,6 +222,35 @@ lemma hasLeftKanExtension [w.GuitartExact]
have := w.hasPointwiseLeftKanExtension F
infer_instance

lemma hasPointwiseRightKanExtensionAt_iff
(F : C₃ ⥤ D) (X₂ : C₂) [(w.structuredArrowDownwards X₂).Initial] :
T.HasPointwiseRightKanExtensionAt (L ⋙ F) X₂ ↔
B.HasPointwiseRightKanExtensionAt F (R.obj X₂) := by
dsimp [Functor.HasPointwiseRightKanExtensionAt]
rw [← Functor.Initial.hasLimit_comp_iff (w.structuredArrowDownwards X₂)]
rfl

lemma hasPointwiseRightKanExtension_iff [w.GuitartExact] [R.EssSurj] (F : C₃ ⥤ D) :
T.HasPointwiseRightKanExtension (L ⋙ F) ↔
B.HasPointwiseRightKanExtension F := by
dsimp [Functor.HasPointwiseRightKanExtension]
simp only [hasPointwiseRightKanExtensionAt_iff w]
refine ⟨fun h X₄ ↦ ?_, fun h _ ↦ h _⟩
rw [← Functor.hasPointwiseRightKanExtensionAt_iff_of_iso _ _ (R.objObjPreimageIso X₄)]
apply h

lemma hasPointwiseRightKanExtension [w.GuitartExact]
(F : C₃ ⥤ D) [B.HasPointwiseRightKanExtension F] :
T.HasPointwiseRightKanExtension (L ⋙ F) :=
((B.pointwiseRightKanExtensionIsPointwiseRightKanExtension
F).compTwoSquare w).hasPointwiseRightKanExtension

lemma hasRightKanExtension [w.GuitartExact]
(F : C₃ ⥤ D) [B.HasPointwiseRightKanExtension F] :
T.HasRightKanExtension (L ⋙ F) := by
have := w.hasPointwiseRightKanExtension F
infer_instance

section

open CategoryTheory.Functor
Expand All @@ -160,7 +259,6 @@ section

variable [∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F] [∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F]

set_option backward.defeqAttrib.useBackward true in
/-- The base change natural transformation for left Kan extensions associated to
a 2-square. -/
@[simps -isSimp]
Expand All @@ -175,10 +273,8 @@ noncomputable def lanBaseChange :
(Eq.trans ?_ (Adjunction.homEquiv_naturality_right_symm ..))
congr 1
ext X
have := R.lanUnit.naturality_app (T.obj X) τ
simp [reassoc_of% this]
simp [dsimp% R.lanUnit.naturality_app_assoc (T.obj X) τ]

set_option backward.defeqAttrib.useBackward true in
lemma isIso_lanBaseChange_app_iff (F : C₂ ⥤ D) :
IsIso (w.lanBaseChange.app F) ↔
IsLeftKanExtension _ ((LeftExtension.mk _ (R.lanUnit.app F)).compTwoSquare w).hom := by
Expand All @@ -200,6 +296,46 @@ instance [∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F]
rw [NatTrans.isIso_iff_isIso_app]
infer_instance

section

variable [∀ (F : C₁ ⥤ D), T.HasRightKanExtension F] [∀ (F : C₃ ⥤ D), B.HasRightKanExtension F]

/-- The base change natural transformation for left Kan extensions associated to
a 2-square. -/
@[simps -isSimp]
noncomputable def ranBaseChange :
B.ran ⋙ (whiskeringLeft C₂ C₄ D).obj R ⟶ (whiskeringLeft C₁ C₃ D).obj L ⋙ T.ran where
app F :=
((T.ranAdjunction _).homEquiv _ _)
((RightExtension.mk _ (B.ranCounit.app F)).compTwoSquare w).hom
naturality {F₁ F₂} τ := by
refine (Adjunction.homEquiv_naturality_left ..).symm.trans
(Eq.trans ?_ (Adjunction.homEquiv_naturality_right ..))
congr 1
ext X
simp [← dsimp% B.ranCounit.naturality_app (L.obj X) τ]

lemma isIso_ranBaseChange_app_iff (F : C₃ ⥤ D) :
IsIso (w.ranBaseChange.app F) ↔
IsRightKanExtension _ ((RightExtension.mk _ (B.ranCounit.app F)).compTwoSquare w).hom := by
rw [ranBaseChange_app, isIso_ranAdjunction_homEquiv_iff]
simp

instance isIso_ranBaseChange_app (F : C₃ ⥤ D)
[B.HasPointwiseRightKanExtension F] [w.GuitartExact] :
IsIso (w.ranBaseChange.app F) := by
rw [isIso_ranBaseChange_app_iff]
let hF := isPointwiseRightKanExtensionOfIsRightKanExtension (F := F) _ (B.ranCounit.app F)
exact (hF.compTwoSquare w).isRightKanExtension

end

instance [∀ (F : C₁ ⥤ D), T.HasRightKanExtension F]
[∀ (F : C₃ ⥤ D), B.HasPointwiseRightKanExtension F] [w.GuitartExact] :
IsIso (w.ranBaseChange (D := D)) := by
rw [NatTrans.isIso_iff_isIso_app]
infer_instance

end

end TwoSquare
Expand Down
Loading