feat(CategoryTheory/Sites): characterization of covering sieves using locally surjective morphisms (leanprover-community#35529)

The sieve generated by a family of morphisms `f i : X i ⟶ S` is covering iff the induced map from the coproduct of the presheaves represented by the `X i` to the presheaf represented by `S` is locally surjective.

Author: joelriou

Mathlib/CategoryTheory/ShrinkYoneda.lean

@@ -71,6 +71,23 @@ noncomputable def shrinkYonedaObjObjEquiv {X : C} {Y : Cᵒᵖ} :
     ((shrinkYoneda.{w}.obj X).obj Y) ≃ (Y.unop ⟶ X) :=
   (equivShrink _).symm
 
+lemma shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm
+    {X : C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y') (f : Y.unop ⟶ X) :
+    (shrinkYoneda.obj _).map g (shrinkYonedaObjObjEquiv.symm f) =
+      shrinkYonedaObjObjEquiv.symm (g.unop ≫ f) := by
+  simp [shrinkYoneda, shrinkYonedaObjObjEquiv]
+
+lemma shrinkYonedaObjObjEquiv_symm_comp {X Y Y' : C} (g : Y' ⟶ Y) (f : Y ⟶ X) :
+    shrinkYonedaObjObjEquiv.symm (g ≫ f) =
+    (shrinkYoneda.obj _).map g.op (shrinkYonedaObjObjEquiv.symm f) :=
+  (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op f).symm
+
+lemma shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm
+    {X X' : C} {Y : Cᵒᵖ} (f : Y.unop ⟶ X) (g : X ⟶ X') :
+    (shrinkYoneda.map g).app _ (shrinkYonedaObjObjEquiv.symm f) =
+      shrinkYonedaObjObjEquiv.symm (f ≫ g) := by
+  simp [shrinkYoneda, shrinkYonedaObjObjEquiv]
+
 set_option backward.isDefEq.respectTransparency false in
 /-- The type of natural transformations `shrinkYoneda.{w}.obj X ⟶ P`
 with `X : C` and `P : Cᵒᵖ ⥤ Type w` is equivalent to `P.obj (op X)`. -/
@@ -119,6 +136,13 @@ lemma shrinkYonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {P : Cᵒᵖ ⥤
     rw [← shrinkYonedaEquiv_naturality]
     simp)
 
+lemma shrinkYonedaEquiv_symm_app_shrinkYonedaObjObjEquiv_symm {X : C} {P : Cᵒᵖ ⥤ Type w}
+    (s : P.obj (op X)) {Y : C} (f : Y ⟶ X) :
+    (shrinkYonedaEquiv.symm s).app (op Y) (shrinkYonedaObjObjEquiv.symm f) =
+      P.map f.op s := by
+  obtain ⟨g, rfl⟩ := shrinkYonedaEquiv.surjective s
+  simp [map_shrinkYonedaEquiv]
+
 variable (C) in
 /-- The functor `shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w` for a locally `w`-small category `C`
 is fully faithful. -/
@@ -134,4 +158,14 @@ instance : (shrinkYoneda.{w} (C := C)).Faithful := (fullyFaithfulShrinkYoneda C)
 
 instance : (shrinkYoneda.{w} (C := C)).Full := (fullyFaithfulShrinkYoneda C).full
 
+/-- `uliftYoneda` identifies to `shrinkYoneda`. -/
+noncomputable def uliftYonedaIsoShrinkYoneda :
+    uliftYoneda.{w'} (C := C) ≅ shrinkYoneda.{max w' v} :=
+  NatIso.ofComponents (fun X ↦ NatIso.ofComponents
+    (fun Y ↦ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso) (fun f ↦ by
+      ext
+      exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm _ _).symm)) (fun g ↦ by
+      ext
+      exact (shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm _ _).symm)
+
 end CategoryTheory

Mathlib/CategoryTheory/Sites/LocallySurjective.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.CategoryTheory.Sites.Subsheaf
 public import Mathlib.CategoryTheory.Sites.CompatibleSheafification
 public import Mathlib.CategoryTheory.Sites.LocallyInjective
+public import Mathlib.CategoryTheory.ShrinkYoneda
 /-!
 
 # Locally surjective morphisms
@@ -29,9 +30,9 @@ public import Mathlib.CategoryTheory.Sites.LocallyInjective
 @[expose] public section
 
 
-universe v u w v' u' w'
+universe w v u v' u' w'
 
-open Opposite CategoryTheory CategoryTheory.GrothendieckTopology CategoryTheory.Functor
+open Opposite CategoryTheory CategoryTheory.GrothendieckTopology CategoryTheory.Functor Limits
 
 namespace CategoryTheory
 
@@ -52,6 +53,13 @@ def imageSieve {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : ToType (G.obj (o
     refine ⟨F.map j.op t, ?_⟩
     rw [op_comp, G.map_comp, ConcreteCategory.comp_apply, ← ht, NatTrans.naturality_apply f]
 
+lemma pullback_imageSieve
+    {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : ToType (G.obj (op U)))
+    {V : C} (g : V ⟶ U) :
+    (imageSieve f s).pullback g = imageSieve f (G.map g.op s) := by
+  ext W g
+  simp [imageSieve]
+
 theorem imageSieve_eq_sieveOfSection {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C}
     (s : ToType (G.obj (op U))) :
     imageSieve f s = (Subfunctor.range (whiskerRight f (forget A))).sieveOfSection s :=
@@ -399,4 +407,96 @@ lemma isAmalgamation_map_localPreimage :
 
 end Presieve.FamilyOfElements
 
+namespace Presheaf
+
+variable {S : C} {ι : Type*} [Small.{w} ι] {X : ι → C} (f : ∀ i, X i ⟶ S)
+
+variable [LocallySmall.{w} C]
+
+lemma imageSieve_cofanIsColimitDesc_shrinkYoneda_map
+    {c : Cofan (fun i ↦ shrinkYoneda.{w}.obj (X i))} (hc : IsColimit c)
+    {U : C} (g : U ⟶ S) :
+    Presheaf.imageSieve
+      (Cofan.IsColimit.desc hc (fun i ↦ shrinkYoneda.{w}.map (f i))) (U := U)
+        (shrinkYonedaObjObjEquiv.symm g) = Sieve.pullback g (Sieve.ofArrows X f) := by
+  ext V v
+  simp only [Sieve.pullback_apply, Sieve.generate_apply]
+  refine ⟨fun hv ↦ ?_, ?_⟩
+  · obtain ⟨w, hw⟩ := hv
+    obtain ⟨⟨i⟩, a, rfl⟩ := Types.jointly_surjective_of_isColimit
+      (isColimitOfPreserves ((evaluation _ _).obj (op V)) hc) w
+    obtain ⟨a : V ⟶ X i, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective a
+    refine ⟨_, a, _, ⟨i⟩, shrinkYonedaObjObjEquiv.symm.injective ?_⟩
+    rw [← shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm]
+    convert hw using 1
+    · exact (congr_fun (NatTrans.congr_app
+        ((Cofan.IsColimit.fac hc (fun i ↦ shrinkYoneda.{w}.map (f i))) i) (op V))
+          (shrinkYonedaObjObjEquiv.symm a)).symm
+    · exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm
+  · rintro ⟨_, a, _, ⟨i⟩, fac⟩
+    refine ⟨(c.inj i).app (op V) (shrinkYonedaObjObjEquiv.symm a),
+      (congr_fun (NatTrans.congr_app
+      ((Cofan.IsColimit.fac hc (fun i ↦ shrinkYoneda.{w}.map (f i))) i) (op V))
+        (shrinkYonedaObjObjEquiv.symm a)).trans ?_⟩
+    rw [shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm a (f i), fac]
+    exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm
+
+end Presheaf
+
+namespace GrothendieckTopology
+
+lemma ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map
+    [LocallySmall.{w} C] {S : C} {ι : Type*} [Small.{w} ι] {X : ι → C}
+    (f : ∀ i, X i ⟶ S)
+    {c : Cofan (fun i ↦ shrinkYoneda.{w}.obj (X i))} (hc : IsColimit c) :
+    Sieve.ofArrows _ f ∈ J S ↔
+      Presheaf.IsLocallySurjective J
+        (Cofan.IsColimit.desc hc (fun i ↦ shrinkYoneda.{w}.map (f i))) := by
+  refine ⟨fun hf ↦ ⟨fun {U u} ↦ ?_⟩, fun hf ↦ ?_⟩
+  · obtain ⟨u, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective u
+    replace hf := J.pullback_stable u hf
+    rwa [← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc u] at hf
+  · rw [← Sieve.pullback_id (S := Sieve.ofArrows X f),
+      ← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc (𝟙 S)]
+    exact Presheaf.imageSieve_mem J (Cofan.IsColimit.desc hc (fun i ↦ shrinkYoneda.{w}.map (f i)))
+      (shrinkYonedaObjObjEquiv.symm (𝟙 S))
+
+lemma ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map
+    {S : C} {ι : Type*} [Small.{max w v} ι] {X : ι → C}
+    (f : ∀ i, X i ⟶ S)
+    {c : Cofan (fun i ↦ uliftYoneda.{w}.obj (X i))} (hc : IsColimit c) :
+    Sieve.ofArrows _ f ∈ J S ↔
+      Presheaf.IsLocallySurjective J
+        (Cofan.IsColimit.desc hc (fun i ↦ uliftYoneda.{w}.map (f i))) := by
+  let e : Discrete.functor (fun i ↦ uliftYoneda.{w}.obj (X i)) ≅
+      Discrete.functor (fun i ↦ shrinkYoneda.{max w v}.obj (X i)) :=
+    Discrete.natIso (fun i ↦ uliftYonedaIsoShrinkYoneda.{w}.app (X i.as))
+  let hc' := (IsColimit.precomposeInvEquiv e _).2 hc
+  rw [ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map.{max w v} J f hc']
+  have :
+      Cofan.IsColimit.desc hc (fun i ↦ uliftYoneda.map (f i)) ≫
+        uliftYonedaIsoShrinkYoneda.hom.app _ =
+      Cofan.IsColimit.desc hc' (fun i ↦ shrinkYoneda.map (f i)) :=
+    Cofan.IsColimit.hom_ext hc _ _ (fun i ↦ by
+      rw [Cofan.IsColimit.fac_assoc, NatTrans.naturality,
+        ← Cofan.IsColimit.fac hc' (fun i ↦ shrinkYoneda.map (f i)) i]
+      simp [Cofan.inj, e])
+  rw [← this, Presheaf.isLocallySurjective_comp_iff J]
+
+lemma ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map [LocallySmall.{w} C]
+    {S : C} {ι : Type*} [Small.{w} ι] {X : ι → C} (f : ∀ i, X i ⟶ S) :
+    Sieve.ofArrows _ f ∈ J S ↔
+      Presheaf.IsLocallySurjective J (Sigma.desc (fun i ↦ shrinkYoneda.{w}.map (f i))) :=
+  ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map J f
+    (coproductIsCoproduct _)
+
+lemma ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map
+    {S : C} {ι : Type*} [Small.{max w v} ι] {X : ι → C} (f : ∀ i, X i ⟶ S) :
+    Sieve.ofArrows _ f ∈ J S ↔
+      Presheaf.IsLocallySurjective J (Sigma.desc (fun i ↦ uliftYoneda.{w}.map (f i))) :=
+  ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map J f
+    (coproductIsCoproduct _)
+
+end GrothendieckTopology
+
 end CategoryTheory