feat(CategoryTheory/Sites): commutation of fiber functors with functors which preserves filtered colimits (leanprover-community#34989)

Author: joelriou

Mathlib/CategoryTheory/Sites/Point/Basic.lean

@@ -46,7 +46,7 @@ and with arbitrary colimits.
 
 @[expose] public section
 
-universe w' w v v' u u'
+universe w' w v v' v'' u u' u''
 
 namespace CategoryTheory
 
@@ -77,7 +77,8 @@ namespace Point
 attribute [instance] initiallySmall isCofiltered
 
 variable {J} (Φ : Point.{w} J) {A : Type u'} [Category.{v'} A]
-  [HasColimitsOfSize.{w, w} A]
+  {B : Type u''} [Category.{v''} B]
+  [HasColimitsOfSize.{w, w} A] [HasColimitsOfSize.{w, w} B]
 
 instance : HasColimitsOfShape Φ.fiber.Elementsᵒᵖ A :=
   hasColimitsOfShape_of_finallySmall _ _
@@ -279,6 +280,36 @@ instance [HasSheafify J A] [J.WEqualsLocallyBijective A] [(forget A).ReflectsIso
             rw [← Functor.map_comp, Sheaf.sheafifyCocone_ι_app_val]
             dsimp))⟩
 
+variable (F : A ⥤ B) [LocallySmall.{w} C] [PreservesFilteredColimitsOfSize.{w, w} F]
+
+/-- If `Φ` is a point of a site and `F : A ⥤ B` is a functor which preserves
+filtered colimits, then taking fibers of presheaves at `Φ` commutes with `F`. -/
+noncomputable def presheafFiberCompIso :
+  (Functor.whiskeringRight _ _ _).obj F ⋙ Φ.presheafFiber ≅
+    Φ.presheafFiber ⋙ F :=
+  haveI := Functor.Final.preservesColimitsOfShape_of_final
+    (FinallySmall.fromFilteredFinalModel.{w} (Φ.fiber.Elementsᵒᵖ)) F
+  Functor.isoWhiskerLeft
+    ((Functor.whiskeringLeft _ _ _).obj _) (preservesColimitNatIso F).symm
+
+@[reassoc]
+lemma toPresheafFiber_presheafFiberCompIso_hom_app
+    (X : C) (x : Φ.fiber.obj X) (P : Cᵒᵖ ⥤ A) :
+    Φ.toPresheafFiber X x (P ⋙ F) ≫ (Φ.presheafFiberCompIso F).hom.app P =
+      F.map (Φ.toPresheafFiber X x P) := by
+  haveI := Functor.Final.preservesColimitsOfShape_of_final
+    (FinallySmall.fromFilteredFinalModel.{w} (Φ.fiber.Elementsᵒᵖ)) F
+  simp only [presheafFiberCompIso]
+  exact ι_preservesColimitIso_inv F ((CategoryOfElements.π Φ.fiber).op ⋙ P) _
+
+/-- If `Φ` is a point of a site and `F : A ⥤ B` is a functor which preserves
+filtered colimits, then taking fibers of sheaves at `Φ` commutes with `F`. -/
+@[simps!]
+noncomputable def sheafFiberCompIso [J.HasSheafCompose F] :
+    sheafCompose J F ⋙ Φ.sheafFiber ≅ Φ.sheafFiber ⋙ F :=
+  Functor.isoWhiskerLeft (sheafToPresheaf J A) (Φ.presheafFiberCompIso F) ≪≫
+    (Functor.associator _ _ _).symm
+
 end Point
 
 end GrothendieckTopology