feat(CategoryTheory/KanExtension): Composing lan with colim (#17355)

Co-authored-by: Joël Riou <[email protected]>

Mathlib/CategoryTheory/Functor/Const.lean

@@ -99,6 +99,13 @@ def compConstIso (F : C ⥤ D) :
     (fun X => NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
     (by aesop_cat)
 
+/-- The canonical isomorphism
+`const D ⋙ (whiskeringLeft J _ _).obj F ≅ const J`.-/
+@[simps!]
+def constCompWhiskeringLeftIso (F : J ⥤ D) :
+    const D ⋙ (whiskeringLeft J D C).obj F ≅ const J :=
+  NatIso.ofComponents fun X => NatIso.ofComponents fun Y => Iso.refl _
+
 end
 
 end CategoryTheory.Functor

Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

@@ -22,7 +22,7 @@ right Kan extension along `L`.
 
 namespace CategoryTheory
 
-open Category
+open Category Limits
 
 namespace Functor
 
@@ -122,6 +122,20 @@ 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
 
+/-- Composing the left Kan extension of `L : C ⥤ D` with `colim` on shapes `D` is isomorphic
+to `colim` on shapes `C`. -/
+@[simps!]
+noncomputable def lanCompColimIso (L : C ⥤ D) [∀ (G : C ⥤ H), L.HasLeftKanExtension G]
+    [HasColimitsOfShape C H] [HasColimitsOfShape D H] : L.lan ⋙ colim ≅ colim (C := H) :=
+  Iso.symm <| NatIso.ofComponents
+    (fun G ↦ (colimitIsoOfIsLeftKanExtension _ (L.lanUnit.app G)).symm)
+    (fun f ↦ colimit.hom_ext (fun i ↦ by
+      dsimp
+      rw [ι_colimMap_assoc, ι_colimitIsoOfIsLeftKanExtension_inv,
+        ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimMap, ← assoc, ← assoc]
+      congr 1
+      exact congr_app (L.lanUnit.naturality f) i))
+
 end
 
 section
@@ -251,6 +265,20 @@ 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
 
+/-- Composing the right Kan extension of `L : C ⥤ D` with `lim` on shapes `D` is isomorphic
+to `lim` on shapes `C`. -/
+@[simps!]
+noncomputable def ranCompLimIso (L : C ⥤ D) [∀ (G : C ⥤ H), L.HasRightKanExtension G]
+    [HasLimitsOfShape C H] [HasLimitsOfShape D H] : L.ran ⋙ lim ≅ lim (C := H) :=
+  NatIso.ofComponents
+    (fun G ↦ limitIsoOfIsRightKanExtension _ (L.ranCounit.app G))
+    (fun f ↦ limit.hom_ext (fun i ↦ by
+      dsimp
+      rw [assoc, assoc, limMap_π, limitIsoOfIsRightKanExtension_hom_π_assoc,
+        limitIsoOfIsRightKanExtension_hom_π, limMap_π_assoc]
+      congr 1
+      exact congr_app (L.ranCounit.naturality f) i))
+
 end
 
 section

Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean

@@ -544,6 +544,106 @@ lemma isRightKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : L ⋙ F
 
 end
 
+section Colimit
+
+variable (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') [F'.IsLeftKanExtension α]
+
+/-- Construct a cocone for a left Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor
+`L : C ⥤ D` given a cocone for `F`. -/
+@[simps]
+noncomputable def coconeOfIsLeftKanExtension (c : Cocone F) : Cocone F' where
+  pt := c.pt
+  ι := F'.descOfIsLeftKanExtension α _ c.ι
+
+/-- If `c` is a colimit cocone for a functor `F : C ⥤ H` and `α : F ⟶ L ⋙ F'` is the unit of any
+left Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coconeOfIsLeftKanExtension α c` is
+a colimit cocone, too. -/
+@[simps]
+def isColimitCoconeOfIsLeftKanExtension {c : Cocone F} (hc : IsColimit c) :
+    IsColimit (F'.coconeOfIsLeftKanExtension α c) where
+  desc s := hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))
+  fac s := by
+    have : F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
+        (Functor.const _).map (hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))) = s.ι :=
+      F'.hom_ext_of_isLeftKanExtension α _ _ (by aesop_cat)
+    exact congr_app this
+  uniq s m hm := hc.hom_ext (fun j ↦ by
+    have := hm (L.obj j)
+    nth_rw 1 [← F'.descOfIsLeftKanExtension_fac_app α ((const D).obj c.pt)]
+    dsimp at this ⊢
+    rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app])
+
+variable [HasColimit F] [HasColimit F']
+
+/-- If `F' : D ⥤ H` is a left Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the colimit over `F'`
+is isomorphic to the colimit over `F`. -/
+noncomputable def colimitIsoOfIsLeftKanExtension : colimit F' ≅ colimit F :=
+  IsColimit.coconePointUniqueUpToIso (colimit.isColimit F')
+    (F'.isColimitCoconeOfIsLeftKanExtension α (colimit.isColimit F))
+
+@[reassoc (attr := simp)]
+lemma ι_colimitIsoOfIsLeftKanExtension_hom (i : C) :
+    α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom =
+      colimit.ι F i := by
+  simp [colimitIsoOfIsLeftKanExtension]
+
+@[reassoc (attr := simp)]
+lemma ι_colimitIsoOfIsLeftKanExtension_inv (i : C) :
+    colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv =
+    α.app i ≫ colimit.ι F' (L.obj i) := by
+  rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]
+
+end Colimit
+
+section Limit
+
+variable (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) [F'.IsRightKanExtension α]
+
+/-- Construct a cone for a right Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor
+`L : C ⥤ D` given a cone for `F`. -/
+@[simps]
+noncomputable def coneOfIsRightKanExtension (c : Cone F) : Cone F' where
+  pt := c.pt
+  π := F'.liftOfIsRightKanExtension α _ c.π
+
+/-- If `c` is a limit cone for a functor `F : C ⥤ H` and `α : L ⋙ F' ⟶ F` is the counit of any
+right Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coneOfIsRightKanExtension α c` is
+a limit cone, too. -/
+@[simps]
+def isLimitConeOfIsRightKanExtension {c : Cone F} (hc : IsLimit c) :
+    IsLimit (F'.coneOfIsRightKanExtension α c) where
+  lift s := hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))
+  fac s := by
+    have : (Functor.const _).map (hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))) ≫
+        F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π = s.π :=
+      F'.hom_ext_of_isRightKanExtension α _ _ (by aesop_cat)
+    exact congr_app this
+  uniq s m hm := hc.hom_ext (fun j ↦ by
+    have := hm (L.obj j)
+    nth_rw 1 [← F'.liftOfIsRightKanExtension_fac_app α ((const D).obj c.pt)]
+    dsimp at this ⊢
+    rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app])
+
+variable [HasLimit F] [HasLimit F']
+
+/-- If `F' : D ⥤ H` is a right Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the limit over `F'`
+is isomorphic to the limit over `F`. -/
+noncomputable def limitIsoOfIsRightKanExtension : limit F' ≅ limit F :=
+  IsLimit.conePointUniqueUpToIso (limit.isLimit F')
+    (F'.isLimitConeOfIsRightKanExtension α (limit.isLimit F))
+
+@[reassoc (attr := simp)]
+lemma limitIsoOfIsRightKanExtension_inv_π (i : C) :
+    (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i := by
+  simp [limitIsoOfIsRightKanExtension]
+
+@[reassoc (attr := simp)]
+lemma limitIsoOfIsRightKanExtension_hom_π (i : C) :
+    (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i := by
+  rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]
+
+end Limit
+
 end Functor
 
 end CategoryTheory