From 3ab4537692baa46a8258c5c5332dc95fb6d31d15 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 15 May 2024 16:06:17 +0000 Subject: [PATCH] feat(CategoryTheory/Sites): 1-hypercovers (#12803) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 <37772949+joelriou@users.noreply.github.com> --- Mathlib.lean | 1 + .../CategoryTheory/Sites/OneHypercover.lean | 217 ++++++++++++++++++ Mathlib/CategoryTheory/Sites/Sheaf.lean | 36 +++ 3 files changed, 254 insertions(+) create mode 100644 Mathlib/CategoryTheory/Sites/OneHypercover.lean diff --git a/Mathlib.lean b/Mathlib.lean index abb74ddb90fe1c..f951f2a25fcc42 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/OneHypercover.lean b/Mathlib/CategoryTheory/Sites/OneHypercover.lean new file mode 100644 index 00000000000000..8f115839b45531 --- /dev/null +++ b/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 diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean index babeba9dfb570d..96a26fc2322871 100644 --- a/Mathlib/CategoryTheory/Sites/Sheaf.lean +++ b/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 _),