[Merged by Bors] - feat(CategoryTheory): transport Kan extensions via equivalences

Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean

@@ -5,6 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Comma.StructuredArrow
 import Mathlib.CategoryTheory.Limits.Shapes.Equivalence
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
 
 /-!
 # Kan extensions
@@ -39,7 +40,8 @@ open Category Limits
 
 namespace Functor
 
-variable {C H D D' : Type*} [Category C] [Category H] [Category D] [Category D']
+variable {C C' H H' D D' : Type*} [Category C] [Category C'] [Category H] [Category H']
+  [Category D] [Category D']
 
 /-- Given two functors `L : C ⥤ D` and `F : C ⥤ H`, this is the category of functors
 `F' : H ⥤ D` equipped with a natural transformation `L ⋙ F' ⟶ F`. -/
@@ -265,35 +267,145 @@ end
 
 section
 
-variable (L L' : C ⥤ D) (iso₁ : L ≅ L') (F F' : C ⥤ H) (e : D ≌ D') (iso₂ : F ≅ F')
+variable {L : C ⥤ D} {L' : C ⥤ D'} (G : D ⥤ D') (e : L ⋙ G ≅ L') (F : C ⥤ H)
 
-/-- The equivalence of categories `RightExtension (L ⋙ e.functor) F ≌ RightExtension L F`
-when `e` is an equivalence. -/
-noncomputable def rightExtensionEquivalenceOfPostcomp₁ :
-    RightExtension (L ⋙ e.functor) F ≌ RightExtension L F := by
-  have := CostructuredArrow.isEquivalence_pre ((whiskeringLeft D D' H).obj e.functor)
-    ((whiskeringLeft C D H).obj L) F
-  exact Functor.asEquivalence (CostructuredArrow.pre ((whiskeringLeft D D' H).obj e.functor)
-    ((whiskeringLeft C D H).obj L) F)
+/-- The functor `LeftExtension L' F ⥤ LeftExtension L F` induced by an isomorphism
+`L ⋙ G ≅ L'`. -/
+@[simps!]
+def LeftExtension.postcomp₁ : LeftExtension L' F ⥤ LeftExtension L F :=
+  StructuredArrow.map₂ (F := (whiskeringLeft D D' H).obj G) (G := 𝟭 _) (𝟙 _)
+    ((whiskeringLeft C D' H).map e.inv)
 
-lemma hasRightExtension_iff_postcomp₁ :
-    HasRightKanExtension L F ↔ HasRightKanExtension (L ⋙ e.functor) F :=
-  (rightExtensionEquivalenceOfPostcomp₁ L F e).symm.hasTerminal_iff
-
-/-- The equivalence of categories `LeftExtension (L ⋙ e.functor) F ≌ LeftExtension L F`
-when `e` is an equivalence. -/
-noncomputable def leftExtensionEquivalenceOfPostcomp₁ :
-    LeftExtension (L ⋙ e.functor) F ≌ LeftExtension L F := by
-  have := StructuredArrow.isEquivalence_pre F ((whiskeringLeft D D' H).obj e.functor)
-    ((whiskeringLeft C D H).obj L)
-  exact Functor.asEquivalence (StructuredArrow.pre F ((whiskeringLeft D D' H).obj e.functor)
-    ((whiskeringLeft C D H).obj L))
+/-- The functor `RightExtension L' F ⥤ RightExtension L F` induced by an isomorphism
+`L ⋙ G ≅ L'`. -/
+@[simps!]
+def RightExtension.postcomp₁ : RightExtension L' F ⥤ RightExtension L F :=
+  CostructuredArrow.map₂ (F := (whiskeringLeft D D' H).obj G) (G := 𝟭 _)
+    ((whiskeringLeft C D' H).map e.hom) (𝟙 _)
+
+variable [IsEquivalence G]
+
+noncomputable instance : IsEquivalence (LeftExtension.postcomp₁ G e F) := by
+  apply StructuredArrow.isEquivalenceMap₂
 
+noncomputable instance : IsEquivalence (RightExtension.postcomp₁ G e F) := by
+  apply CostructuredArrow.isEquivalenceMap₂
+
+variable {G} in
 lemma hasLeftExtension_iff_postcomp₁ :
-    HasLeftKanExtension L F ↔ HasLeftKanExtension (L ⋙ e.functor) F :=
-  (leftExtensionEquivalenceOfPostcomp₁ L F e).symm.hasInitial_iff
+    HasLeftKanExtension L' F ↔ HasLeftKanExtension L F :=
+  (LeftExtension.postcomp₁ G e F).asEquivalence.hasInitial_iff
+
+variable {G} in
+lemma hasRightExtension_iff_postcomp₁ :
+    HasRightKanExtension L' F ↔ HasRightKanExtension L F :=
+  (RightExtension.postcomp₁ G e F).asEquivalence.hasTerminal_iff
+
+/-- Given an isomorphism `e : L ⋙ G ≅ L'`, a left extension of `F` along `L'` is universal
+iff the corresponding left extension of `L` along `L` is. -/
+noncomputable def LeftExtension.isUniversalPostcomp₁Equiv (ex : LeftExtension L' F) :
+    ex.IsUniversal ≃ ((LeftExtension.postcomp₁ G e F).obj ex).IsUniversal := by
+  apply IsInitial.isInitialIffObj (LeftExtension.postcomp₁ G e F)
+
+/-- Given an isomorphism `e : L ⋙ G ≅ L'`, a right extension of `F` along `L'` is universal
+iff the corresponding right extension of `L` along `L` is. -/
+noncomputable def RightExtension.isUniversalPostcomp₁Equiv (ex : RightExtension L' F) :
+    ex.IsUniversal ≃ ((RightExtension.postcomp₁ G e F).obj ex).IsUniversal := by
+  apply IsTerminal.isTerminalIffObj (RightExtension.postcomp₁ G e F)
+
+variable {F F'}
+
+lemma isLeftKanExtension_iff_postcomp₁ (α : F ⟶ L' ⋙ F') :
+    F'.IsLeftKanExtension α ↔ (G ⋙ F').IsLeftKanExtension
+      (α ≫ whiskerRight e.inv _ ≫ (Functor.associator _ _ _).hom) := by
+  let eq : (LeftExtension.mk _ α).IsUniversal ≃
+      (LeftExtension.mk _
+        (α ≫ whiskerRight e.inv _ ≫ (Functor.associator _ _ _).hom)).IsUniversal :=
+    (LeftExtension.isUniversalPostcomp₁Equiv G e F _).trans
+    (IsInitial.equivOfIso (StructuredArrow.isoMk (Iso.refl _)))
+  constructor
+  · exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
+  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩
+
+lemma isRightKanExtension_iff_postcomp₁ (α : L' ⋙ F' ⟶ F) :
+    F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension
+      ((Functor.associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α) := by
+  let eq : (RightExtension.mk _ α).IsUniversal ≃
+    (RightExtension.mk _
+      ((Functor.associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)).IsUniversal :=
+  (RightExtension.isUniversalPostcomp₁Equiv G e F _).trans
+    (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))
+  constructor
+  · exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
+  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩
+
+end
+
+section
+
+variable (L : C ⥤ D) (F : C ⥤ H) (F' : D ⥤ H) (G : C' ⥤ C)
+
+/-- The functor `LeftExtension L F ⥤ LeftExtension (G ⋙ L) (G ⋙ F)`
+obtained by precomposition. -/
+@[simps!]
+def LeftExtension.precomp : LeftExtension L F ⥤ LeftExtension (G ⋙ L) (G ⋙ F) :=
+  StructuredArrow.map₂ (F := 𝟭 _) (G := (whiskeringLeft C' C H).obj G) (𝟙 _) (𝟙 _)
+
+/-- The functor `RightExtension L F ⥤ RightExtension (G ⋙ L) (G ⋙ F)`
+obtained by precomposition. -/
+@[simps!]
+def RightExtension.precomp : RightExtension L F ⥤ RightExtension (G ⋙ L) (G ⋙ F) :=
+  CostructuredArrow.map₂ (F := 𝟭 _) (G := (whiskeringLeft C' C H).obj G) (𝟙 _) (𝟙 _)
+
+variable [IsEquivalence G]
+
+noncomputable instance : IsEquivalence (LeftExtension.precomp L F G) := by
+  apply StructuredArrow.isEquivalenceMap₂
+
+noncomputable instance : IsEquivalence (RightExtension.precomp L F G) := by
+  apply CostructuredArrow.isEquivalenceMap₂
+
+/-- If `G` is an equivalence, then a left extension of `F` along `L` is universal iff
+the corresponding left extension of `G ⋙ F` along `G ⋙ L` is. -/
+noncomputable def LeftExtension.isUniversalPrecompEquiv (e : LeftExtension L F) :
+    e.IsUniversal ≃ ((LeftExtension.precomp L F G).obj e).IsUniversal := by
+  apply IsInitial.isInitialIffObj (LeftExtension.precomp L F G)
+
+/-- If `G` is an equivalence, then a right extension of `F` along `L` is universal iff
+the corresponding left extension of `G ⋙ F` along `G ⋙ L` is. -/
+noncomputable def RightExtension.isUniversalPrecompEquiv (e : RightExtension L F) :
+    e.IsUniversal ≃ ((RightExtension.precomp L F G).obj e).IsUniversal := by
+  apply IsTerminal.isTerminalIffObj (RightExtension.precomp L F G)
+
+variable {F L}
+
+lemma isLeftKanExtension_iff_precomp (α : F ⟶ L ⋙ F') :
+    F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension
+      (whiskerLeft G α ≫ (Functor.associator _ _ _).inv) := by
+  let eq : (LeftExtension.mk _ α).IsUniversal ≃ (LeftExtension.mk _
+      (whiskerLeft G α ≫ (Functor.associator _ _ _).inv)).IsUniversal :=
+    (LeftExtension.isUniversalPrecompEquiv L F G _).trans
+    (IsInitial.equivOfIso (StructuredArrow.isoMk (Iso.refl _)))
+  constructor
+  · exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
+  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩
+
+lemma isRightKanExtension_iff_precomp (α : L ⋙ F' ⟶ F) :
+    F'.IsRightKanExtension α ↔
+      F'.IsRightKanExtension ((Functor.associator _ _ _).hom ≫ whiskerLeft G α) := by
+  let eq : (RightExtension.mk _ α).IsUniversal ≃ (RightExtension.mk _
+      ((Functor.associator _ _ _).hom ≫ whiskerLeft G α)).IsUniversal :=
+    (RightExtension.isUniversalPrecompEquiv L F G _).trans
+    (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))
+  constructor
+  · exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
+  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩
 
-variable {L L'}
+end
+
+section
+
+variable {L L' : C ⥤ D} (iso₁ : L ≅ L') (F : C ⥤ H)
 
 /-- The equivalence `RightExtension L F ≌ RightExtension L' F` induced by
 a natural isomorphism `L ≅ L'`. -/
@@ -311,7 +423,11 @@ def leftExtensionEquivalenceOfIso₁ : LeftExtension L F ≌ LeftExtension L' F
 lemma hasLeftExtension_iff_of_iso₁ : HasLeftKanExtension L F ↔ HasLeftKanExtension L' F :=
   (leftExtensionEquivalenceOfIso₁ iso₁ F).hasInitial_iff
 
-variable (L) {F F'}
+end
+
+section
+
+variable (L : C ⥤ D) {F F' : C ⥤ H} (iso₂ : F ≅ F')
 
 /-- The equivalence `RightExtension L F ≌ RightExtension L F'` induced by
 a natural isomorphism `F ≅ F'`. -/
@@ -331,6 +447,54 @@ lemma hasLeftExtension_iff_of_iso₂ : HasLeftKanExtension L F ↔ HasLeftKanExt
 
 end
 
+section
+
+variable {L : C ⥤ D} {F₁ F₂ : C ⥤ H}
+
+/-- When two left extensions `α₁ : LeftExtension L F₁` and `α₂ : LeftExtension L F₂`
+are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
+then `α₁` is universal iff `α₂` is. -/
+noncomputable def LeftExtension.isUniversalEquivOfIso₂
+    (α₁ : LeftExtension L F₁) (α₂ : LeftExtension L F₂) (e : F₁ ≅ F₂)
+    (e' : α₁.right ≅ α₂.right)
+    (h : α₁.hom ≫ whiskerLeft L e'.hom = e.hom ≫ α₂.hom) :
+    α₁.IsUniversal ≃ α₂.IsUniversal :=
+  (IsInitial.isInitialIffObj (leftExtensionEquivalenceOfIso₂ L e).functor α₁).trans
+    (IsInitial.equivOfIso (StructuredArrow.isoMk e'
+      (by simp [leftExtensionEquivalenceOfIso₂, h])))
+
+lemma isLeftKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : F₁ ⟶ L ⋙ F₁') (α₂ : F₂ ⟶ L ⋙ F₂')
+    (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') (h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂) :
+    F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂ := by
+  let eq := LeftExtension.isUniversalEquivOfIso₂ (LeftExtension.mk _ α₁)
+    (LeftExtension.mk _ α₂) e e' h
+  constructor
+  · exact fun _ => ⟨⟨eq.1 (isUniversalOfIsLeftKanExtension F₁' α₁)⟩⟩
+  · exact fun _ => ⟨⟨eq.2 (isUniversalOfIsLeftKanExtension F₂' α₂)⟩⟩
+
+/-- When two right extensions `α₁ : RightExtension L F₁` and `α₂ : RightExtension L F₂`
+are essentially the same via an isomorphism of functors `F₁ ≅ F₂`,
+then `α₁` is universal iff `α₂` is. -/
+noncomputable def RightExtension.isUniversalEquivOfIso₂
+    (α₁ : RightExtension L F₁) (α₂ : RightExtension L F₂) (e : F₁ ≅ F₂)
+    (e' : α₁.left ≅ α₂.left)
+    (h : whiskerLeft L e'.hom ≫ α₂.hom = α₁.hom ≫ e.hom) :
+    α₁.IsUniversal ≃ α₂.IsUniversal :=
+  (IsTerminal.isTerminalIffObj (rightExtensionEquivalenceOfIso₂ L e).functor α₁).trans
+    (IsTerminal.equivOfIso (CostructuredArrow.isoMk e'
+      (by simp [rightExtensionEquivalenceOfIso₂, h])))
+
+lemma isRightKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : L ⋙ F₁' ⟶ F₁) (α₂ : L ⋙ F₂' ⟶ F₂)
+    (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') (h : whiskerLeft L e'.hom ≫ α₂ = α₁ ≫ e.hom) :
+    F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂ := by
+  let eq := RightExtension.isUniversalEquivOfIso₂ (RightExtension.mk _ α₁)
+    (RightExtension.mk _ α₂) e e' h
+  constructor
+  · exact fun _ => ⟨⟨eq.1 (isUniversalOfIsRightKanExtension F₁' α₁)⟩⟩
+  · exact fun _ => ⟨⟨eq.2 (isUniversalOfIsRightKanExtension F₂' α₂)⟩⟩
+
+end
+
 end Functor
 
 end CategoryTheory

Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean

@@ -96,6 +96,14 @@ def IsTerminal.ofIso {Y Z : C} (hY : IsTerminal Y) (i : Y ≅ Z) : IsTerminal Z
       inv := { hom := i.inv } }
 #align category_theory.limits.is_terminal.of_iso CategoryTheory.Limits.IsTerminal.ofIso
 
+/-- If `X` and `Y` are isomorphic, then `X` is terminal iff `Y` is. -/
+def IsTerminal.equivOfIso {X Y : C} (e : X ≅ Y) :
+    IsTerminal X ≃ IsTerminal Y where
+  toFun h := IsTerminal.ofIso h e
+  invFun h := IsTerminal.ofIso h e.symm
+  left_inv _ := Subsingleton.elim _ _
+  right_inv _ := Subsingleton.elim _ _
+
 /-- An object `X` is initial iff for every `Y` there is a unique morphism `X ⟶ Y`. -/
 def isInitialEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (X : C) :
     IsColimit (⟨X, ⟨by aesop_cat, by aesop_cat⟩⟩ : Cocone F) ≃ ∀ Y : C, Unique (X ⟶ Y) where
@@ -137,6 +145,14 @@ def IsInitial.ofIso {X Y : C} (hX : IsInitial X) (i : X ≅ Y) : IsInitial Y :=
       inv := { hom := i.inv } }
 #align category_theory.limits.is_initial.of_iso CategoryTheory.Limits.IsInitial.ofIso
 
+/-- If `X` and `Y` are isomorphic, then `X` is initial iff `Y` is. -/
+def IsInitial.equivOfIso {X Y : C} (e : X ≅ Y) :
+    IsInitial X ≃ IsInitial Y where
+  toFun h := IsInitial.ofIso h e
+  invFun h := IsInitial.ofIso h e.symm
+  left_inv _ := Subsingleton.elim _ _
+  right_inv _ := Subsingleton.elim _ _
+
 /-- Give the morphism to a terminal object from any other. -/
 def IsTerminal.from {X : C} (t : IsTerminal X) (Y : C) : Y ⟶ X :=
   t.lift (asEmptyCone Y)