feat(CategoryTheory/Functor): more API for pointwise Kan extensions (#22474)

Transport pointwise Kan extensions via isomorphisms/equivalences.

Author: joelriou

Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

@@ -33,7 +33,8 @@ open Category Limits
 
 namespace Functor
 
-variable {C D H : Type*} [Category C] [Category D] [Category H] (L : C ⥤ D) (F : C ⥤ H)
+variable {C D D' H : Type*} [Category C] [Category D] [Category D'] [Category H]
+  (L : C ⥤ D) (L' : C ⥤ D') (F : C ⥤ H)
 
 /-- The condition that a functor `F` has a pointwise left Kan extension along `L` at `Y`.
 It means that the functor `CostructuredArrow.proj L Y ⋙ F : CostructuredArrow L Y ⥤ H`
@@ -55,6 +56,108 @@ abbrev HasPointwiseRightKanExtensionAt (Y : D) :=
 that it has a pointwise right Kan extension at any object. -/
 abbrev HasPointwiseRightKanExtension := ∀ (Y : D), HasPointwiseRightKanExtensionAt L F Y
 
+lemma hasPointwiseLeftKanExtensionAt_iff_of_iso {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂) :
+    HasPointwiseLeftKanExtensionAt L F Y₁ ↔
+      HasPointwiseLeftKanExtensionAt L F Y₂ := by
+  revert Y₁ Y₂ e
+  suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseLeftKanExtensionAt L F Y₁],
+      HasPointwiseLeftKanExtensionAt L F Y₂ from
+    fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
+  intro Y₁ Y₂ e _
+  change HasColimit ((CostructuredArrow.mapIso e.symm).functor ⋙ CostructuredArrow.proj L Y₁ ⋙ F)
+  infer_instance
+
+lemma hasPointwiseRightKanExtensionAt_iff_of_iso {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂) :
+    HasPointwiseRightKanExtensionAt L F Y₁ ↔
+      HasPointwiseRightKanExtensionAt L F Y₂ := by
+  revert Y₁ Y₂ e
+  suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseRightKanExtensionAt L F Y₁],
+      HasPointwiseRightKanExtensionAt L F Y₂ from
+    fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
+  intro Y₁ Y₂ e _
+  change HasLimit ((StructuredArrow.mapIso e.symm).functor ⋙ StructuredArrow.proj Y₁ L ⋙ F)
+  infer_instance
+
+variable {L} in
+/-- `HasPointwiseLeftKanExtensionAt` is invariant when we replace `L` by an equivalent functor. -/
+lemma hasPointwiseLeftKanExtensionAt_iff_of_natIso {L' : C ⥤ D} (e : L ≅ L') (Y : D) :
+    HasPointwiseLeftKanExtensionAt L F Y ↔
+      HasPointwiseLeftKanExtensionAt L' F Y := by
+  revert L L' e
+  suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseLeftKanExtensionAt L F Y],
+      HasPointwiseLeftKanExtensionAt L' F Y from
+    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
+  intro L L' e _
+  let Φ : CostructuredArrow L' Y ≌ CostructuredArrow L Y := Comma.mapLeftIso _ e.symm
+  let e' : CostructuredArrow.proj L' Y ⋙ F ≅
+    Φ.functor ⋙ CostructuredArrow.proj L Y ⋙ F := Iso.refl _
+  exact hasColimit_of_iso e'
+
+variable {L} in
+/-- `HasPointwiseRightKanExtensionAt` is invariant when we replace `L` by an equivalent functor. -/
+lemma hasPointwiseRightKanExtensionAt_iff_of_natIso {L' : C ⥤ D} (e : L ≅ L') (Y : D) :
+    HasPointwiseRightKanExtensionAt L F Y ↔
+      HasPointwiseRightKanExtensionAt L' F Y := by
+  revert L L' e
+  suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseRightKanExtensionAt L F Y],
+      HasPointwiseRightKanExtensionAt L' F Y from
+    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
+  intro L L' e _
+  let Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso _ e.symm
+  let e' : StructuredArrow.proj Y L' ⋙ F ≅
+    Φ.functor ⋙ StructuredArrow.proj Y L ⋙ F := Iso.refl _
+  exact hasLimit_of_iso e'.symm
+
+lemma hasPointwiseLeftKanExtensionAt_of_equivalence
+    (E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y')
+    [HasPointwiseLeftKanExtensionAt L F Y] :
+    HasPointwiseLeftKanExtensionAt L' F Y' := by
+  rw [← hasPointwiseLeftKanExtensionAt_iff_of_natIso F eL,
+    hasPointwiseLeftKanExtensionAt_iff_of_iso _ F e.symm]
+  let Φ := CostructuredArrow.post L E.functor Y
+  have : HasColimit ((asEquivalence Φ).functor ⋙
+    CostructuredArrow.proj (L ⋙ E.functor) (E.functor.obj Y) ⋙ F) :=
+    (inferInstance : HasPointwiseLeftKanExtensionAt L F Y)
+  exact hasColimit_of_equivalence_comp (asEquivalence Φ)
+
+lemma hasPointwiseLeftKanExtensionAt_iff_of_equivalence
+    (E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y') :
+    HasPointwiseLeftKanExtensionAt L F Y ↔
+      HasPointwiseLeftKanExtensionAt L' F Y' := by
+  constructor
+  · intro
+    exact hasPointwiseLeftKanExtensionAt_of_equivalence L L' F E eL Y Y' e
+  · intro
+    exact hasPointwiseLeftKanExtensionAt_of_equivalence L' L F E.symm
+      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
+        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
+      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)
+
+lemma hasPointwiseRightKanExtensionAt_of_equivalence
+    (E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y')
+    [HasPointwiseRightKanExtensionAt L F Y] :
+    HasPointwiseRightKanExtensionAt L' F Y' := by
+  rw [← hasPointwiseRightKanExtensionAt_iff_of_natIso F eL,
+    hasPointwiseRightKanExtensionAt_iff_of_iso _ F e.symm]
+  let Φ := StructuredArrow.post Y L E.functor
+  have : HasLimit ((asEquivalence Φ).functor ⋙
+    StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F) :=
+    (inferInstance : HasPointwiseRightKanExtensionAt L F Y)
+  exact hasLimit_of_equivalence_comp (asEquivalence Φ)
+
+lemma hasPointwiseRightKanExtensionAt_iff_of_equivalence
+    (E : D ≌ D') (eL : L ⋙ E.functor ≅ L') (Y : D) (Y' : D') (e : E.functor.obj Y ≅ Y') :
+    HasPointwiseRightKanExtensionAt L F Y ↔
+      HasPointwiseRightKanExtensionAt L' F Y' := by
+  constructor
+  · intro
+    exact hasPointwiseRightKanExtensionAt_of_equivalence L L' F E eL Y Y' e
+  · intro
+    exact hasPointwiseRightKanExtensionAt_of_equivalence L' L F E.symm
+      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
+        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
+      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)
+
 namespace LeftExtension
 
 variable {F L}
@@ -98,6 +201,27 @@ lemma IsPointwiseLeftKanExtensionAt.isIso_hom_app
     IsIso (E.hom.app X) := by
   simpa using h.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal
 
+/-- The condition of being a pointwise left Kan extension at an object `Y` is
+unchanged by replacing `Y` by an isomorphic object `Y'`. -/
+def isPointwiseLeftKanExtensionAtOfIso'
+    {Y : D} (hY : E.IsPointwiseLeftKanExtensionAt Y) {Y' : D} (e : Y ≅ Y') :
+    E.IsPointwiseLeftKanExtensionAt Y' :=
+  IsColimit.ofIsoColimit (hY.whiskerEquivalence (CostructuredArrow.mapIso e.symm))
+    (Cocones.ext (E.right.mapIso e))
+
+/-- The condition of being a pointwise left Kan extension at an object `Y` is
+unchanged by replacing `Y` by an isomorphic object `Y'`. -/
+def isPointwiseLeftKanExtensionAtEquivOfIso' {Y Y' : D} (e : Y ≅ Y') :
+    E.IsPointwiseLeftKanExtensionAt Y ≃ E.IsPointwiseLeftKanExtensionAt Y' where
+  toFun h := E.isPointwiseLeftKanExtensionAtOfIso' h e
+  invFun h := E.isPointwiseLeftKanExtensionAtOfIso' h e.symm
+  left_inv h := by
+    dsimp only [IsPointwiseLeftKanExtensionAt]
+    apply Subsingleton.elim
+  right_inv h := by
+    dsimp only [IsPointwiseLeftKanExtensionAt]
+    apply Subsingleton.elim
+
 namespace IsPointwiseLeftKanExtensionAt
 
 variable {E} {Y : D} (h : E.IsPointwiseLeftKanExtensionAt Y)
@@ -235,6 +359,27 @@ lemma IsPointwiseRightKanExtensionAt.isIso_hom_app
     IsIso (E.hom.app X) := by
   simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial
 
+/-- The condition of being a pointwise right Kan extension at an object `Y` is
+unchanged by replacing `Y` by an isomorphic object `Y'`. -/
+def isPointwiseRightKanExtensionAtOfIso'
+    {Y : D} (hY : E.IsPointwiseRightKanExtensionAt Y) {Y' : D} (e : Y ≅ Y') :
+    E.IsPointwiseRightKanExtensionAt Y' :=
+  IsLimit.ofIsoLimit (hY.whiskerEquivalence (StructuredArrow.mapIso e.symm))
+    (Cones.ext (E.left.mapIso e))
+
+/-- The condition of being a pointwise right Kan extension at an object `Y` is
+unchanged by replacing `Y` by an isomorphic object `Y'`. -/
+def isPointwiseRightKanExtensionAtEquivOfIso' {Y Y' : D} (e : Y ≅ Y') :
+    E.IsPointwiseRightKanExtensionAt Y ≃ E.IsPointwiseRightKanExtensionAt Y' where
+  toFun h := E.isPointwiseRightKanExtensionAtOfIso' h e
+  invFun h := E.isPointwiseRightKanExtensionAtOfIso' h e.symm
+  left_inv h := by
+    dsimp only [IsPointwiseRightKanExtensionAt]
+    apply Subsingleton.elim
+  right_inv h := by
+    dsimp only [IsPointwiseRightKanExtensionAt]
+    apply Subsingleton.elim
+
 namespace IsPointwiseRightKanExtensionAt
 
 variable {E} {Y : D} (h : E.IsPointwiseRightKanExtensionAt Y)

Mathlib/CategoryTheory/Limits/HasLimits.lean

@@ -433,18 +433,23 @@ theorem limit.pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤
 
 open CategoryTheory.Equivalence
 
-instance hasLimitEquivalenceComp (e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F) :=
+instance hasLimit_equivalence_comp (e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F) :=
   HasLimit.mk
     { cone := Cone.whisker e.functor (limit.cone F)
       isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) e }
 
 -- not entirely sure why this is needed
 /-- If a `E ⋙ F` has a limit, and `E` is an equivalence, we can construct a limit of `F`.
 -/
-theorem hasLimitOfEquivalenceComp (e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F := by
-  haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimitEquivalenceComp e.symm
+theorem hasLimit_of_equivalence_comp (e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F := by
+  haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimit_equivalence_comp e.symm
   apply hasLimit_of_iso (e.invFunIdAssoc F)
 
+@[deprecated (since := "2025-03-02")] alias hasLimitEquivalenceComp :=
+  hasLimit_equivalence_comp
+@[deprecated (since := "2025-03-02")] alias hasLimitOfEquivalenceComp :=
+  hasLimit_of_equivalence_comp
+
 -- `hasLimitCompEquivalence` and `hasLimitOfCompEquivalence`
 -- are proved in `CategoryTheory/Adjunction/Limits.lean`.
 section LimFunctor
@@ -560,7 +565,7 @@ theorem hasLimitsOfShape_of_equivalence {J' : Type u₂} [Category.{v₂} J'] (e
     [HasLimitsOfShape J C] : HasLimitsOfShape J' C := by
   constructor
   intro F
-  apply hasLimitOfEquivalenceComp e
+  apply hasLimit_of_equivalence_comp e
 
 variable (C)
 

Mathlib/CategoryTheory/Limits/Opposites.lean

@@ -558,7 +558,7 @@ variable [HasCoproduct Z]
 instance : HasLimit (Discrete.functor Z).op := hasLimit_op_of_hasColimit (Discrete.functor Z)
 
 instance : HasLimit ((Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op) :=
-  hasLimitEquivalenceComp (Discrete.opposite α).symm
+  hasLimit_equivalence_comp (Discrete.opposite α).symm
 
 instance : HasProduct (op <| Z ·) := hasLimit_of_iso
   ((Discrete.natIsoFunctor ≪≫ Discrete.natIso (fun _ ↦ by rfl)) :

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -102,7 +102,7 @@ lemma hasCoproduct_of_equiv_of_iso (f : α → C) (g : β → C)
 lemma hasProduct_of_equiv_of_iso (f : α → C) (g : β → C)
     [HasProduct f] (e : β ≃ α) (iso : ∀ j, g j ≅ f (e j)) : HasProduct g := by
   have : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f) :=
-    hasLimitEquivalenceComp _
+    hasLimit_equivalence_comp _
   have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
     Discrete.natIso (fun ⟨j⟩ => iso j)
   exact hasLimit_of_iso α.symm