From 1c992798613ae8f6e348005280a6be6b5a46dc93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 29 Jun 2024 10:20:42 +0200
Subject: [PATCH 1/8] feat: dualising results in
 CategoryTheory.Functor.KanExtension.Basic

---
 .../Functor/KanExtension/Basic.lean           | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
index 4e26c9a1ab9609..b799e10ad00f8f 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@@ -83,6 +83,7 @@ a natural transformation, this is the induced morphism `G ⟶ F'`. -/
 noncomputable def liftOfIsRightKanExtension (G : D ⥤ H) (β : L ⋙ G ⟶ F) : G ⟶ F' :=
   (F'.isUniversalOfIsRightKanExtension α).lift (RightExtension.mk G β)
 
+@[reassoc (attr := simp)]
 lemma liftOfIsRightKanExtension_fac (G : D ⥤ H) (β : L ⋙ G ⟶ F) :
     whiskerLeft L (F'.liftOfIsRightKanExtension α G β) ≫ α = β :=
   (F'.isUniversalOfIsRightKanExtension α).fac (RightExtension.mk G β)
@@ -96,6 +97,15 @@ lemma hom_ext_of_isRightKanExtension {G : D ⥤ H} (γ₁ γ₂ : G ⟶ F')
     (hγ : whiskerLeft L γ₁ ≫ α = whiskerLeft L γ₂ ≫ α) : γ₁ = γ₂ :=
   (F'.isUniversalOfIsRightKanExtension α).hom_ext hγ
 
+/-- If `(F', α)` is a right Kan extension of `F` along `L`, then this
+is the induced bijection `(G ⟶ F') ≃ (L ⋙ G ⟶ F)` for all `G`. -/
+noncomputable def homEquivOfIsRightKanExtension (G : D ⥤ H) :
+    (G ⟶ F') ≃ (L ⋙ G ⟶ F) where
+  toFun β := whiskerLeft _ β ≫ α
+  invFun β := liftOfIsRightKanExtension _ α _ β
+  left_inv β := Functor.hom_ext_of_isRightKanExtension _ α _ _ (by aesop_cat)
+  right_inv := by aesop_cat
+
 lemma isRightKanExtension_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H}
     (α : L ⋙ F' ⟶ F) (α' : L ⋙ F'' ⟶ F) (comm : whiskerLeft L e.hom ≫ α' = α)
     [F'.IsRightKanExtension α] : F''.IsRightKanExtension α' where
@@ -112,6 +122,27 @@ lemma isRightKanExtension_iff_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C
     refine isRightKanExtension_of_iso e.symm α' α ?_
     rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]
 
+/-- Two right Kan extensions are (canonically) isomorphic. -/
+@[simps]
+noncomputable def rightKanExtensionUnique
+    (F'' : D ⥤ H) (α' : L ⋙ F'' ⟶ F) [F''.IsRightKanExtension α'] : F' ≅ F'' where
+  hom := F''.liftOfIsRightKanExtension α' F' α
+  inv := F'.liftOfIsRightKanExtension α F'' α'
+  hom_inv_id := F'.hom_ext_of_isRightKanExtension α _ _ (by simp)
+  inv_hom_id := F''.hom_ext_of_isRightKanExtension α' _ _ (by simp)
+
+lemma isRightKanExtension_iff_isIso {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F'' ⟶ F')
+    {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) (α' : L ⋙ F'' ⟶ F)
+    (comm : whiskerLeft L φ ≫ α = α') [F'.IsRightKanExtension α] :
+    F''.IsRightKanExtension α' ↔ IsIso φ := by
+  constructor
+  · intro
+    rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom
+      (by simp [comm])]
+    infer_instance
+  · intro
+    rw [isRightKanExtension_iff_of_iso (asIso φ) α' α comm]
+    infer_instance
 end
 
 section

From 7626f2bddc17277979af1fd82f2cf36112ce0c7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 29 Jun 2024 10:38:42 +0200
Subject: [PATCH 2/8] merging Pointwise.lean with the version in #10425

---
 .../Functor/KanExtension/Pointwise.lean       | 65 +++++++++----------
 1 file changed, 31 insertions(+), 34 deletions(-)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
index c6c2f11f388a78..f716999426820f 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@@ -50,7 +50,7 @@ abbrev HasPointwiseLeftKanExtension := ∀ (Y : D), HasPointwiseLeftKanExtension
 
 namespace LeftExtension
 
-variable {F L} (E : LeftExtension L F)
+variable {F L} (E E' : LeftExtension L F)
 
 /-- The cocone for `CostructuredArrow.proj L Y ⋙ F` attached to `E : LeftExtension L F`.
 The point is this cocone is `E.right.obj Y` -/
@@ -65,14 +65,24 @@ def coconeAt (Y : D) : Cocone (CostructuredArrow.proj L Y ⋙ F) where
         simp only [assoc, NatTrans.naturality_assoc, Functor.comp_map,
           Functor.map_comp, comp_id] }
 
+variable (L F) in
+/-- The cocones for `CostructuredArrow.proj L Y ⋙ F`, as a functor from `LeftExtension L F`. -/
+@[simps]
+def coconeAtFunctor (Y : D) :
+    LeftExtension L F ⥤ Cocone (CostructuredArrow.proj L Y ⋙ F) where
+  obj E := E.coconeAt Y
+  map {E E'} φ := CoconeMorphism.mk (φ.right.app Y) (fun G => by
+    dsimp
+    rw [← StructuredArrow.w φ]
+    simp)
+
 /-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension at `Y` when
 `E.coconeAt Y` is a colimit cocone. -/
 def IsPointwiseLeftKanExtensionAt (Y : D) := IsColimit (E.coconeAt Y)
 
-variable {E}
-
+variable {E} in
 lemma IsPointwiseLeftKanExtensionAt.hasPointwiseLeftKanExtensionAt
-    {E : LeftExtension L F} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) :
+    {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y) :
     HasPointwiseLeftKanExtensionAt L F Y := ⟨_, h⟩
 
 lemma IsPointwiseLeftKanExtensionAt.isIso_hom_app
@@ -80,11 +90,27 @@ lemma IsPointwiseLeftKanExtensionAt.isIso_hom_app
     IsIso (E.hom.app X) := by
   simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal
 
-variable (E) in
 /-- A left extension `E : LeftExtension L F` is a pointwise left Kan extension when
 it is a pointwise left Kan extension at any object. -/
 abbrev IsPointwiseLeftKanExtension := ∀ (Y : D), E.IsPointwiseLeftKanExtensionAt Y
 
+variable {E E'}
+
+/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
+left Kan extension at `Y` iff `E'` is. -/
+def isPointwiseLeftKanExtensionAtEquivOfIso (e : E ≅ E') (Y : D) :
+    E.IsPointwiseLeftKanExtensionAt Y ≃ E'.IsPointwiseLeftKanExtensionAt Y :=
+  IsColimit.equivIsoColimit ((coconeAtFunctor L F Y).mapIso e)
+
+/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
+left Kan extension iff `E'` is. -/
+def isPointwiseLeftKanExtensionEquivOfIso (e : E ≅ E') :
+    E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension where
+  toFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y)
+  invFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y)
+  left_inv h := by aesop
+  right_inv h := by aesop
+
 variable (h : E.IsPointwiseLeftKanExtension)
 
 lemma IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension :
@@ -130,35 +156,6 @@ lemma IsPointwiseLeftKanExtension.isIso_hom [L.Full] [L.Faithful] :
   have := fun X => (h (L.obj X)).isIso_hom_app
   apply NatIso.isIso_of_isIso_app
 
-variable (L F)
-
-/-- The cocones for `CostructuredArrow.proj L Y ⋙ F`, as a functor from `LeftExtension L F`. -/
-@[simps]
-def coconeAtFunctor (Y : D) :
-    LeftExtension L F ⥤ Cocone (CostructuredArrow.proj L Y ⋙ F) where
-  obj E := E.coconeAt Y
-  map {E E'} φ := CoconeMorphism.mk (φ.right.app Y) (fun G => by
-    dsimp
-    rw [← StructuredArrow.w φ]
-    simp)
-
-variable {L F E'}
-
-/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
-left Kan extension at `Y` iff `E'` is. -/
-def isPointwiseLeftKanExtensionAtEquivOfIso (e : E ≅ E') (Y : D) :
-    E.IsPointwiseLeftKanExtensionAt Y ≃ E'.IsPointwiseLeftKanExtensionAt Y :=
-  IsColimit.equivIsoColimit ((coconeAtFunctor L F Y).mapIso e)
-
-/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
-left Kan extension iff `E'` is. -/
-def isPointwiseLeftKanExtensionEquivOfIso (e : E ≅ E') :
-    E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension where
-  toFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y)
-  invFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y)
-  left_inv h := by aesop
-  right_inv h := by aesop
-
 end LeftExtension
 
 section

From 02e4cadf46733437b03cf03500bcafdf6078f9bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 29 Jun 2024 11:17:13 +0200
Subject: [PATCH 3/8] sync

---
 .../Functor/KanExtension/Pointwise.lean       | 202 +++++++++++++++++-
 1 file changed, 200 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
index f716999426820f..578c500351a726 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@@ -20,9 +20,10 @@ Conversely, when `CostructuredArrow.proj L Y ⋙ F` has a colimit, we say that
 and if this holds for all `Y : D`, we construct a functor
 `pointwiseLeftKanExtension L F : D ⥤ H` and show it is a pointwise Kan extension.
 
+A dual API for pointwise right Kan extension is also formalized.
+
 ## TODO
 
-* obtain similar results for right Kan extensions
 * refactor the file `CategoryTheory.Limits.KanExtension` using this new general API
 
 ## References
@@ -48,12 +49,22 @@ abbrev HasPointwiseLeftKanExtensionAt (Y : D) :=
 that it has a pointwise left Kan extension at any object. -/
 abbrev HasPointwiseLeftKanExtension := ∀ (Y : D), HasPointwiseLeftKanExtensionAt L F Y
 
+/-- The condition that a functor `F` has a pointwise right Kan extension along `L` at `Y`.
+It means that the functor `StructuredArrow.proj Y L ⋙ F : StructuredArrow Y L ⥤ H`
+has a limit. -/
+abbrev HasPointwiseRightKanExtensionAt (Y : D) :=
+  HasLimit (StructuredArrow.proj Y L ⋙ F)
+
+/-- The condition that a functor `F` has a pointwise right Kan extension along `L`: it means
+that it has a pointwise right Kan extension at any object. -/
+abbrev HasPointwiseRightKanExtension := ∀ (Y : D), HasPointwiseRightKanExtensionAt L F Y
+
 namespace LeftExtension
 
 variable {F L} (E E' : LeftExtension L F)
 
 /-- The cocone for `CostructuredArrow.proj L Y ⋙ F` attached to `E : LeftExtension L F`.
-The point is this cocone is `E.right.obj Y` -/
+The point of this cocone is `E.right.obj Y` -/
 @[simps]
 def coconeAt (Y : D) : Cocone (CostructuredArrow.proj L Y ⋙ F) where
   pt := E.right.obj Y
@@ -158,6 +169,115 @@ lemma IsPointwiseLeftKanExtension.isIso_hom [L.Full] [L.Faithful] :
 
 end LeftExtension
 
+namespace RightExtension
+
+variable {F L} (E E' : RightExtension L F)
+
+/-- The cone for `StructuredArrow.proj Y L ⋙ F` attached to `E : RightExtension L F`.
+The point of this cone is `E.left.obj Y` -/
+@[simps]
+def coneAt (Y : D) : Cone (StructuredArrow.proj Y L ⋙ F) where
+  pt := E.left.obj Y
+  π :=
+    { app := fun g ↦ E.left.map g.hom ≫ E.hom.app g.right
+      naturality := fun g₁ g₂ φ ↦ by
+        dsimp
+        rw [assoc, id_comp, ← StructuredArrow.w φ, Functor.map_comp, assoc]
+        congr 1
+        apply E.hom.naturality }
+
+variable (L F) in
+/-- The cones for `StructuredArrow.proj Y L ⋙ F`, as a functor from `RightExtension L F`. -/
+@[simps]
+def coneAtFunctor (Y : D) :
+    RightExtension L F ⥤ Cone (StructuredArrow.proj Y L ⋙ F) where
+  obj E := E.coneAt Y
+  map {E E'} φ := ConeMorphism.mk (φ.left.app Y) (fun G ↦ by
+    dsimp
+    rw [← CostructuredArrow.w φ]
+    simp)
+
+/-- A right extension `E : RightExtension L F` is a pointwise right Kan extension at `Y` when
+`E.coneAt Y` is a limit cone. -/
+def IsPointwiseRightKanExtensionAt (Y : D) := IsLimit (E.coneAt Y)
+
+variable {E} in
+lemma IsPointwiseRightKanExtensionAt.hasPointwiseRightKanExtensionAt
+    {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y) :
+    HasPointwiseRightKanExtensionAt L F Y := ⟨_, h⟩
+
+lemma IsPointwiseRightKanExtensionAt.isIso_hom_app
+    {X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
+    IsIso (E.hom.app X) := by
+  simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial
+
+/-- A right extension `E : RightExtension L F` is a pointwise right Kan extension when
+it is a pointwise right Kan extension at any object. -/
+abbrev IsPointwiseRightKanExtension := ∀ (Y : D), E.IsPointwiseRightKanExtensionAt Y
+
+variable {E E'}
+
+/-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
+left Kan extension at `Y` iff `E'` is. -/
+def isPointwiseRightKanExtensionAtEquivOfIso (e : E ≅ E') (Y : D) :
+    E.IsPointwiseRightKanExtensionAt Y ≃ E'.IsPointwiseRightKanExtensionAt Y :=
+  IsLimit.equivIsoLimit ((coneAtFunctor L F Y).mapIso e)
+
+/-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
+right Kan extension iff `E'` is. -/
+def isPointwiseRightKanExtensionEquivOfIso (e : E ≅ E') :
+    E.IsPointwiseRightKanExtension ≃ E'.IsPointwiseRightKanExtension where
+  toFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y)
+  invFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y)
+  left_inv h := by aesop
+  right_inv h := by aesop
+
+variable (h : E.IsPointwiseRightKanExtension)
+
+lemma IsPointwiseRightKanExtension.hasPointwiseRightKanExtension :
+    HasPointwiseRightKanExtension L F :=
+  fun Y => (h Y).hasPointwiseRightKanExtensionAt
+
+/-- The (unique) morphism to a pointwise right Kan extension. -/
+def IsPointwiseRightKanExtension.homTo (G : RightExtension L F) : G ⟶ E :=
+  CostructuredArrow.homMk
+    { app := fun Y ↦ (h Y).lift (RightExtension.coneAt G Y)
+      naturality := fun Y₁ Y₂ φ ↦ (h Y₂).hom_ext (fun X ↦ by
+        rw [assoc, (h Y₂).fac (coneAt G Y₂) X]
+        simpa using ((h Y₁).fac (coneAt G Y₁) ((StructuredArrow.map φ).obj X)).symm) }
+    (by
+      ext X
+      simpa using (h (L.obj X)).fac (RightExtension.coneAt G _) (StructuredArrow.mk (𝟙 _)) )
+
+lemma IsPointwiseRightKanExtension.hom_ext {G : RightExtension L F} {f₁ f₂ : G ⟶ E} : f₁ = f₂ := by
+  ext Y
+  apply (h Y).hom_ext
+  intro X
+  have eq₁ := congr_app (CostructuredArrow.w f₁) X.right
+  have eq₂ := congr_app (CostructuredArrow.w f₂) X.right
+  dsimp at eq₁ eq₂ ⊢
+  simp only [assoc, ← NatTrans.naturality_assoc, eq₁, eq₂]
+
+/-- A pointwise right Kan extension is universal, i.e. it is a right Kan extension. -/
+def IsPointwiseRightKanExtension.isUniversal : E.IsUniversal :=
+  IsTerminal.ofUniqueHom h.homTo (fun _ _ => h.hom_ext)
+
+lemma IsPointwiseRightKanExtension.isRightKanExtension :
+    E.left.IsRightKanExtension E.hom where
+  nonempty_isUniversal := ⟨h.isUniversal⟩
+
+lemma IsPointwiseRightKanExtension.hasRightKanExtension :
+    HasRightKanExtension L F :=
+  have := h.isRightKanExtension
+  HasRightKanExtension.mk E.left E.hom
+
+lemma IsPointwiseRightKanExtension.isIso_hom [L.Full] [L.Faithful] :
+    IsIso (E.hom) := by
+  have := fun X => (h (L.obj X)).isIso_hom_app
+  apply NatIso.isIso_of_isIso_app
+
+end RightExtension
+
 section
 
 variable [HasPointwiseLeftKanExtension L F]
@@ -235,6 +355,84 @@ noncomputable def isPointwiseLeftKanExtensionOfIsLeftKanExtension (F' : D ⥤ H)
 
 end
 
+section
+
+variable [HasPointwiseRightKanExtension L F]
+
+/-- The constructed pointwise right Kan extension
+when `HasPointwiseRightKanExtension L F` holds. -/
+@[simps]
+noncomputable def pointwiseRightKanExtension : D ⥤ H where
+  obj Y := limit (StructuredArrow.proj Y L ⋙ F)
+  map {Y₁ Y₂} f := limit.lift (StructuredArrow.proj Y₂ L ⋙ F)
+      (Cone.mk (limit (StructuredArrow.proj Y₁ L ⋙ F))
+        { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F)
+            ((StructuredArrow.map f).obj g)
+          naturality := fun g₁ g₂ φ ↦ by
+            simpa using (limit.w (StructuredArrow.proj Y₁ L ⋙ F)
+              ((StructuredArrow.map f).map φ)).symm })
+  map_id Y := limit.hom_ext (fun j => by
+    dsimp
+    simp only [limit.lift_π, id_comp]
+    congr
+    apply StructuredArrow.map_id)
+  map_comp {Y₁ Y₂ Y₃} f f' := limit.hom_ext (fun j => by
+    dsimp
+    simp only [limit.lift_π, assoc]
+    congr 1
+    apply StructuredArrow.map_comp)
+
+/-- The counit of the constructed pointwise right Kan extension when
+`HasPointwiseRightKanExtension L F` holds. -/
+@[simps]
+noncomputable def pointwiseRightKanExtensionCounit :
+    L ⋙ pointwiseRightKanExtension L F ⟶ F where
+  app X := limit.π (StructuredArrow.proj (L.obj X) L ⋙ F)
+    (StructuredArrow.mk (𝟙 (L.obj X)))
+  naturality {X₁ X₂} f:= by
+    simp only [comp_obj, pointwiseRightKanExtension_obj, comp_map,
+      pointwiseRightKanExtension_map, limit.lift_π, StructuredArrow.map_mk]
+    rw [comp_id]
+    let φ : StructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) :=
+      StructuredArrow.homMk f
+    exact (limit.w (StructuredArrow.proj (L.obj X₁) L ⋙ F) φ).symm
+
+/-- The functor `pointwiseRightKanExtension L F` is a pointwise right Kan
+extension of `F` along `L`. -/
+noncomputable def pointwiseRightKanExtensionIsPointwiseRightKanExtension :
+    (RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).IsPointwiseRightKanExtension :=
+  fun X => IsLimit.ofIsoLimit (limit.isLimit _) (Cones.ext (Iso.refl _) (fun j => by
+    dsimp
+    simp only [limit.lift_π, StructuredArrow.map_mk, id_comp]
+    congr
+    rw [comp_id, ← StructuredArrow.eq_mk]))
+
+/-- The functor `pointwiseRightKanExtension L F` is a right Kan extension of `F` along `L`. -/
+noncomputable def pointwiseRightKanExtensionIsUniversal :
+    (RightExtension.mk _ (pointwiseRightKanExtensionCounit L F)).IsUniversal :=
+  (pointwiseRightKanExtensionIsPointwiseRightKanExtension L F).isUniversal
+
+instance : (pointwiseRightKanExtension L F).IsRightKanExtension
+    (pointwiseRightKanExtensionCounit L F) where
+  nonempty_isUniversal := ⟨pointwiseRightKanExtensionIsUniversal L F⟩
+
+instance : HasRightKanExtension L F :=
+  HasRightKanExtension.mk _ (pointwiseRightKanExtensionCounit L F)
+
+variable {F L}
+
+/-- If `F` admits a pointwise right Kan extension along `L`, then any right Kan extension of `F`
+along `L` is a pointwise right Kan extension. -/
+noncomputable def isPointwiseRightKanExtensionOfIsRightKanExtension (F' : D ⥤ H) (α : L ⋙ F' ⟶ F)
+    [F'.IsRightKanExtension α] :
+    (RightExtension.mk _ α).IsPointwiseRightKanExtension :=
+  RightExtension.isPointwiseRightKanExtensionEquivOfIso
+    (IsLimit.conePointUniqueUpToIso (pointwiseRightKanExtensionIsUniversal L F)
+      (F'.isUniversalOfIsRightKanExtension α))
+    (pointwiseRightKanExtensionIsPointwiseRightKanExtension L F)
+
+end
+
 end Functor
 
 end CategoryTheory

From cea366070c837f7f8350388bca5ec56622f42616 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 29 Jun 2024 11:48:01 +0200
Subject: [PATCH 4/8] sync Adjunction.lean

---
 .../Functor/KanExtension/Adjunction.lean      | 136 +++++++++++++++++-
 1 file changed, 129 insertions(+), 7 deletions(-)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
index 8bdc6e90e21780..abd599ac0e19df 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@@ -14,8 +14,11 @@ a left Kan extension. It is shown that `L.lan` is the left adjoint to
 the functor `(D ⥤ H) ⥤ (C ⥤ H)` given by the precomposition
 with `L` (see `Functor.lanAdjunction`).
 
+Similarly, we define the right Kan extension functor
+`L.ran : (C ⥤ H) ⥤ (D ⥤ H)` which sends a functor `F : C ⥤ H` to its
+right Kan extension along `L`.
+
 ## TODO
-- dualize the results for right Kan extensions
 - refactor the file `CategoryTheory.Limits.KanExtension` so that
 the definitions of `Lan` and `Ran` in that file (which rely on the
 existence of (co)limits) are replaced by the new definition
@@ -29,8 +32,13 @@ open Category
 
 namespace Functor
 
-variable {C D : Type*} [Category C] [Category D] (L : C ⥤ D)
-  {H : Type*} [Category H] [∀ (F : C ⥤ H), HasLeftKanExtension L F]
+variable {C D : Type*} [Category C] [Category D] (L : C ⥤ D) {H : Type*} [Category H]
+
+section lan
+
+section
+
+variable [∀ (F : C ⥤ H), HasLeftKanExtension L F]
 
 /-- The left Kan extension functor `(C ⥤ H) ⥤ (D ⥤ H)` along a functor `C ⥤ D`. -/
 noncomputable def lan : (C ⥤ H) ⥤ (D ⥤ H) where
@@ -61,7 +69,7 @@ noncomputable def lanAdjunction : L.lan ⊣ (whiskeringLeft C D H).obj L :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun F G => homEquivOfIsLeftKanExtension _ (L.lanUnit.app F) G
       homEquiv_naturality_left_symm := fun {F₁ F₂ G} f α =>
-        hom_ext_of_isLeftKanExtension _  (L.lanUnit.app F₁) _ _ (by
+        hom_ext_of_isLeftKanExtension _ (L.lanUnit.app F₁) _ _ (by
           ext X
           dsimp [homEquivOfIsLeftKanExtension]
           rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]
@@ -98,15 +106,19 @@ lemma isIso_lanAdjunction_counit_app_iff (G : D ⥤ H) :
     IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (𝟙 (L ⋙ G)) :=
   (isLeftKanExtension_iff_isIso _ (L.lanUnit.app (L ⋙ G)) _ (by simp)).symm
 
+end
+
 section
 
 variable [Full L] [Faithful L]
 
-instance (F : C ⥤ H) (X : C) [HasPointwiseLeftKanExtension L F] :
+instance (F : C ⥤ H) (X : C) [HasPointwiseLeftKanExtension L F]
+    [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
     IsIso ((L.lanUnit.app F).app X) :=
   (isPointwiseLeftKanExtensionLanUnit L F (L.obj X)).isIso_hom_app
 
-instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] :
+instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F]
+    [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
     IsIso (L.lanUnit.app F) :=
   NatIso.isIso_of_isIso_app _
 
@@ -114,7 +126,8 @@ instance coreflective [∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] :
     IsIso (L.lanUnit (H := H)) := by
   apply NatIso.isIso_of_isIso_app _
 
-instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] :
+instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F]
+    [∀ (F : C ⥤ H), HasLeftKanExtension L F] :
     IsIso ((L.lanAdjunction H).unit.app F) := by
   rw [lanAdjunction_unit]
   infer_instance
@@ -125,6 +138,115 @@ instance coreflective' [∀ (F : C ⥤ H), HasPointwiseLeftKanExtension L F] :
 
 end
 
+end lan
+
+section ran
+
+section
+
+variable [∀ (F : C ⥤ H), HasRightKanExtension L F]
+
+/-- The right Kan extension functor `(C ⥤ H) ⥤ (D ⥤ H)` along a functor `C ⥤ D`. -/
+noncomputable def ran : (C ⥤ H) ⥤ (D ⥤ H) where
+  obj F := rightKanExtension L F
+  map {F₁ F₂} φ := liftOfIsRightKanExtension _ (rightKanExtensionCounit L F₂) _
+    (rightKanExtensionCounit L F₁ ≫ φ)
+
+/-- The natural transformation `L ⋙ (L.lan).obj G ⟶ L`. -/
+noncomputable def ranCounit : L.ran ⋙ (whiskeringLeft C D H).obj L ⟶ (𝟭 (C ⥤ H)) where
+  app F := rightKanExtensionCounit L F
+  naturality {F₁ F₂} φ := by ext; simp [ran]
+
+instance (F : C ⥤ H) : (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F) := by
+  dsimp [ran, ranCounit]
+  infer_instance
+
+/-- If there exists a pointwise right Kan extension of `F` along `L`,
+then `L.lan.obj G` is a pointwise right Kan extension of `F`. -/
+noncomputable def isPointwiseRightKanExtensionRanCounit
+    (F : C ⥤ H) [HasPointwiseRightKanExtension L F] :
+    (RightExtension.mk _ (L.ranCounit.app F)).IsPointwiseRightKanExtension :=
+  isPointwiseRightKanExtensionOfIsRightKanExtension (F := F) _ (L.ranCounit.app F)
+
+variable (H) in
+/-- The right Kan extension functor `L.ran` is left adjoint to the
+precomposition by `L`. -/
+noncomputable def ranAdjunction : (whiskeringLeft C D H).obj L ⊣ L.ran :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv := fun F G =>
+        (homEquivOfIsRightKanExtension (α := L.ranCounit.app G) F).symm
+      homEquiv_naturality_right := fun {F G₁ G₂} β f ↦
+        hom_ext_of_isRightKanExtension _ (L.ranCounit.app G₂) _ _ (by
+        ext X
+        dsimp [homEquivOfIsRightKanExtension]
+        rw [liftOfIsRightKanExtension_fac_app, NatTrans.comp_app, assoc]
+        have h := congr_app (L.ranCounit.naturality f) X
+        dsimp at h ⊢
+        rw [h, liftOfIsRightKanExtension_fac_app_assoc])
+      homEquiv_naturality_left_symm := fun {F₁ F₂ G} β f ↦ by
+        dsimp [homEquivOfIsRightKanExtension]
+        rw [assoc] }
+
+variable (H) in
+@[simp]
+lemma ranAdjunction_counit : (L.ranAdjunction H).counit = L.ranCounit := by
+  ext F : 2
+  dsimp [ranAdjunction, homEquivOfIsRightKanExtension]
+  simp
+
+lemma ranAdjunction_unit_app (G : D ⥤ H) :
+    (L.ranAdjunction H).unit.app G =
+      liftOfIsRightKanExtension (L.ran.obj (L ⋙ G)) (L.ranCounit.app (L ⋙ G)) G (𝟙 (L ⋙ G)) :=
+  rfl
+
+@[reassoc (attr := simp)]
+lemma ranCounit_app_whiskerLeft_ranAdjunction_unit_app (G : D ⥤ H) :
+    whiskerLeft L ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G) := by
+  simp [ranAdjunction_unit_app]
+
+@[reassoc (attr := simp)]
+lemma ranCounit_app_app_ranAdjunction_unit_app_app (G : D ⥤ H) (X : C) :
+    ((L.ranAdjunction H).unit.app G).app (L.obj X) ≫ (L.ranCounit.app (L ⋙ G)).app X = 𝟙 _ :=
+  congr_app (L.ranCounit_app_whiskerLeft_ranAdjunction_unit_app G) X
+
+lemma isIso_ranAdjunction_unit_app_iff (G : D ⥤ H) :
+    IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (𝟙 (L ⋙ G)) :=
+  (isRightKanExtension_iff_isIso _ (L.ranCounit.app (L ⋙ G)) _ (by simp)).symm
+
+end
+
+section
+
+variable [Full L] [Faithful L]
+
+instance (F : C ⥤ H) (X : C) [HasPointwiseRightKanExtension L F]
+    [∀ (F : C ⥤ H), HasRightKanExtension L F] :
+    IsIso ((L.ranCounit.app F).app X) :=
+  (isPointwiseRightKanExtensionRanCounit L F (L.obj X)).isIso_hom_app
+
+instance (F : C ⥤ H) [HasPointwiseRightKanExtension L F]
+    [∀ (F : C ⥤ H), HasRightKanExtension L F] :
+    IsIso (L.ranCounit.app F) :=
+  NatIso.isIso_of_isIso_app _
+
+instance reflective [∀ (F : C ⥤ H), HasPointwiseRightKanExtension L F] :
+    IsIso (L.ranCounit (H := H)) := by
+  apply NatIso.isIso_of_isIso_app _
+
+instance (F : C ⥤ H) [HasPointwiseRightKanExtension L F]
+    [∀ (F : C ⥤ H), HasRightKanExtension L F] :
+    IsIso ((L.ranAdjunction H).counit.app F) := by
+  rw [ranAdjunction_counit]
+  infer_instance
+
+instance reflective' [∀ (F : C ⥤ H), HasPointwiseRightKanExtension L F] :
+    IsIso (L.ranAdjunction H).counit := by
+  apply NatIso.isIso_of_isIso_app _
+
+end
+
+end ran
+
 end Functor
 
 end CategoryTheory

From 435013779c60a3298a8d5d3412939dc883b1acae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Mon, 1 Jul 2024 11:21:05 +0200
Subject: [PATCH 5/8] fix

---
 Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
index bd8aa7a949f627..90dee24fe319e6 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@@ -172,7 +172,8 @@ end LeftExtension
 
 namespace RightExtension
 
-variable {F L} (E E' : RightExtension L F)
+variable {F L}
+variable (E E' : RightExtension L F)
 
 /-- The cone for `StructuredArrow.proj Y L ⋙ F` attached to `E : RightExtension L F`.
 The point of this cone is `E.left.obj Y` -/

From c931dccb8798ddfecc756ef7ca28521a439ded1c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Wed, 3 Jul 2024 19:02:03 +0200
Subject: [PATCH 6/8] Update
 Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
---
 Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
index 90dee24fe319e6..f4d31d1bff5817 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@@ -220,7 +220,7 @@ abbrev IsPointwiseRightKanExtension := ∀ (Y : D), E.IsPointwiseRightKanExtensi
 variable {E E'}
 
 /-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
-left Kan extension at `Y` iff `E'` is. -/
+right Kan extension at `Y` iff `E'` is. -/
 def isPointwiseRightKanExtensionAtEquivOfIso (e : E ≅ E') (Y : D) :
     E.IsPointwiseRightKanExtensionAt Y ≃ E'.IsPointwiseRightKanExtensionAt Y :=
   IsLimit.equivIsoLimit ((coneAtFunctor L F Y).mapIso e)

From 3541bdbb2e6b4e838ecd56a3e167e6aa9adb46e8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Fri, 5 Jul 2024 13:26:54 +0200
Subject: [PATCH 7/8] Update
 Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
---
 Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
index 05ea56c0c77d65..d09cc81db67a10 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@@ -170,7 +170,7 @@ noncomputable def isPointwiseRightKanExtensionRanCounit
   isPointwiseRightKanExtensionOfIsRightKanExtension (F := F) _ (L.ranCounit.app F)
 
 variable (H) in
-/-- The right Kan extension functor `L.ran` is left adjoint to the
+/-- The right Kan extension functor `L.ran` is right adjoint to the
 precomposition by `L`. -/
 noncomputable def ranAdjunction : (whiskeringLeft C D H).obj L ⊣ L.ran :=
   Adjunction.mkOfHomEquiv

From 73213fe077bd7260788282389b6545cb3e7b6b9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?=
 <37772949+joelriou@users.noreply.github.com>
Date: Fri, 5 Jul 2024 13:27:02 +0200
Subject: [PATCH 8/8] Update
 Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Dagur Tómas Ásgeirsson <dagurtomas@gmail.com>
---
 Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
index d09cc81db67a10..0475aa99517fce 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@@ -163,7 +163,7 @@ instance (F : C ⥤ H) : (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F) :
   infer_instance
 
 /-- If there exists a pointwise right Kan extension of `F` along `L`,
-then `L.lan.obj G` is a pointwise right Kan extension of `F`. -/
+then `L.ran.obj G` is a pointwise right Kan extension of `F`. -/
 noncomputable def isPointwiseRightKanExtensionRanCounit
     (F : C ⥤ H) [HasPointwiseRightKanExtension L F] :
     (RightExtension.mk _ (L.ranCounit.app F)).IsPointwiseRightKanExtension :=