feat(CategoryTheory/Functor): refactoring Ran (#14291)

This PR refactors the definition of the right Kan extension functor (`Functor.ran : (C ⥤ E) ⥤ (D ⥤ E)`) which sends a functor to its right Kan extension along a given functor `F : C ⥤ D`. It used to be defined under the existence of certain colimits. It is now part of the general Kan extension API.

The only significant change in this PR is about showing that the right Kan extension functor associated to a cocontinuous functors between sites sends sheaves to sheaves (this is in the file `CategoryTheory.Sites.CoverLifting`). As this functor is no longer based on the limits API, the proofs had to be changed. In the new proof, we proceed directly with sheaves with values in a category `A` rather than translating the sheaf property in terms of sheaves of types.

This PR is the dual counterpart of #10425 which refactored left Kan extensions.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib.lean

@@ -1470,7 +1470,6 @@ import Mathlib.CategoryTheory.Limits.IndYoneda
 import Mathlib.CategoryTheory.Limits.Indization.IndObject
 import Mathlib.CategoryTheory.Limits.IsConnected
 import Mathlib.CategoryTheory.Limits.IsLimit
-import Mathlib.CategoryTheory.Limits.KanExtension
 import Mathlib.CategoryTheory.Limits.Lattice
 import Mathlib.CategoryTheory.Limits.MonoCoprod
 import Mathlib.CategoryTheory.Limits.Opposites

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -476,18 +476,29 @@ def ofNatIsoRight {F : C ⥤ D} {G H : D ⥤ C} (adj : F ⊣ G) (iso : G ≅ H)
 section
 
 variable {E : Type u₃} [ℰ : Category.{v₃} E] {H : D ⥤ E} {I : E ⥤ D}
+  (adj₁ : F ⊣ G) (adj₂ : H ⊣ I)
 
 /-- Composition of adjunctions.
 
 See <https://stacks.math.columbia.edu/tag/0DV0>.
 -/
-def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G where
+def comp : F ⋙ H ⊣ I ⋙ G where
   homEquiv X Z := Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)
   unit := adj₁.unit ≫ (whiskerLeft F <| whiskerRight adj₂.unit G) ≫ (Functor.associator _ _ _).inv
   counit :=
     (Functor.associator _ _ _).hom ≫ (whiskerLeft I <| whiskerRight adj₁.counit H) ≫ adj₂.counit
 #align category_theory.adjunction.comp CategoryTheory.Adjunction.comp
 
+@[simp, reassoc]
+lemma comp_unit_app (X : C) :
+    (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X)) := by
+  simp [Adjunction.comp]
+
+@[simp, reassoc]
+lemma comp_counit_app (X : E) :
+    (adj₁.comp adj₂).counit.app X = H.map (adj₁.counit.app (I.obj X)) ≫ adj₂.counit.app X := by
+  simp [Adjunction.comp]
+
 end
 
 section ConstructLeft

Mathlib/CategoryTheory/Adjunction/Restrict.lean

@@ -23,8 +23,8 @@ variable {C : Type u₁} [Category.{v₁} C]
 variable {D : Type u₂} [Category.{v₂} D]
 variable {C' : Type u₃} [Category.{v₃} C']
 variable {D' : Type u₄} [Category.{v₄} D']
-variable {iC : C ⥤ C'} {iD : D ⥤ D'} (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful)
-  {L' : C' ⥤ D'} {R' : D' ⥤ C'} (adj : L' ⊣ R')
+variable {iC : C ⥤ C'} {iD : D ⥤ D'}
+  {L' : C' ⥤ D'} {R' : D' ⥤ C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful) (hiD : iD.FullyFaithful)
   {L : C ⥤ D} {R : D ⥤ C} (comm1 : iC ⋙ L' ≅ L ⋙ iD) (comm2 : iD ⋙ R' ≅ R ⋙ iC)
 
 /-- If `C` is a full subcategory of `C'` and `D` is a full subcategory of `D'`, then we can restrict
@@ -55,19 +55,19 @@ noncomputable def restrictFullyFaithful : L ⊣ R :=
 
 @[simp, reassoc]
 lemma map_restrictFullyFaithful_unit_app (X : C) :
-    iC.map ((restrictFullyFaithful hiC hiD adj comm1 comm2).unit.app X) =
+    iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) =
     adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) := by
   simp [restrictFullyFaithful]
 
 @[simp, reassoc]
 lemma map_restrictFullyFaithful_counit_app (X : D) :
-    iD.map ((restrictFullyFaithful hiC hiD adj comm1 comm2).counit.app X) =
+    iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
     comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X) := by
   dsimp [restrictFullyFaithful]
   simp
 
 lemma restrictFullyFaithful_homEquiv_apply {X : C} {Y : D} (f : L.obj X ⟶ Y) :
-    (restrictFullyFaithful hiC hiD adj comm1 comm2).homEquiv X Y f =
+    (adj.restrictFullyFaithful hiC hiD comm1 comm2).homEquiv X Y f =
       hiC.preimage (adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫
         R'.map (iD.map f) ≫ comm2.hom.app Y) := by
   simp [restrictFullyFaithful]

Mathlib/CategoryTheory/Closed/Ideal.lean

@@ -152,8 +152,8 @@ def cartesianClosedOfReflective : CartesianClosed D :=
     closed := fun B =>
       { rightAdj :=i ⋙ exp (i.obj B) ⋙ reflector i
         adj := by
-          apply Adjunction.restrictFullyFaithful i.fullyFaithfulOfReflective
-            i.fullyFaithfulOfReflective (exp.adjunction (i.obj B))
+          apply (exp.adjunction (i.obj B)).restrictFullyFaithful i.fullyFaithfulOfReflective
+            i.fullyFaithfulOfReflective
           · symm
             refine NatIso.ofComponents (fun X => ?_) (fun f => ?_)
             · haveI :=

Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

@@ -18,13 +18,6 @@ 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
-- refactor the file `CategoryTheory.Limits.KanExtension` so that
-the definition of `Ran` in that file (which relies on the
-existence of limits) is replaced by a definition
-`Functor.ran` based on the Kan extension API, similarly as
-left Kan extensions have been refactored in #10425.
-
 -/
 
 namespace CategoryTheory

Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

@@ -22,10 +22,6 @@ and if this holds for all `Y : D`, we construct a functor
 
 A dual API for pointwise right Kan extension is also formalized.
 
-## TODO
-
-* refactor the file `CategoryTheory.Limits.KanExtension` using this new general API
-
 ## References
 * https://ncatlab.org/nlab/show/Kan+extension
 

Mathlib/CategoryTheory/Sites/Continuous.lean

@@ -176,16 +176,24 @@ instance [PreservesOneHypercovers.{max u₁ v₁} F J K] :
   isContinuous_of_preservesOneHypercovers.{max u₁ v₁} F J K
 
 variable (A)
+variable [Functor.IsContinuous.{t} F J K]
 
 /-- The induced functor `Sheaf K A ⥤ Sheaf J A` given by `F.op ⋙ _`
 if `F` is a continuous functor.
 -/
-def sheafPushforwardContinuous [Functor.IsContinuous.{t} F J K] :
-    Sheaf K A ⥤ Sheaf J A where
+@[simps!]
+def sheafPushforwardContinuous : Sheaf K A ⥤ Sheaf J A where
   obj ℱ := ⟨F.op ⋙ ℱ.val, F.op_comp_isSheaf J K ℱ⟩
   map f := ⟨((whiskeringLeft _ _ _).obj F.op).map f.val⟩
 #align category_theory.sites.pullback CategoryTheory.Functor.sheafPushforwardContinuous
 
+/-- The functor `F.sheafPushforwardContinuous A J K : Sheaf K A ⥤ Sheaf J A`
+is induced by the precomposition with `F.op`. -/
+@[simps!]
+def sheafPushforwardContinuousCompSheafToPresheafIso :
+    F.sheafPushforwardContinuous A J K ⋙ sheafToPresheaf J A ≅
+      sheafToPresheaf K A ⋙ (whiskeringLeft _ _ _).obj F.op := Iso.refl _
+
 end Functor
 
 end CategoryTheory