feat(CategoryTheory/Sites): sheaf condition and coproducts (leanprover-community#26231)

We show that under suitable conditions, checking that a presheaf is a sheaf for a covering is equivalent to checking it on the single object covering by the coproduct.

Author: chrisflav

Mathlib.lean

@@ -3148,6 +3148,7 @@ public import Mathlib.CategoryTheory.Sites.CompatibleSheafification
 public import Mathlib.CategoryTheory.Sites.ConcreteSheafification
 public import Mathlib.CategoryTheory.Sites.ConstantSheaf
 public import Mathlib.CategoryTheory.Sites.Continuous
+public import Mathlib.CategoryTheory.Sites.CoproductSheafCondition
 public import Mathlib.CategoryTheory.Sites.CoverLifting
 public import Mathlib.CategoryTheory.Sites.CoverPreserving
 public import Mathlib.CategoryTheory.Sites.Coverage

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -864,6 +864,12 @@ theorem Pi.reindex_hom_π (b : β) : (Pi.reindex ε f).hom ≫ Pi.π f (ε b) =
 theorem Pi.reindex_inv_π (b : β) : (Pi.reindex ε f).inv ≫ Pi.π (f ∘ ε) b = Pi.π f (ε b) := by
   simp [Iso.inv_comp_eq]
 
+variable {f} in
+/-- Being a limiting fan is stable under equivalences in the index type. -/
+def Fan.isLimitEquivOfEquiv (c : Fan f) :
+    IsLimit c ≃ IsLimit (Fan.mk _ fun i : β ↦ c.proj (ε i)) :=
+  IsLimit.whiskerEquivalenceEquiv (Discrete.equivalence ε)
+
 end
 
 section
@@ -892,6 +898,12 @@ set_option backward.isDefEq.respectTransparency false in
 theorem Sigma.ι_reindex_inv (b : β) :
     Sigma.ι f (ε b) ≫ (Sigma.reindex ε f).inv = Sigma.ι (f ∘ ε) b := by simp [Iso.comp_inv_eq]
 
+variable {f} in
+/-- Being a colimiting cofan is stable under equivalences in the index type. -/
+def Cofan.isColimitEquivOfEquiv (c : Cofan f) :
+    IsColimit c ≃ IsColimit (Cofan.mk _ fun i : β ↦ c.inj (ε i)) :=
+  IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence ε)
+
 end
 
 end Reindex

Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean

@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2026 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.CategoryTheory.Limits.Final
+public import Mathlib.CategoryTheory.Limits.VanKampen
+public import Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
+
+/-!
+# The sheaf condition and universal coproducts
+
+In this file we show that if `{ fᵢ : Yᵢ ⟶ X }` is a family of morphisms and `∐ᵢ Yᵢ` is a universal
+coproduct, then any presheaf `F` that preserves products is a sheaf for the single object covering
+`{ ∐ᵢ Yᵢ ⟶ X }` if and only if it is a sheaf for `{ fᵢ : Yᵢ ⟶ X }ᵢ`.
+
+We provide both a version for a general coefficient category and one for type values presheafs.
+-/
+
+universe w
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Limits Opposite
+
+variable {C : Type*} [Category* C] {A : Type*} [Category* A] {S : C}
+
+set_option backward.isDefEq.respectTransparency false in
+/--
+Let `E` be a pre-`0`-hypercover with pairwise pullbacks. If `∐ᵢ Eᵢ` is a universal coproduct
+and the presheaf `F` preserves products, then the multifork associated to the single object
+`0`-hypercover `{ ∐ᵢ Eᵢ ⟶ S }` is exact if and only if the multifork for `E` is exact.
+-/
+noncomputable
+def PreZeroHypercover.isLimitSigmaOfIsColimitEquiv (E : PreZeroHypercover.{w} S)
+    [E.HasPullbacks] {c : Cofan E.X} (hc : IsColimit c) (huniv : IsUniversalColimit c)
+    [(E.sigmaOfIsColimit hc).HasPullbacks]
+    [∀ i, HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)]
+    (F : Cᵒᵖ ⥤ A)
+    [PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F]
+    [PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F] :
+    IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃
+      IsLimit (E.toPreOneHypercover.multifork F) := by
+  have : HasPullback (Cofan.IsColimit.desc hc E.f) (Cofan.IsColimit.desc hc E.f) :=
+    inferInstanceAs <| HasPullback
+      ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
+  let c' : Cofan E.toPreOneHypercover.Y' :=
+    Cofan.mk
+      ((E.sigmaOfIsColimit hc).toPreOneHypercover.Y (i₁ := ⟨⟩) (i₂ := ⟨⟩) ⟨⟩)
+      fun b ↦ pullback.map _ _ _ _ (c.inj _) (c.inj _) (𝟙 _) (by simp) (by simp)
+  let equiv : E.toPreOneHypercover.I₁' ≃ E.I₀ × E.I₀ :=
+    Equiv.sigmaPUnit (E.toPreOneHypercover.I₀ × E.toPreOneHypercover.I₀)
+  have hc' : IsColimit c' := by
+    refine (c'.isColimitEquivOfEquiv equiv.symm).symm (Nonempty.some ?_)
+    exact IsUniversalColimit.nonempty_isColimit_prod_of_isPullback
+      huniv huniv E.f E.f ((E.sigmaOfIsColimit hc).f ⟨⟩) ((E.sigmaOfIsColimit hc).f ⟨⟩)
+      (fun i j ↦ .of_hasPullback _ _) (.of_hasPullback _ _) (.refl _) (by simp) (by simp)
+      (by simp [c', equiv, Equiv.sigmaPUnit]) (by simp [c', equiv, Equiv.sigmaPUnit])
+  refine .trans ?_ (E.toPreOneHypercover.isLimitSigmaOfIsColimitEquiv hc hc' F)
+  apply PreOneHypercover.isLimitEquivOfIso
+  refine PreOneHypercover.isoMk (.refl _) (fun _ ↦ .refl _) (fun _ _ ↦ .refl _)
+      (fun _ _ _ ↦ Iso.refl _) (by cat_disch) ?_ ?_
+  · intro ⟨⟩ ⟨⟩ k
+    refine Cofan.IsColimit.hom_ext hc' _ _ fun k ↦ ?_
+    congr 1
+    exact Cofan.IsColimit.hom_ext hc' _ _ fun a ↦ by simp; simp [c']
+  · intro ⟨⟩ ⟨⟩ k
+    exact Cofan.IsColimit.hom_ext hc' _ _ fun a ↦ by simp; simp [c']
+
+set_option backward.isDefEq.respectTransparency false in
+open PreZeroHypercover in
+/--
+Let `{ fᵢ : Xᵢ ⟶ S }` be a family of morphisms. If `∐ᵢ Xᵢ` is a universal coproduct
+and the presheaf `F` preserves products, then `F` is a sheaf for the single object covering
+`{ ∐ᵢ Xᵢ ⟶ S }` if and only if it is a sheaf for `{ fᵢ : Xᵢ ⟶ S }ᵢ`.
+-/
+lemma Presieve.isSheafFor_sigmaDesc_iff {ι : Type*} {X : ι → C} (f : ∀ i, X i ⟶ S)
+    [(ofArrows X f).HasPairwisePullbacks] {c : Cofan X} (hc : IsColimit c)
+    (hc' : IsUniversalColimit c)
+    [HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)]
+    [∀ i, HasPullback (f i) (Cofan.IsColimit.desc hc f)]
+    (F : Cᵒᵖ ⥤ Type*)
+    [PreservesLimit (Discrete.functor <| fun i ↦ op (X i)) F]
+    [PreservesLimit (Discrete.functor fun (ij : ι × ι) ↦ op (pullback (f ij.1) (f ij.2))) F] :
+    Presieve.IsSheafFor F (.singleton <| Cofan.IsColimit.desc hc f) ↔
+      Presieve.IsSheafFor F (.ofArrows X f) := by
+  let E := PreZeroHypercover.mk _ _ f
+  have : (E.sigmaOfIsColimit hc).HasPullbacks :=
+    fun i j ↦ by dsimp [sigmaOfIsColimit]; infer_instance
+  have (i : E.I₀) : HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit) := by
+    dsimp [sigmaOfIsColimit_f]; infer_instance
+  have : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.X i)) F := by
+    dsimp [E]; infer_instance
+  have : PreservesLimit (Discrete.functor fun i ↦ op (E.toPreOneHypercover.Y' i)) F := by
+    convert Functor.Initial.preservesLimit_of_comp (Discrete.equivalence <| .sigmaPUnit _).inverse
+    assumption
+  let equiv := (E.isLimitSigmaOfIsColimitEquiv hc hc' F).nonempty_congr
+  rwa [isLimit_toPreOneHypercover_type_iff, isLimit_toPreOneHypercover_type_iff,
+    presieve₀_sigmaOfIsColimit] at equiv
+
+end CategoryTheory

Mathlib/CategoryTheory/Sites/Hypercover/SheafOfTypes.lean

@@ -37,6 +37,38 @@ open Limits Opposite
 
 variable {C : Type*} [Category* C]
 
+namespace PreZeroHypercover
+
+variable {S : C}
+
+/-- If the pre-`0`-hypercover `E` has pairwise pullbacks, the sections over the multifork
+associated to a presheaf of types are equivalent to the compatible families on `E`. -/
+@[simps]
+def sectionsEquivOfHasPullbacks (E : PreZeroHypercover S)
+    [E.HasPullbacks] (F : Cᵒᵖ ⥤ Type*) :
+    (E.toPreOneHypercover.multicospanIndex F).sections ≃
+      Subtype (Presieve.Arrows.Compatible F E.f) where
+  toFun s :=
+    ⟨s.val, fun i j W gi gj hgij ↦ by
+      have heq := s.property ⟨(i, j), ⟨⟩⟩
+      dsimp at heq
+      rw [← pullback.lift_fst _ _ hgij]
+      conv_rhs => rw [← pullback.lift_snd _ _ hgij]
+      rw [op_comp, Functor.map_comp, op_comp, Functor.map_comp]
+      simp [heq]⟩
+  invFun s := ⟨s.val, fun r ↦ s.property _ _ _ _ _ pullback.condition⟩
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+lemma isLimit_toPreOneHypercover_type_iff (E : PreZeroHypercover.{w} S) [E.HasPullbacks]
+    (F : Cᵒᵖ ⥤ Type*) :
+    Nonempty (IsLimit <| E.toPreOneHypercover.multifork F) ↔ E.presieve₀.IsSheafFor F := by
+  rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
+    ← Function.Bijective.of_comp_iff' (E.sectionsEquivOfHasPullbacks F).symm.bijective]
+  rfl
+
+end PreZeroHypercover
+
 namespace PreOneHypercover
 
 variable {X : C} {E : PreOneHypercover.{w} X} {F : Cᵒᵖ ⥤ Type*}

Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

@@ -222,7 +222,7 @@ def add (E : PreZeroHypercover.{w} S) {T : C} (f : T ⟶ S) : PreZeroHypercover.
   simp [add, presieve₀_reindex, presieve₀_sum]
 
 /-- The single object pre-`0`-hypercover obtained from taking the coproduct of the components. -/
-@[simps I₀ X]
+@[simps I₀ X, simps -isSimp f]
 def sigmaOfIsColimit (E : PreZeroHypercover.{w} S) {c : Cofan E.X} (hc : IsColimit c) :
     PreZeroHypercover.{w} S where
   I₀ := PUnit
@@ -235,6 +235,11 @@ lemma inj_sigmaOfIsColimit_f (E : PreZeroHypercover.{w} S) {c : Cofan E.X} (hc :
     c.inj i ≫ (E.sigmaOfIsColimit hc).f r = E.f i := by
   simp [PreZeroHypercover.sigmaOfIsColimit]
 
+@[simp]
+lemma presieve₀_sigmaOfIsColimit (E : PreZeroHypercover.{w} S) {c : Cofan E.X} (hc : IsColimit c) :
+    (E.sigmaOfIsColimit hc).presieve₀ = Presieve.singleton (Cofan.IsColimit.desc hc E.f) :=
+  Presieve.ofArrows_pUnit _
+
 section Category
 
 variable {E : PreZeroHypercover.{w} S} {F : PreZeroHypercover.{w'} S}