feat(CategoryTheory): finite-product preserving presheaves are sheaves for extensive presieves (#7949)

We prove that finite-product preserving presheaves on extensive categories are sheaves for `extensive` presieves.

-  [x] depends on: #7804 

Co-authored-by: Riccardo Brasca @riccardobrasca [[email protected]](mailto:[email protected])
Co-authored-by: Filippo A E Nuccio @faenuccio [[email protected]](mailto:[email protected])

Author: dagurtomas

Mathlib/CategoryTheory/Sites/RegularExtensive.lean

@@ -3,11 +3,10 @@ Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson, Filippo A. E. Nuccio, Riccardo Brasca
 -/
+import Mathlib.CategoryTheory.Extensive
 import Mathlib.CategoryTheory.Preadditive.Projective
 import Mathlib.CategoryTheory.Sites.Coherent
-import Mathlib.CategoryTheory.Extensive
-import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
-import Mathlib.Tactic.ApplyFun
+import Mathlib.CategoryTheory.Sites.Preserves
 /-!
 
 # The Regular and Extensive Coverages
@@ -23,19 +22,29 @@ The second one is called the *extensive* coverage and for that to exist, the cat
 satisfy a condition called `FinitaryPreExtensive C`. This means `C` has finite coproducts and that
 those are preserved by pullbacks. The covering sieves of this coverage are generated by presieves
 consisting finitely many arrows that together induce an isomorphism from the coproduct to the
-target.
+target. This condition is weaker than `FinitaryExtensive`, where in addition finite coproducts are
+disjoint.
+
+## Main results
 
-In `extensive_union_regular_generates_coherent`, we prove that the union of these two coverages
-generates the coherent topology on `C` if `C` is precoherent, extensive and regular.
+* `extensive_union_regular_generates_coherent`: the union of the regular and extensive coverages
+  generates the coherent topology on `C` if `C` is precoherent, preextensive and preregular.
 
-In `isSheafFor_regular_of_hasPullbacks` we prove that a presheaf satisfying an "equaliser condition"
-satisfies the sheaf condition for a presieve consisting of a single effective epimorphism. In
-`isSheafFor_regular_of_projective`, we prove that every presheaf satisfies the sheaf condition for
-such presieves with projective target.
+* `isSheaf_iff_equalizerCondition`: In a preregular category with pullbacks, the sheaves for the
+  regular topology are precisely the presheaves satisfying an equaliser condition with respect to
+  effective epimorphisms.
+
+* `isSheaf_of_projective`: In a preregular category in which every object is projective, every
+  presheaf is a sheaf for the regular topology.
+
+* `isSheaf_iff_preservesFiniteProducts`: In a finitary extensive category, the sheaves for the
+  extensive topology are precisely those preserving finite products.
 
 TODO: figure out under what conditions `Preregular` and `Extensive` are implied by `Precoherent` and
 vice versa.
 
+TODO: refactor the section `RegularSheaves` to use the new `Arrows` sheaf API.
+
 -/
 
 universe v u w
@@ -89,6 +98,8 @@ def regularCoverage [Preregular C] : Coverage C where
 
 /--
 The extensive coverage on an extensive category `C`
+
+TODO: use general colimit API instead of `IsIso (Sigma.desc π)`
 -/
 def extensiveCoverage [FinitaryPreExtensive C] : Coverage C where
   covering B := { S | ∃ (α : Type) (_ : Fintype α) (X : α → C) (π : (a : α) → (X a ⟶ B)),
@@ -256,4 +267,81 @@ lemma isSheaf_of_projective (F : Cᵒᵖ ⥤ Type (max u v)) [Preregular C] [∀
 
 end RegularSheaves
 
+section ExtensiveSheaves
+
+variable [FinitaryPreExtensive C] {C}
+
+/-- A presieve is *extensive* if it is finite and its arrows induce an isomorphism from the
+coproduct to the target. -/
+class Presieve.extensive {X : C} (R : Presieve X) :
+    Prop where
+  /-- `R` consists of a finite collection of arrows that together induce an isomorphism from the
+  coproduct of their sources. -/
+  arrows_nonempty_isColimit : ∃ (α : Type) (_ : Fintype α) (Z : α → C) (π : (a : α) → (Z a ⟶ X)),
+    R = Presieve.ofArrows Z π ∧ Nonempty (IsColimit (Cofan.mk X π))
+
+instance {X : C} (S : Presieve X) [S.extensive] : S.hasPullbacks where
+  has_pullbacks := by
+    obtain ⟨_, _, _, _, rfl, ⟨hc⟩⟩ := Presieve.extensive.arrows_nonempty_isColimit (R := S)
+    intro _ _ _ _ _ hg
+    cases hg
+    apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct hc
+
+instance {α : Type} [Fintype α] {Z : α → C} {F : C ⥤ Type w}
+    [PreservesFiniteProducts F] : PreservesLimit (Discrete.functor fun a => (Z a)) F :=
+  (PreservesFiniteProducts.preserves α).preservesLimit
+
+open Presieve Opposite
+
+/--
+A finite product preserving presheaf is a sheaf for the extensive topology on a category which is
+`FinitaryPreExtensive`.
+-/
+theorem isSheafFor_extensive_of_preservesFiniteProducts {X : C} (S : Presieve X) [S.extensive]
+    (F : Cᵒᵖ ⥤ Type max u v) [PreservesFiniteProducts F] : S.IsSheafFor F  := by
+  obtain ⟨_, _, Z, π, rfl, ⟨hc⟩⟩ := extensive.arrows_nonempty_isColimit (R := S)
+  have : (ofArrows Z (Cofan.mk X π).inj).hasPullbacks :=
+    (inferInstance : (ofArrows Z π).hasPullbacks)
+  exact isSheafFor_of_preservesProduct _ _ hc
+
+instance {α : Type} [Fintype α] (Z : α → C) : (ofArrows Z (fun i ↦ Sigma.ι Z i)).extensive :=
+  ⟨⟨α, inferInstance, Z, (fun i ↦ Sigma.ι Z i), rfl, ⟨coproductIsCoproduct _⟩⟩⟩
+
+/--
+A presheaf on a category which is `FinitaryExtensive` is a sheaf iff it preserves finite products.
+-/
+theorem isSheaf_iff_preservesFiniteProducts [FinitaryExtensive C] (F : Cᵒᵖ ⥤ Type max u v) :
+    Presieve.IsSheaf (extensiveCoverage C).toGrothendieck F ↔
+    Nonempty (PreservesFiniteProducts F) := by
+  refine ⟨fun hF ↦ ⟨⟨fun α _ ↦ ⟨fun {K} ↦ ?_⟩⟩⟩, fun hF ↦ ?_⟩
+  · rw [Presieve.isSheaf_coverage] at hF
+    let Z : α → C := fun i ↦ unop (K.obj ⟨i⟩)
+    have : (Presieve.ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks :=
+      (inferInstance : (Presieve.ofArrows Z (Sigma.ι Z)).hasPullbacks)
+    have : ∀ (i : α), Mono (Cofan.inj (Cofan.mk (∐ Z) (Sigma.ι Z)) i) :=
+      (inferInstance : ∀ (i : α), Mono (Sigma.ι Z i))
+    let i : K ≅ Discrete.functor (fun i ↦ op (Z i)) := Discrete.natIsoFunctor
+    let _ : PreservesLimit (Discrete.functor (fun i ↦ op (Z i))) F :=
+        Presieve.preservesProductOfIsSheafFor F ?_ initialIsInitial _ (coproductIsCoproduct Z)
+        (FinitaryExtensive.isPullback_initial_to_sigma_ι Z)
+        (hF (Presieve.ofArrows Z (fun i ↦ Sigma.ι Z i)) ?_)
+    · exact preservesLimitOfIsoDiagram F i.symm
+    · apply hF
+      refine ⟨Empty, inferInstance, Empty.elim, IsEmpty.elim inferInstance, rfl, ⟨default,?_, ?_⟩⟩
+      · ext b
+        cases b
+      · simp only [eq_iff_true_of_subsingleton]
+    · refine ⟨α, inferInstance, Z, (fun i ↦ Sigma.ι Z i), rfl, ?_⟩
+      suffices Sigma.desc (fun i ↦ Sigma.ι Z i) = 𝟙 _ by rw [this]; infer_instance
+      ext
+      simp
+  · let _ := hF.some
+    rw [Presieve.isSheaf_coverage]
+    intro X R ⟨Y, α, Z, π, hR, hi⟩
+    have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi
+    have : R.extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩
+    exact isSheafFor_extensive_of_preservesFiniteProducts R F
+
+end ExtensiveSheaves
+
 end CategoryTheory