feat(CategoryTheory/Sites): 1-hypercovers (#12803)

This PR defines a notion of `1`-hypercovers in a category `C` equipped with a Grothendieck topology `J`. A covering of an object `S : C` consists of a family of maps `f i : X i ⟶ S` which generates a covering sieve. In the favourable case where the fibre products of `X i` and `X j` over `S` exist, the data of a `1`-hypercover consists of the data of objects `Y j` which cover these fibre products. We formalize this notion without assuming that these fibre products actually exists. If `F` is a sheaf and `E` is a `1`-hypercover of `S`, we show that `F.val.obj (op S)` is a multiequalizer of suitable maps `F.val.obj (op (X i)) ⟶ F.val.obj (op (Y j))`.



Co-authored-by: Joël Riou <[email protected]>

Mathlib.lean

@@ -1565,6 +1565,7 @@ import Mathlib.CategoryTheory.Sites.InducedTopology
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 import Mathlib.CategoryTheory.Sites.LeftExact
 import Mathlib.CategoryTheory.Sites.Limits
+import Mathlib.CategoryTheory.Sites.OneHypercover
 import Mathlib.CategoryTheory.Sites.Over
 import Mathlib.CategoryTheory.Sites.Plus
 import Mathlib.CategoryTheory.Sites.Preserves

Mathlib/CategoryTheory/Sites/OneHypercover.lean

@@ -0,0 +1,217 @@
+/-
+Copyright (c) 2024 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.Sites.Sheaf
+
+/-!
+# 1-hypercovers
+
+Given a Grothendieck topology `J` on a category `C`, we define the type of
+`1`-hypercovers of an object `S : C`. They consists of a covering family
+of morphisms `X i ⟶ S` indexed by a type `I₀` and, for each tuple `(i₁, i₂)`
+of elements of `I₀`, a "covering `Y j` of the fibre product of `X i₁` and
+`X i₂` over `S`", a condition which is phrased here without assuming that
+the fibre product actually exist.
+
+The definition `OneHypercover.isLimitMultifork` shows that if `E` is a
+`1`-hypercover of `S`, and `F` is a sheaf, then `F.obj (op S)`
+identifies to the multiequalizer of suitable maps
+`F.obj (op (E.X i)) ⟶ F.obj (op (E.Y j))`.
+
+-/
+
+universe w v u
+
+namespace CategoryTheory
+
+open Category Limits
+
+variable {C : Type u} [Category.{v} C] {A : Type*} [Category A]
+
+/-- The categorical data that is involved in a `1`-hypercover of an object `S`. This
+consists of a family of morphisms `f i : X i ⟶ S` for `i : I₀`, and for each
+tuple `(i₁, i₂)` of elements in `I₀`, a family of objects `Y j` indexed by
+a type `I₁ i₁ i₂`, which are equipped with a map to the fibre product of `X i₁`
+and `X i₂`, which is phrased here as the data of the two projections
+`p₁ : Y j ⟶ X i₁`, `p₂ : Y j ⟶ X i₂` and the relation `p₁ j ≫ f i₁ = p₂ j ≫ f i₂`.
+(See `GrothendieckTopology.OneHypercover` for the topological conditions.) -/
+structure PreOneHypercover (S : C) where
+  /-- the index type of the covering of `S` -/
+  I₀ : Type w
+  /-- the objects in the covering of `S` -/
+  X (i : I₀) : C
+  /-- the morphisms in the covering of `S` -/
+  f (i : I₀) : X i ⟶ S
+  /-- the index type of the coverings of the fibre products -/
+  I₁ (i₁ i₂ : I₀) : Type w
+  /-- the objects in the coverings of the fibre products  -/
+  Y ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂) : C
+  /-- the first projection `Y j ⟶ X i₁` -/
+  p₁ ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂) : Y j ⟶ X i₁
+  /-- the second projection `Y j ⟶ X i₂` -/
+  p₂ ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂) : Y j ⟶ X i₂
+  w ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂) : p₁ j ≫ f i₁ = p₂ j ≫ f i₂
+
+namespace PreOneHypercover
+
+variable {S : C} (E : PreOneHypercover.{w} S)
+
+/-- The assumption that the pullback of `X i₁` and `X i₂` over `S` exists
+for any `i₁` and `i₂`. -/
+abbrev HasPullbacks := ∀ (i₁ i₂ : E.I₀), HasPullback (E.f i₁) (E.f i₂)
+
+/-- The sieve of `S` that is generated by the morphisms `f i : X i ⟶ S`. -/
+abbrev sieve₀ : Sieve S := Sieve.ofArrows _ E.f
+
+/-- Given an object `W` equipped with morphisms `p₁ : W ⟶ E.X i₁`, `p₂ : W ⟶ E.X i₂`,
+this is the sieve of `W` which consists of morphisms `g : Z ⟶ W` such that there exists `j`
+and `h : Z ⟶ E.Y j` such that `g ≫ p₁ = h ≫ E.p₁ j` and `g ≫ p₂ = h ≫ E.p₂ j`.
+See lemmas `sieve₁_eq_pullback_sieve₁'` and `sieve₁'_eq_sieve₁` for equational lemmas
+regarding this sieve. -/
+@[simps]
+def sieve₁ {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) : Sieve W where
+  arrows Z g := ∃ (j : E.I₁ i₁ i₂) (h : Z ⟶ E.Y j), g ≫ p₁ = h ≫ E.p₁ j ∧ g ≫ p₂ = h ≫ E.p₂ j
+  downward_closed := by
+    rintro Z Z' g ⟨j, h, fac₁, fac₂⟩ φ
+    exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩
+
+section
+
+variable {i₁ i₂ : E.I₀} [HasPullback (E.f i₁) (E.f i₂)]
+
+/-- The obvious morphism `E.Y j ⟶ pullback (E.f i₁) (E.f i₂)` given by `E : PreOneHypercover S`. -/
+noncomputable abbrev toPullback (j : E.I₁ i₁ i₂) [HasPullback (E.f i₁) (E.f i₂)] :
+    E.Y j ⟶ pullback (E.f i₁) (E.f i₂) :=
+  pullback.lift (E.p₁ j) (E.p₂ j) (E.w j)
+
+variable (i₁ i₂) in
+/-- The sieve of `pullback (E.f i₁) (E.f i₂)` given by `E : PreOneHypercover S`. -/
+def sieve₁' : Sieve (pullback (E.f i₁) (E.f i₂)) :=
+  Sieve.ofArrows _ (fun (j : E.I₁ i₁ i₂) => E.toPullback j)
+
+lemma sieve₁_eq_pullback_sieve₁' {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂)
+    (w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂) :
+    E.sieve₁ p₁ p₂ = (E.sieve₁' i₁ i₂).pullback (pullback.lift _ _ w) := by
+  ext Z g
+  constructor
+  · rintro ⟨j, h, fac₁, fac₂⟩
+    exact ⟨_, h, _, ⟨j⟩, by aesop_cat⟩
+  · rintro ⟨_, h, w, ⟨j⟩, fac⟩
+    exact ⟨j, h, by simpa using fac.symm =≫ pullback.fst,
+      by simpa using fac.symm =≫ pullback.snd⟩
+
+variable (i₁ i₂) in
+lemma sieve₁'_eq_sieve₁ : E.sieve₁' i₁ i₂ = E.sieve₁ pullback.fst pullback.snd := by
+  rw [← Sieve.pullback_id (S := E.sieve₁' i₁ i₂),
+    sieve₁_eq_pullback_sieve₁' _ _ _ pullback.condition]
+  congr
+  aesop_cat
+
+end
+
+/-- The sigma type of all `E.I₁ i₁ i₂` for `⟨i₁, i₂⟩ : E.I₀ × E.I₀`. -/
+abbrev I₁' : Type w := Sigma (fun (i : E.I₀ × E.I₀) => E.I₁ i.1 i.2)
+
+/-- The diagram of the multifork attached to a presheaf
+`F : Cᵒᵖ ⥤ A`, `S : C` and `E : PreOneHypercover S`. -/
+@[simps]
+def multicospanIndex (F : Cᵒᵖ ⥤ A) : MulticospanIndex A where
+  L := E.I₀
+  R := E.I₁'
+  fstTo j := j.1.1
+  sndTo j := j.1.2
+  left i := F.obj (Opposite.op (E.X i))
+  right j := F.obj (Opposite.op (E.Y j.2))
+  fst j := F.map ((E.p₁ j.2).op)
+  snd j := F.map ((E.p₂ j.2).op)
+
+/-- The multifork attached to a presheaf `F : Cᵒᵖ ⥤ A`, `S : C` and `E : PreOneHypercover S`. -/
+def multifork (F : Cᵒᵖ ⥤ A) :
+    Multifork (E.multicospanIndex F) :=
+  Multifork.ofι _ (F.obj (Opposite.op S)) (fun i₀ => F.map (E.f i₀).op) (by
+    rintro ⟨⟨i₁, i₂⟩, (j : E.I₁ i₁ i₂)⟩
+    dsimp
+    simp only [← F.map_comp, ← op_comp, E.w])
+
+end PreOneHypercover
+
+namespace GrothendieckTopology
+
+variable (J : GrothendieckTopology C)
+
+/-- The type of `1`-hypercovers of an object `S : C` in a category equipped with a
+Grothendieck topology `J`. This can be constructed from a covering of `S` and
+a covering of the fibre products of the objects in this covering (see `OneHypercover.mk'`). -/
+structure OneHypercover (S : C) extends PreOneHypercover S where
+  mem₀ : toPreOneHypercover.sieve₀ ∈ J S
+  mem₁ (i₁ i₂ : I₀) ⦃W : C⦄ (p₁ : W ⟶ X i₁) (p₂ : W ⟶ X i₂) (w : p₁ ≫ f i₁ = p₂ ≫ f i₂) :
+    toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W
+
+variable {J}
+
+lemma OneHypercover.mem_sieve₁' {S : C} (E : J.OneHypercover S)
+    (i₁ i₂ : E.I₀) [HasPullback (E.f i₁) (E.f i₂)] :
+    E.sieve₁' i₁ i₂ ∈ J _ := by
+  rw [E.sieve₁'_eq_sieve₁]
+  exact mem₁ _ _ _ _ _ pullback.condition
+
+namespace OneHypercover
+
+/-- In order to check that a certain data is a `1`-hypercover of `S`, it suffices to
+check that the data provides a covering of `S` and of the fibre products. -/
+@[simps toPreOneHypercover]
+def mk' {S : C} (E : PreOneHypercover S) [E.HasPullbacks]
+    (mem₀ : E.sieve₀ ∈ J S) (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J _) :
+        J.OneHypercover S where
+  toPreOneHypercover := E
+  mem₀ := mem₀
+  mem₁ i₁ i₂ W p₁ p₂ w := by
+    rw [E.sieve₁_eq_pullback_sieve₁' _ _ w]
+    exact J.pullback_stable' _ (mem₁' i₁ i₂)
+
+section
+
+variable {S : C} (E : J.OneHypercover S) (F : Sheaf J A)
+
+section
+
+variable {E F}
+variable (c : Multifork (E.multicospanIndex F.val))
+
+/-- Auxiliary definition of `isLimitMultifork`. -/
+noncomputable def multiforkLift : c.pt ⟶ F.val.obj (Opposite.op S) :=
+  F.cond.amalgamateOfArrows _ E.mem₀ c.ι (fun W i₁ i₂ p₁ p₂ w => by
+    apply F.cond.hom_ext ⟨_, E.mem₁ _ _ _ _ w⟩
+    rintro ⟨T, g, j, h, fac₁, fac₂⟩
+    dsimp
+    simp only [assoc, ← Functor.map_comp, ← op_comp, fac₁, fac₂]
+    simp only [op_comp, Functor.map_comp]
+    simpa using c.condition ⟨⟨i₁, i₂⟩, j⟩ =≫ F.val.map h.op)
+
+@[reassoc]
+lemma multiforkLift_map (i₀ : E.I₀) : multiforkLift c ≫ F.val.map (E.f i₀).op = c.ι i₀ := by
+  simp [multiforkLift]
+
+end
+
+/-- If `E : J.OneHypercover S` and `F : Sheaf J A`, then `F.obj (op S)` is
+a multiequalizer of suitable maps `F.obj (op (E.X i)) ⟶ F.obj (op (E.Y j))`
+induced by `E.p₁ j` and `E.p₂ j`. -/
+noncomputable def isLimitMultifork : IsLimit (E.multifork F.1) :=
+  Multifork.IsLimit.mk _ (fun c => multiforkLift c) (fun c => multiforkLift_map c) (by
+    intro c m hm
+    apply F.cond.hom_ext_ofArrows _ E.mem₀
+    intro i₀
+    dsimp only
+    rw [multiforkLift_map]
+    exact hm i₀)
+
+end
+
+end OneHypercover
+
+end GrothendieckTopology
+
+end CategoryTheory

Mathlib/CategoryTheory/Sites/Sheaf.lean

@@ -254,6 +254,42 @@ theorem IsSheaf.hom_ext {A : Type u₂} [Category.{v₂} A] {E : A} {X : C} {P :
   (hP _ _ S.condition).isSeparatedFor.ext fun Y f hf => h ⟨Y, f, hf⟩
 #align category_theory.presheaf.is_sheaf.hom_ext CategoryTheory.Presheaf.IsSheaf.hom_ext
 
+lemma IsSheaf.hom_ext_ofArrows
+    {P : Cᵒᵖ ⥤ A} (hP : Presheaf.IsSheaf J P) {I : Type*} {S : C} {X : I → C}
+    (f : ∀ i, X i ⟶ S) (hf : Sieve.ofArrows _ f ∈ J S) {E : A}
+    {x y : E ⟶ P.obj (op S)} (h : ∀ i, x ≫ P.map (f i).op = y ≫ P.map (f i).op) :
+    x = y := by
+  apply hP.hom_ext ⟨_, hf⟩
+  rintro ⟨Z, _, _, g, _, ⟨i⟩, rfl⟩
+  dsimp
+  rw [P.map_comp, reassoc_of% (h i)]
+
+section
+
+variable {P : Cᵒᵖ ⥤ A} (hP : Presheaf.IsSheaf J P) {I : Type*} {S : C} {X : I → C}
+  (f : ∀ i, X i ⟶ S) (hf : Sieve.ofArrows _ f ∈ J S) {E : A}
+  (x : ∀ i, E ⟶ P.obj (op (X i)))
+  (hx : ∀ ⦃W : C⦄ ⦃i j : I⦄ (a : W ⟶ X i) (b : W ⟶ X j),
+    a ≫ f i = b ≫ f j → x i ≫ P.map a.op = x j ≫ P.map b.op)
+
+lemma IsSheaf.exists_unique_amalgamation_ofArrows :
+    ∃! (g : E ⟶ P.obj (op S)), ∀ (i : I), g ≫ P.map (f i).op = x i :=
+  (Presieve.isSheafFor_arrows_iff _ _).1
+    ((Presieve.isSheafFor_iff_generate _).2 (hP E _ hf)) x (fun _ _ _ _ _ w => hx _ _ w)
+
+/-- If `P : Cᵒᵖ ⥤ A` is a sheaf and `f i : X i ⟶ S` is a covering family, then
+a morphism `E ⟶ P.obj (op S)` can be constructed from a compatible family of
+morphisms `x : E ⟶ P.obj (op (X i))`. -/
+def IsSheaf.amalgamateOfArrows : E ⟶ P.obj (op S) :=
+  (hP.exists_unique_amalgamation_ofArrows f hf x hx).choose
+
+@[reassoc (attr := simp)]
+lemma IsSheaf.amalgamateOfArrows_map (i : I) :
+    hP.amalgamateOfArrows f hf x hx ≫ P.map (f i).op = x i :=
+  (hP.exists_unique_amalgamation_ofArrows f hf x hx).choose_spec.1 i
+
+end
+
 theorem isSheaf_of_iso_iff {P P' : Cᵒᵖ ⥤ A} (e : P ≅ P') : IsSheaf J P ↔ IsSheaf J P' :=
   forall_congr' fun _ =>
     ⟨Presieve.isSheaf_iso J (isoWhiskerRight e _),