[Merged by Bors] - feat(CategoryTheory/Functor): refactoring Lan

Mathlib.lean

@@ -1061,7 +1061,9 @@ import Mathlib.CategoryTheory.Functor.Flat
 import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
+import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
 import Mathlib.CategoryTheory.Functor.KanExtension.Basic
+import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
 import Mathlib.CategoryTheory.Functor.ReflectsIso
 import Mathlib.CategoryTheory.Functor.Trifunctor
 import Mathlib.CategoryTheory.Galois.Basic

Mathlib/CategoryTheory/Elements.lean

@@ -47,6 +47,8 @@ def Functor.Elements (F : C ⥤ Type w) :=
   Σc : C, F.obj c
 #align category_theory.functor.elements CategoryTheory.Functor.Elements
 
+abbrev Functor.elementsMk (F : C ⥤ Type w) (X : C) (x : F.obj X) : F.Elements := ⟨X, x⟩
+
 -- porting note: added because Sigma.ext would be triggered automatically
 lemma Functor.Elements.ext {F : C ⥤ Type w} (x y : F.Elements) (h₁ : x.fst = y.fst)
     (h₂ : F.map (eqToHom h₁) x.snd = y.snd) : x = y := by

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -282,34 +282,28 @@ section SmallCategory
 variable {C D : Type u₁} [SmallCategory C] [SmallCategory D] (E : Type u₂) [Category.{u₁} E]
 
 
+-- this should be moved to `CategoryTheory.Functor.KanExtension.Adjunction`
 /-- (Implementation)
 The evaluation of `Lan F` at `X` is the colimit over the costructured arrows over `X`.
 -/
 noncomputable def lanEvaluationIsoColim (F : C ⥤ D) (X : D)
     [∀ X : D, HasColimitsOfShape (CostructuredArrow F X) E] :
-    lan F ⋙ (evaluation D E).obj X ≅
+    F.lan ⋙ (evaluation D E).obj X ≅
       (whiskeringLeft _ _ E).obj (CostructuredArrow.proj F X) ⋙ colim :=
-  NatIso.ofComponents (fun G => colim.mapIso (Iso.refl _))
-    (by
-      intro G H i
-      -- porting note: was `ext` in lean 3
-      -- Now `ext` can't see that `lan` is a colimit.
-      -- Uncertain whether it makes sense to add another `@[ext]` lemma.
-      -- See https://github.com/leanprover-community/mathlib4/issues/5229
-      apply colimit.hom_ext
-      intro j
-      simp only [Functor.comp_map, Functor.mapIso_refl, evaluation_obj_map, whiskeringLeft_obj_map,
-        lan_map_app, colimit.ι_desc_assoc, Category.comp_id, Category.assoc]
-      -- porting note: this deals with the fact that the type of `lan_map_app` has changed
-      -- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/change.20in.20behaviour.20with.20.60simps.60/near/354350606
-      erw [show ((Lan.equiv F H (Lan.loc F H)) (𝟙 (Lan.loc F H))).app j.left =
-        colimit.ι (Lan.diagram F H (F.obj j.left))
-        (CostructuredArrow.mk (𝟙 (F.obj j.left))) by apply Category.comp_id]
-      erw [colimit.ι_pre_assoc (Lan.diagram F H X) (CostructuredArrow.map j.hom), Category.id_comp,
-        Category.comp_id, colimit.ι_map]
-      rcases j with ⟨j_left, ⟨⟨⟩⟩, j_hom⟩
-      congr
-      rw [CostructuredArrow.map_mk, Category.id_comp, CostructuredArrow.mk])
+  NatIso.ofComponents (fun G =>
+    IsColimit.coconePointUniqueUpToIso (Functor.isPointwiseLeftKanExtensionLanUnit F G X)
+    (colimit.isColimit _)) (fun {G₁ G₂} φ => by
+      apply (Functor.isPointwiseLeftKanExtensionLanUnit F G₁ X).hom_ext
+      intro T
+      have h₁ := fun (G : C ⥤ E) => IsColimit.comp_coconePointUniqueUpToIso_hom
+        (Functor.isPointwiseLeftKanExtensionLanUnit F G X) (colimit.isColimit _) T
+      have h₂ := congr_app (F.lanUnit.naturality φ) T.left
+      dsimp at h₁ h₂ ⊢
+      simp only [Category.assoc] at h₁ ⊢
+      rw [reassoc_of% h₁, NatTrans.naturality_assoc, ← reassoc_of% h₂, h₁,
+        ι_colimMap, whiskerLeft_app]
+      rfl)
+
 set_option linter.uppercaseLean3 false in
 #align category_theory.Lan_evaluation_iso_colim CategoryTheory.lanEvaluationIsoColim
 
@@ -323,10 +317,10 @@ variable [PreservesLimits (forget E)]
 `Lan F.op` that takes presheaves over `C` to presheaves over `D` preserves finite limits.
 -/
 noncomputable instance lanPreservesFiniteLimitsOfFlat (F : C ⥤ D) [RepresentablyFlat F] :
-    PreservesFiniteLimits (lan F.op : _ ⥤ Dᵒᵖ ⥤ E) := by
+    PreservesFiniteLimits (F.op.lan : _ ⥤ Dᵒᵖ ⥤ E) := by
   apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
   intro J _ _; skip
-  apply preservesLimitsOfShapeOfEvaluation (lan F.op : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J
+  apply preservesLimitsOfShapeOfEvaluation (F.op.lan : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J
   intro K
   haveI : IsFiltered (CostructuredArrow F.op K) :=
     IsFiltered.of_equivalence (structuredArrowOpEquivalence F (unop K))
@@ -335,25 +329,25 @@ set_option linter.uppercaseLean3 false in
 #align category_theory.Lan_preserves_finite_limits_of_flat CategoryTheory.lanPreservesFiniteLimitsOfFlat
 
 instance lan_flat_of_flat (F : C ⥤ D) [RepresentablyFlat F] :
-    RepresentablyFlat (lan F.op : _ ⥤ Dᵒᵖ ⥤ E) :=
+    RepresentablyFlat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ E) :=
   flat_of_preservesFiniteLimits _
 set_option linter.uppercaseLean3 false in
 #align category_theory.Lan_flat_of_flat CategoryTheory.lan_flat_of_flat
 
 variable [HasFiniteLimits C]
 
 noncomputable instance lanPreservesFiniteLimitsOfPreservesFiniteLimits (F : C ⥤ D)
-    [PreservesFiniteLimits F] : PreservesFiniteLimits (lan F.op : _ ⥤ Dᵒᵖ ⥤ E) := by
+    [PreservesFiniteLimits F] : PreservesFiniteLimits (F.op.lan : _ ⥤ Dᵒᵖ ⥤ E) := by
   haveI := flat_of_preservesFiniteLimits F
   infer_instance
 set_option linter.uppercaseLean3 false in
 #align category_theory.Lan_preserves_finite_limits_of_preserves_finite_limits CategoryTheory.lanPreservesFiniteLimitsOfPreservesFiniteLimits
 
 theorem flat_iff_lan_flat (F : C ⥤ D) :
-    RepresentablyFlat F ↔ RepresentablyFlat (lan F.op : _ ⥤ Dᵒᵖ ⥤ Type u₁) :=
+    RepresentablyFlat F ↔ RepresentablyFlat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁) :=
   ⟨fun H => inferInstance, fun H => by
     skip
-    haveI := preservesFiniteLimitsOfFlat (lan F.op : _ ⥤ Dᵒᵖ ⥤ Type u₁)
+    haveI := preservesFiniteLimitsOfFlat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁)
     haveI : PreservesFiniteLimits F := by
       apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}
       intros; skip; apply preservesLimitOfLanPreservesLimit
@@ -365,7 +359,7 @@ set_option linter.uppercaseLean3 false in
 `Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves finite limits.
 -/
 noncomputable def preservesFiniteLimitsIffLanPreservesFiniteLimits (F : C ⥤ D) :
-    PreservesFiniteLimits F ≃ PreservesFiniteLimits (lan F.op : _ ⥤ Dᵒᵖ ⥤ Type u₁) where
+    PreservesFiniteLimits F ≃ PreservesFiniteLimits (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁) where
   toFun _ := inferInstance
   invFun _ := by
     apply preservesFiniteLimitsOfPreservesFiniteLimitsOfSize.{u₁}

Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

@@ -0,0 +1,123 @@
+-- refactor of Limits.KanExtension
+import Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
+
+namespace CategoryTheory
+
+open Category
+
+namespace Limits
+
+namespace IsColimit
+
+variable {J C : Type*} [Category J] [Category C] {F : J ⥤ C} {c : Cocone F}
+  (hc : IsColimit c)
+
+lemma isIso_ι_app_of_isTerminal (X : J) (hX : IsTerminal X) : IsIso (c.ι.app X) := by
+  change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom
+  infer_instance
+
+end IsColimit
+
+end Limits
+
+namespace Functor
+
+variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
+  {E : Type*} [Category E] [∀ (G : C ⥤ E), HasLeftKanExtension F G]
+
+noncomputable def lan : (C ⥤ E) ⥤ (D ⥤ E) where
+  obj G := leftKanExtension F G
+  map {G₁ G₂} φ := descOfIsLeftKanExtension _ (leftKanExtensionUnit F G₁) _
+    (φ ≫ leftKanExtensionUnit F G₂)
+
+noncomputable def lanUnit : (𝟭 (C ⥤ E)) ⟶ lan F ⋙ (whiskeringLeft C D E).obj F where
+  app G := leftKanExtensionUnit F G
+  naturality {G₁ G₂} φ := by ext; simp [lan]
+
+instance (G : C ⥤ E) : ((lan F).obj G).IsLeftKanExtension ((lanUnit F).app G) := by
+  dsimp [lan, lanUnit]
+  infer_instance
+
+noncomputable def isPointwiseLeftKanExtensionLanUnit
+    (G : C ⥤ E) [HasPointwiseLeftKanExtension F G] :
+    (LeftExtension.mk _ ((lanUnit F).app G)).IsPointwiseLeftKanExtension := by
+  have : HasPointwiseLeftKanExtension F ((𝟭 (C ⥤ E)).obj G) := by
+    dsimp
+    infer_instance
+  exact isPointwiseLeftKanExtensionOfIsLeftKanExtension _ ((lanUnit F).app G)
+
+variable {F} in
+noncomputable def homEquivOfIsLeftKanExtension
+    {G : C ⥤ E} (G' : D ⥤ E) (α : G ⟶ F ⋙ G') (H : D ⥤ E)
+    [G'.IsLeftKanExtension α] : (G' ⟶ H) ≃ (G ⟶ F ⋙ H) where
+  toFun β := α ≫ whiskerLeft _ β
+  invFun β := descOfIsLeftKanExtension _ α _ β
+  left_inv β := Functor.hom_ext_of_isLeftKanExtension _ α _ _ (by aesop_cat)
+  right_inv := by aesop_cat
+
+variable (E) in
+noncomputable def Lan.adjunction : lan F ⊣ (whiskeringLeft _ _ E).obj F :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv := fun G H => homEquivOfIsLeftKanExtension _ ((lanUnit F).app G) H
+      homEquiv_naturality_left_symm := fun {G₁ G₂ H} f α =>
+        hom_ext_of_isLeftKanExtension _  ((lanUnit F).app G₁) _ _ (by
+          ext X
+          dsimp [homEquivOfIsLeftKanExtension]
+          rw [descOfIsLeftKanExtension_fac_app, NatTrans.comp_app, ← assoc]
+          have h := congr_app ((lanUnit F).naturality f) X
+          dsimp at h ⊢
+          rw [← h, assoc, descOfIsLeftKanExtension_fac_app] )
+      homEquiv_naturality_right := fun {G H₁ H₂} β f => by
+        dsimp [homEquivOfIsLeftKanExtension]
+        rw [assoc] }
+
+variable (E) in
+@[simp]
+lemma Lan.adjunction_unit :
+    (Lan.adjunction F E).unit =
+      lanUnit F := by
+  ext G : 2
+  dsimp [adjunction, homEquivOfIsLeftKanExtension]
+  simp
+
+namespace LeftExtension
+
+namespace IsPointwiseLeftKanExtensionAt
+
+variable {F}
+variable {G : C ⥤ E} (e : LeftExtension F G) {X : C}
+    (he : e.IsPointwiseLeftKanExtensionAt (F.obj X))
+
+lemma isIso_hom_app [Full F] [Faithful F] : IsIso (e.hom.app X) := by
+  simpa using he.isIso_ι_app_of_isTerminal _ CostructuredArrow.mkIdTerminal
+
+end IsPointwiseLeftKanExtensionAt
+
+end LeftExtension
+
+section
+
+variable [Full F] [Faithful F]
+
+instance (G : C ⥤ E) (X : C) [HasPointwiseLeftKanExtension F G] :
+    IsIso (((Lan.adjunction F E).unit.app G).app X) := by
+  simpa using (isPointwiseLeftKanExtensionLanUnit F G (F.obj X)).isIso_hom_app
+
+instance (G : C ⥤ E) [HasPointwiseLeftKanExtension F G] :
+    IsIso ((Lan.adjunction F E).unit.app G) :=
+  NatIso.isIso_of_isIso_app _
+
+instance coreflective [∀ (G : C ⥤ E), HasPointwiseLeftKanExtension F G] :
+    IsIso ((Lan.adjunction F E).unit) :=
+  NatIso.isIso_of_isIso_app _
+
+instance coreflective' [∀ (G : C ⥤ E), HasPointwiseLeftKanExtension F G] :
+    IsIso (lanUnit F : (𝟭 (C ⥤ E)) ⟶ _) := by
+  rw [← Lan.adjunction_unit]
+  infer_instance
+
+end
+
+end Functor
+
+end CategoryTheory

Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean

@@ -26,12 +26,10 @@ are obtained as `leftKanExtension L F` and `rightKanExtension L F`.
 
 ## TODO (@joelriou)
 
-* define a condition expressing that a functor is a pointwise Kan extension
-* refactor the file `CategoryTheory.Limits.KanExtension` using this new general API
 * define left/right derived functors as particular cases of Kan extensions
 
 ## References
-https://ncatlab.org/nlab/show/Kan+extension
+* https://ncatlab.org/nlab/show/Kan+extension
 
 -/
 
@@ -302,6 +300,20 @@ lemma hasLeftExtension_iff_of_iso₂ : HasLeftKanExtension L F ↔ HasLeftKanExt
 
 end
 
+section
+
+variable (F₁ F₂ : H ⥤ D) {L : C ⥤ H} {F : C ⥤ D} (α₁ : F ⟶ L ⋙ F₁) (α₂ : F ⟶ L ⋙ F₂)
+
+@[simps]
+noncomputable def leftKanExtensionUnique [F₁.IsLeftKanExtension α₁] [F₂.IsLeftKanExtension α₂] :
+    F₁ ≅ F₂ where
+  hom := F₁.descOfIsLeftKanExtension α₁ F₂ α₂
+  inv := F₂.descOfIsLeftKanExtension α₂ F₁ α₁
+  hom_inv_id := F₁.hom_ext_of_isLeftKanExtension α₁ _ _ (by aesop_cat)
+  inv_hom_id := F₂.hom_ext_of_isLeftKanExtension α₂ _ _ (by aesop_cat)
+
+end
+
 end Functor
 
 end CategoryTheory