From 240726c9449de24c64b3e9333abe0b335f5d46ad Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 19 Dec 2020 16:26:07 +0000 Subject: [PATCH 01/21] definition! --- src/category_theory/sites/canonical.lean | 2 +- src/category_theory/sites/sheaf.lean | 885 +---------------- src/category_theory/sites/sheaf_of_types.lean | 905 ++++++++++++++++++ 3 files changed, 958 insertions(+), 834 deletions(-) create mode 100644 src/category_theory/sites/sheaf_of_types.lean diff --git a/src/category_theory/sites/canonical.lean b/src/category_theory/sites/canonical.lean index eeb4ee71eade6..d9911a10fdc5d 100644 --- a/src/category_theory/sites/canonical.lean +++ b/src/category_theory/sites/canonical.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta -/ -import category_theory.sites.sheaf +import category_theory.sites.sheaf_of_types /-! diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 84b69b8d2141f..f7018700dd08c 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -1,724 +1,64 @@ -/- -Copyright (c) 2020 Bhavik Mehta. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Bhavik Mehta --/ +-- sheaves taking values in a category -import category_theory.sites.pretopology -import category_theory.limits.shapes.types -import category_theory.full_subcategory - -/-! -# Sheaves on a Grothendieck topology - -Defines the notion of a sheaf on a Grothendieck topology, as well as a range of equivalent -conditions useful in different situations. - -First define what it means for a presheaf `P : Cᵒᵖ ⥤ Type v` to be a sheaf *for* a particular -presieve `R` on `X`: -* A *family of elements* `x` for `P` at `R` is an element `x_f` of `P Y` for every `f : Y ⟶ X` in - `R`. See `family_of_elements`. -* The family `x` is *compatible* if, for any `f₁ : Y₁ ⟶ X` and `f₂ : Y₂ ⟶ X` both in `R`, - and any `g₁ : Z ⟶ Y₁` and `g₂ : Z ⟶ Y₂` such that `g₁ ≫ f₁ = g₂ ≫ f₂`, the restriction of - `x_f₁` along `g₁` agrees with the restriction of `x_f₂` along `g₂`. - See `family_of_elements.compatible`. -* An *amalgamation* `t` for the family is an element of `P X` such that for every `f : Y ⟶ X` in - `R`, the restriction of `t` on `f` is `x_f`. - See `family_of_elements.is_amalgamation`. -We then say `P` is *separated* for `R` if every compatible family has at most one amalgamation, -and it is a *sheaf* for `R` if every compatible family has a unique amalgamation. -See `is_separated_for` and `is_sheaf_for`. - -In the special case where `R` is a sieve, the compatibility condition can be simplified: -* The family `x` is *compatible* if, for any `f : Y ⟶ X` in `R` and `g : Z ⟶ Y`, the restriction of - `x_f` along `g` agrees with `x_(g ≫ f)` (which is well defined since `g ≫ f` is in `R`). -See `family_of_elements.sieve_compatible` and `compatible_iff_sieve_compatible`. - -In the special case where `C` has pullbacks, the compatibility condition can be simplified: -* The family `x` is *compatible* if, for any `f : Y ⟶ X` and `g : Z ⟶ X` both in `R`, - the restriction of `x_f` along `π₁ : pullback f g ⟶ Y` agrees with the restriction of `x_g` - along `π₂ : pullback f g ⟶ Z`. -See `family_of_elements.pullback_compatible` and `pullback_compatible_iff`. - -Now given a Grothendieck topology `J`, `P` is a sheaf if it is a sheaf for every sieve in the -topology. See `is_sheaf`. - -In the case where the topology is generated by a basis, it suffices to check `P` is a sheaf for -every sieve in the pretopology. See `is_sheaf_pretopology`. - -We also provide equivalent conditions to satisfy alternate definitions given in the literature. - -* Stacks: In `equalizer.presieve.sheaf_condition`, the sheaf condition at a presieve is shown to be - equivalent to that of https://stacks.math.columbia.edu/tag/00VM (and combined with - `is_sheaf_pretopology`, this shows the notions of `is_sheaf` are exactly equivalent.) - - The condition of https://stacks.math.columbia.edu/tag/00Z8 is virtually identical to the - statement of `yoneda_condition_iff_sheaf_condition` (since the bijection described there carries - the same information as the unique existence.) - -* Maclane-Moerdijk [MM92]: Using `compatible_iff_sieve_compatible`, the definitions of `is_sheaf` - are equivalent. There are also alternate definitions given: - - Yoneda condition: Defined in `yoneda_sheaf_condition` and equivalence in - `yoneda_condition_iff_sheaf_condition`. - - Equalizer condition (Equation 3): Defined in the `equalizer.sieve` namespace, and equivalence - in `equalizer.sieve.sheaf_condition`. - - Matching family for presieves with pullback: `pullback_compatible_iff`. - - Sheaf for a pretopology (Prop 1): `is_sheaf_pretopology` combined with the previous. - - Sheaf for a pretopology as equalizer (Prop 1, bis): `equalizer.presieve.sheaf_condition` - combined with the previous. - -## Implementation - -The sheaf condition is given as a proposition, rather than a subsingleton in `Type (max u v)`. -This doesn't seem to make a big difference, other than making a couple of definitions noncomputable, -but it means that equivalent conditions can be given as `↔` statements rather than `≃` statements, -which can be convenient. - -## References - -* [MM92]: *Sheaves in geometry and logic*, Saunders MacLane, and Ieke Moerdijk: - Chapter III, Section 4. -* [Elephant]: *Sketches of an Elephant*, P. T. Johnstone: C2.1. -* https://stacks.math.columbia.edu/tag/00VL (sheaves on a pretopology or site) -* https://stacks.math.columbia.edu/tag/00ZB (sheaves on a topology) +import category_theory.sites.sheaf_of_types +import category_theory.concrete_category --/ +universes v v' u' u -universes v u namespace category_theory open opposite category_theory category limits sieve classical -namespace presieve - variables {C : Type u} [category.{v} C] -variables {P : Cᵒᵖ ⥤ Type v} -variables {X Y : C} {S : sieve X} {R : presieve X} -variables (J J₂ : grothendieck_topology C) - -/-- -A family of elements for a presheaf `P` given a collection of arrows `R` with fixed codomain `X` -consists of an element of `P Y` for every `f : Y ⟶ X` in `R`. -A presheaf is a sheaf (resp, separated) if every *compatible* family of elements has exactly one -(resp, at most one) amalgamation. - -This data is referred to as a `family` in [MM92], Chapter III, Section 4. It is also a concrete -version of the elements of the middle object in https://stacks.math.columbia.edu/tag/00VM which is -more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Elephant]. --/ -def family_of_elements (P : Cᵒᵖ ⥤ Type v) (R : presieve X) := -Π ⦃Y : C⦄ (f : Y ⟶ X), R f → P.obj (op Y) - -instance : inhabited (family_of_elements P (⊥ : presieve X)) := ⟨λ Y f, false.elim⟩ - -/-- -A family of elements for a presheaf on the presieve `R₂` can be restricted to a smaller presieve -`R₁`. --/ -def family_of_elements.restrict {R₁ R₂ : presieve X} (h : R₁ ≤ R₂) : - family_of_elements P R₂ → family_of_elements P R₁ := -λ x Y f hf, x f (h _ hf) - -/-- -A family of elements for the arrow set `R` is *compatible* if for any `f₁ : Y₁ ⟶ X` and -`f₂ : Y₂ ⟶ X` in `R`, and any `g₁ : Z ⟶ Y₁` and `g₂ : Z ⟶ Y₂`, if the square `g₁ ≫ f₁ = g₂ ≫ f₂` -commutes then the elements of `P Z` obtained by restricting the element of `P Y₁` along `g₁` and -restricting the element of `P Y₂` along `g₂` are the same. - -In special cases, this condition can be simplified, see `pullback_compatible_iff` and -`compatible_iff_sieve_compatible`. - -This is referred to as a "compatible family" in Definition C2.1.2 of [Elephant], and on nlab: -https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents --/ -def family_of_elements.compatible (x : family_of_elements P R) : Prop := -∀ ⦃Y₁ Y₂ Z⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ - (h₁ : R f₁) (h₂ : R f₂), g₁ ≫ f₁ = g₂ ≫ f₂ → P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂) - -/-- -If the category `C` has pullbacks, this is an alternative condition for a family of elements to be -compatible: For any `f : Y ⟶ X` and `g : Z ⟶ X` in the presieve `R`, the restriction of the -given elements for `f` and `g` to the pullback agree. -This is equivalent to being compatible (provided `C` has pullbacks), shown in -`pullback_compatible_iff`. - -This is the definition for a "matching" family given in [MM92], Chapter III, Section 4, -Equation (5). Viewing the type `family_of_elements` as the middle object of the fork in -https://stacks.math.columbia.edu/tag/00VM, this condition expresses that `pr₀* (x) = pr₁* (x)`, -using the notation defined there. --/ -def family_of_elements.pullback_compatible (x : family_of_elements P R) [has_pullbacks C] : Prop := -∀ ⦃Y₁ Y₂⦄ ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : R f₁) (h₂ : R f₂), - P.map (pullback.fst : pullback f₁ f₂ ⟶ _).op (x f₁ h₁) = P.map pullback.snd.op (x f₂ h₂) - -lemma pullback_compatible_iff (x : family_of_elements P R) [has_pullbacks C] : - x.compatible ↔ x.pullback_compatible := -begin - split, - { intros t Y₁ Y₂ f₁ f₂ hf₁ hf₂, - apply t, - apply pullback.condition }, - { intros t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm, - rw [←pullback.lift_fst _ _ comm, op_comp, functor_to_types.map_comp_apply, t hf₁ hf₂, - ←functor_to_types.map_comp_apply, ←op_comp, pullback.lift_snd] } -end - -/-- The restriction of a compatible family is compatible. -/ -lemma family_of_elements.compatible.restrict {R₁ R₂ : presieve X} (h : R₁ ≤ R₂) - {x : family_of_elements P R₂} : x.compatible → (x.restrict h).compatible := -λ q Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm, q g₁ g₂ (h _ h₁) (h _ h₂) comm - -/-- -Extend a family of elements to the sieve generated by an arrow set. -This is the construction described as "easy" in Lemma C2.1.3 of [Elephant]. --/ -noncomputable def family_of_elements.sieve_extend (x : family_of_elements P R) : - family_of_elements P (generate R) := -λ Z f hf, P.map (some (some_spec hf)).op (x _ (some_spec (some_spec (some_spec hf))).1) - -/-- The extension of a compatible family to the generated sieve is compatible. -/ -lemma family_of_elements.compatible.sieve_extend (x : family_of_elements P R) (hx : x.compatible) : - x.sieve_extend.compatible := -begin - intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm, - rw [←(some_spec (some_spec (some_spec h₁))).2, ←(some_spec (some_spec (some_spec h₂))).2, - ←assoc, ←assoc] at comm, - dsimp [family_of_elements.sieve_extend], - rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply], - apply hx _ _ _ _ comm, -end - -/-- The extension of a family agrees with the original family. -/ -lemma extend_agrees {x : family_of_elements P R} (t : x.compatible) {f : Y ⟶ X} (hf : R f) : - x.sieve_extend f ⟨_, 𝟙 _, f, hf, id_comp _⟩ = x f hf := -begin - have h : (generate R) f := ⟨_, _, _, hf, id_comp _⟩, - change P.map (some (some_spec h)).op (x _ _) = x f hf, - rw t (some (some_spec h)) (𝟙 _) _ hf _, - { simp }, - simp_rw [id_comp], - apply (some_spec (some_spec (some_spec h))).2, -end - -/-- The restriction of an extension is the original. -/ -@[simp] -lemma restrict_extend {x : family_of_elements P R} (t : x.compatible) : - x.sieve_extend.restrict (le_generate R) = x := -begin - ext Y f hf, - exact extend_agrees t hf, -end - -/-- -If the arrow set for a family of elements is actually a sieve (i.e. it is downward closed) then the -consistency condition can be simplified. -This is an equivalent condition, see `compatible_iff_sieve_compatible`. - -This is the notion of "matching" given for families on sieves given in [MM92], Chapter III, -Section 4, Equation 1, and nlab: https://ncatlab.org/nlab/show/matching+family. -See also the discussion before Lemma C2.1.4 of [Elephant]. --/ -def family_of_elements.sieve_compatible (x : family_of_elements P S) : Prop := -∀ ⦃Y Z⦄ (f : Y ⟶ X) (g : Z ⟶ Y) (hf), x (g ≫ f) (S.downward_closed hf g) = P.map g.op (x f hf) - -lemma compatible_iff_sieve_compatible (x : family_of_elements P S) : - x.compatible ↔ x.sieve_compatible := -begin - split, - { intros h Y Z f g hf, - simpa using h (𝟙 _) g (S.downward_closed hf g) hf (id_comp _) }, - { intros h Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ k, - simp_rw [← h f₁ g₁ h₁, k, h f₂ g₂ h₂] } -end - -lemma family_of_elements.compatible.to_sieve_compatible {x : family_of_elements P S} - (t : x.compatible) : x.sieve_compatible := -(compatible_iff_sieve_compatible x).1 t - -/-- -Two compatible families on the sieve generated by a presieve `R` are equal if and only if they are -equal when restricted to `R`. --/ -lemma restrict_inj {x₁ x₂ : family_of_elements P (generate R)} - (t₁ : x₁.compatible) (t₂ : x₂.compatible) : - x₁.restrict (le_generate R) = x₂.restrict (le_generate R) → x₁ = x₂ := -begin - intro h, - ext Z f ⟨Y, f, g, hg, rfl⟩, - rw compatible_iff_sieve_compatible at t₁ t₂, - erw [t₁ g f ⟨_, _, g, hg, id_comp _⟩, t₂ g f ⟨_, _, g, hg, id_comp _⟩], - congr' 1, - apply congr_fun (congr_fun (congr_fun h _) g) hg, -end - -/-- -Given a family of elements `x` for the sieve `S` generated by a presieve `R`, if `x` is restricted -to `R` and then extended back up to `S`, the resulting extension equals `x`. --/ -@[simp] -lemma extend_restrict {x : family_of_elements P (generate R)} (t : x.compatible) : - (x.restrict (le_generate R)).sieve_extend = x := -begin - apply restrict_inj, - { exact (t.restrict (le_generate R)).sieve_extend _ }, - { exact t }, - rw restrict_extend, - exact t.restrict (le_generate R), -end - -/-- -The given element `t` of `P.obj (op X)` is an *amalgamation* for the family of elements `x` if every -restriction `P.map f.op t = x_f` for every arrow `f` in the presieve `R`. - -This is the definition given in https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents, -and https://ncatlab.org/nlab/show/matching+family, as well as [MM92], Chapter III, Section 4, -equation (2). --/ -def family_of_elements.is_amalgamation (x : family_of_elements P R) - (t : P.obj (op X)) : Prop := -∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : R f), P.map f.op t = x f h - -lemma is_compatible_of_exists_amalgamation (x : family_of_elements P R) - (h : ∃ t, x.is_amalgamation t) : x.compatible := -begin - cases h with t ht, - intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm, - rw [←ht _ h₁, ←ht _ h₂, ←functor_to_types.map_comp_apply, ←op_comp, comm], - simp, -end - -lemma is_amalgamation_restrict {R₁ R₂ : presieve X} (h : R₁ ≤ R₂) - (x : family_of_elements P R₂) (t : P.obj (op X)) (ht : x.is_amalgamation t) : - (x.restrict h).is_amalgamation t := -λ Y f hf, ht f (h Y hf) - -lemma is_amalgamation_sieve_extend {R : presieve X} - (x : family_of_elements P R) (t : P.obj (op X)) (ht : x.is_amalgamation t) : - x.sieve_extend.is_amalgamation t := -begin - intros Y f hf, - dsimp [family_of_elements.sieve_extend], - rw [←ht _, ←functor_to_types.map_comp_apply, ←op_comp, (some_spec (some_spec (some_spec hf))).2], -end - -/-- A presheaf is separated for a presieve if there is at most one amalgamation. -/ -def is_separated_for (P : Cᵒᵖ ⥤ Type v) (R : presieve X) : Prop := -∀ (x : family_of_elements P R) (t₁ t₂), - x.is_amalgamation t₁ → x.is_amalgamation t₂ → t₁ = t₂ - -lemma is_separated_for.ext {R : presieve X} (hR : is_separated_for P R) - {t₁ t₂ : P.obj (op X)} (h : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : R f), P.map f.op t₁ = P.map f.op t₂) : -t₁ = t₂ := -hR (λ Y f hf, P.map f.op t₂) t₁ t₂ (λ Y f hf, h hf) (λ Y f hf, rfl) - -lemma is_separated_for_iff_generate : - is_separated_for P R ↔ is_separated_for P (generate R) := -begin - split, - { intros h x t₁ t₂ ht₁ ht₂, - apply h (x.restrict (le_generate R)) t₁ t₂ _ _, - { exact is_amalgamation_restrict _ x t₁ ht₁ }, - { exact is_amalgamation_restrict _ x t₂ ht₂ } }, - { intros h x t₁ t₂ ht₁ ht₂, - apply h (x.sieve_extend), - { exact is_amalgamation_sieve_extend x t₁ ht₁ }, - { exact is_amalgamation_sieve_extend x t₂ ht₂ } } -end - -lemma is_separated_for_top (P : Cᵒᵖ ⥤ Type v) : is_separated_for P (⊤ : presieve X) := -λ x t₁ t₂ h₁ h₂, -begin - have q₁ := h₁ (𝟙 X) (by simp), - have q₂ := h₂ (𝟙 X) (by simp), - simp only [op_id, functor_to_types.map_id_apply] at q₁ q₂, - rw [q₁, q₂], -end - -/-- -We define `P` to be a sheaf for the presieve `R` if every compatible family has a unique -amalgamation. - -This is the definition of a sheaf for the given presieve given in C2.1.2 of [Elephant], and -https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents. Using `compatible_iff_sieve_compatible`, -this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4. --/ -def is_sheaf_for (P : Cᵒᵖ ⥤ Type v) (R : presieve X) : Prop := -∀ (x : family_of_elements P R), x.compatible → ∃! t, x.is_amalgamation t - -/-- -This is an equivalent condition to be a sheaf, which is useful for the abstraction to local -operators on elementary toposes. However this definition is defined only for sieves, not presieves. -The equivalence between this and `is_sheaf_for` is given in `yoneda_condition_iff_sheaf_condition`. -This version is also useful to establish that being a sheaf is preserved under isomorphism of -presheaves. - -See the discussion before Equation (3) of [MM92], Chapter III, Section 4. See also C2.1.4 of -[Elephant]. This is also a direct reformulation of https://stacks.math.columbia.edu/tag/00Z8. --/ -def yoneda_sheaf_condition (P : Cᵒᵖ ⥤ Type v) (S : sieve X) : Prop := -∀ (f : S.functor ⟶ P), ∃! g, S.functor_inclusion ≫ g = f - -/-- -(Implementation). This is a (primarily internal) equivalence between natural transformations -and compatible families. - -Cf the discussion after Lemma 7.47.10 in https://stacks.math.columbia.edu/tag/00YW. See also -the proof of C2.1.4 of [Elephant], and the discussion in [MM92], Chapter III, Section 4. --/ -def nat_trans_equiv_compatible_family : - (S.functor ⟶ P) ≃ {x : family_of_elements P S // x.compatible} := -{ to_fun := λ α, - begin - refine ⟨λ Y f hf, _, _⟩, - { apply α.app (op Y) ⟨_, hf⟩ }, - { rw compatible_iff_sieve_compatible, - intros Y Z f g hf, - dsimp, - rw ← functor_to_types.naturality _ _ α g.op, - refl } - end, - inv_fun := λ t, - { app := λ Y f, t.1 _ f.2, - naturality' := λ Y Z g, - begin - ext ⟨f, hf⟩, - apply t.2.to_sieve_compatible _, - end }, - left_inv := λ α, - begin - ext X ⟨_, _⟩, - refl - end, - right_inv := - begin - rintro ⟨x, hx⟩, - refl, - end } - -/-- (Implementation). A lemma useful to prove `yoneda_condition_iff_sheaf_condition`. -/ -lemma extension_iff_amalgamation (x : S.functor ⟶ P) (g : yoneda.obj X ⟶ P) : - S.functor_inclusion ≫ g = x ↔ - (nat_trans_equiv_compatible_family x).1.is_amalgamation (yoneda_equiv g) := -begin - change _ ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S f), P.map f.op (yoneda_equiv g) = x.app (op Y) ⟨f, h⟩, - split, - { rintro rfl Y f hf, - rw yoneda_equiv_naturality, - dsimp, - simp }, -- See note [dsimp, simp]. - { intro h, - ext Y ⟨f, hf⟩, - have : _ = x.app Y _ := h f hf, - rw yoneda_equiv_naturality at this, - rw ← this, - dsimp, - simp }, -- See note [dsimp, simp]. -end - -/-- -The yoneda version of the sheaf condition is equivalent to the sheaf condition. - -C2.1.4 of [Elephant]. --/ -lemma is_sheaf_for_iff_yoneda_sheaf_condition : - is_sheaf_for P S ↔ yoneda_sheaf_condition P S := -begin - rw [is_sheaf_for, yoneda_sheaf_condition], - simp_rw [extension_iff_amalgamation], - rw equiv.forall_congr_left' nat_trans_equiv_compatible_family, - rw subtype.forall, - apply ball_congr, - intros x hx, - rw equiv.exists_unique_congr_left _, - simp, -end - -/-- -If `P` is a sheaf for the sieve `S` on `X`, a natural transformation from `S` (viewed as a functor) -to `P` can be (uniquely) extended to all of `yoneda.obj X`. - - f - S → P - ↓ ↗ - yX - --/ -noncomputable def is_sheaf_for.extend (h : is_sheaf_for P S) (f : S.functor ⟶ P) : - yoneda.obj X ⟶ P := -classical.some (is_sheaf_for_iff_yoneda_sheaf_condition.1 h f).exists - -/-- -Show that the extension of `f : S.functor ⟶ P` to all of `yoneda.obj X` is in fact an extension, ie -that the triangle below commutes, provided `P` is a sheaf for `S` - - f - S → P - ↓ ↗ - yX - --/ -@[simp, reassoc] -lemma is_sheaf_for.functor_inclusion_comp_extend (h : is_sheaf_for P S) (f : S.functor ⟶ P) : - S.functor_inclusion ≫ h.extend f = f := -classical.some_spec (is_sheaf_for_iff_yoneda_sheaf_condition.1 h f).exists - -/-- The extension of `f` to `yoneda.obj X` is unique. -/ -lemma is_sheaf_for.unique_extend (h : is_sheaf_for P S) {f : S.functor ⟶ P} (t : yoneda.obj X ⟶ P) - (ht : S.functor_inclusion ≫ t = f) : - t = h.extend f := -((is_sheaf_for_iff_yoneda_sheaf_condition.1 h f).unique ht (h.functor_inclusion_comp_extend f)) +variables {A : Type u'} [category.{v} A] -/-- -If `P` is a sheaf for the sieve `S` on `X`, then if two natural transformations from `yoneda.obj X` -to `P` agree when restricted to the subfunctor given by `S`, they are equal. --/ -lemma is_sheaf_for.hom_ext (h : is_sheaf_for P S) (t₁ t₂ : yoneda.obj X ⟶ P) - (ht : S.functor_inclusion ≫ t₁ = S.functor_inclusion ≫ t₂) : - t₁ = t₂ := -(h.unique_extend t₁ ht).trans (h.unique_extend t₂ rfl).symm - -/-- `P` is a sheaf for `R` iff it is separated for `R` and there exists an amalgamation. -/ -lemma is_separated_for_and_exists_is_amalgamation_iff_sheaf_for : - is_separated_for P R ∧ (∀ (x : family_of_elements P R), x.compatible → ∃ t, x.is_amalgamation t) ↔ - is_sheaf_for P R := -begin - rw [is_separated_for, ←forall_and_distrib], - apply forall_congr, - intro x, - split, - { intros z hx, exact exists_unique_of_exists_of_unique (z.2 hx) z.1 }, - { intros h, - refine ⟨_, (exists_of_exists_unique ∘ h)⟩, - intros t₁ t₂ ht₁ ht₂, - apply (h _).unique ht₁ ht₂, - exact is_compatible_of_exists_amalgamation x ⟨_, ht₂⟩ } -end - -/-- -If `P` is separated for `R` and every family has an amalgamation, then `P` is a sheaf for `R`. --/ -lemma is_separated_for.is_sheaf_for (t : is_separated_for P R) : - (∀ (x : family_of_elements P R), x.compatible → ∃ t, x.is_amalgamation t) → - is_sheaf_for P R := -begin - rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, - exact and.intro t, -end +variables (P : Cᵒᵖ ⥤ A) -/-- If `P` is a sheaf for `R`, it is separated for `R`. -/ -lemma is_sheaf_for.is_separated_for : is_sheaf_for P R → is_separated_for P R := -λ q, (is_separated_for_and_exists_is_amalgamation_iff_sheaf_for.2 q).1 - -/-- Get the amalgamation of the given compatible family, provided we have a sheaf. -/ -noncomputable def is_sheaf_for.amalgamate - (t : is_sheaf_for P R) (x : family_of_elements P R) (hx : x.compatible) : - P.obj (op X) := -classical.some (t x hx).exists - -lemma is_sheaf_for.is_amalgamation - (t : is_sheaf_for P R) {x : family_of_elements P R} (hx : x.compatible) : - x.is_amalgamation (t.amalgamate x hx) := -classical.some_spec (t x hx).exists - -@[simp] -lemma is_sheaf_for.valid_glue - (t : is_sheaf_for P R) {x : family_of_elements P R} (hx : x.compatible) (f : Y ⟶ X) (Hf : R f) : - P.map f.op (t.amalgamate x hx) = x f Hf := -t.is_amalgamation hx f Hf - -/-- C2.1.3 in [Elephant] -/ -lemma is_sheaf_for_iff_generate (R : presieve X) : - is_sheaf_for P R ↔ is_sheaf_for P (generate R) := -begin - rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, - rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, - rw ← is_separated_for_iff_generate, - apply and_congr (iff.refl _), - split, - { intros q x hx, - apply exists_imp_exists _ (q _ (hx.restrict (le_generate R))), - intros t ht, - simpa [hx] using is_amalgamation_sieve_extend _ _ ht }, - { intros q x hx, - apply exists_imp_exists _ (q _ (hx.sieve_extend _)), - intros t ht, - simpa [hx] using is_amalgamation_restrict (le_generate R) _ _ ht }, -end +variables {U : C} (R : presieve U) -/-- -Every presheaf is a sheaf for the family {𝟙 X}. - -[Elephant] C2.1.5(i) --/ -lemma is_sheaf_for_singleton_iso (P : Cᵒᵖ ⥤ Type v) : - is_sheaf_for P (presieve.singleton (𝟙 X)) := -begin - intros x hx, - refine ⟨x _ (presieve.singleton_self _), _, _⟩, - { rintro _ _ ⟨rfl, rfl⟩, - simp }, - { intros t ht, - simpa using ht _ (presieve.singleton_self _) } -end - -/-- -Every presheaf is a sheaf for the maximal sieve. - -[Elephant] C2.1.5(ii) --/ -lemma is_sheaf_for_top_sieve (P : Cᵒᵖ ⥤ Type v) : - is_sheaf_for P ((⊤ : sieve X) : presieve X) := -begin - rw ← generate_of_singleton_split_epi (𝟙 X), - rw ← is_sheaf_for_iff_generate, - apply is_sheaf_for_singleton_iso, -end - -/-- -If `P` is a sheaf for `S`, and it is iso to `P'`, then `P'` is a sheaf for `S`. This shows that -"being a sheaf for a presieve" is a mathematical or hygenic property. --/ -lemma is_sheaf_for_iso {P' : Cᵒᵖ ⥤ Type v} (i : P ≅ P') : is_sheaf_for P R → is_sheaf_for P' R := -begin - rw [is_sheaf_for_iff_generate R, is_sheaf_for_iff_generate R], - intro h, - rw [is_sheaf_for_iff_yoneda_sheaf_condition], - intro f, - refine ⟨h.extend (f ≫ i.inv) ≫ i.hom, by simp, _⟩, - intros g' hg', - rw [← i.comp_inv_eq, h.unique_extend (g' ≫ i.inv) (by rw reassoc_of hg')], -end - -/-- -If a presieve `R` on `X` has a subsieve `S` such that: - -* `P` is a sheaf for `S`. -* For every `f` in `R`, `P` is separated for the pullback of `S` along `f`, +variables (J : grothendieck_topology C) -then `P` is a sheaf for `R`. +namespace presheaf -This is closely related to [Elephant] C2.1.6(i). --/ -lemma is_sheaf_for_subsieve_aux (P : Cᵒᵖ ⥤ Type v) {S : sieve X} {R : presieve X} - (h : (S : presieve X) ≤ R) - (hS : is_sheaf_for P S) - (trans : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, R f → is_separated_for P (S.pullback f)) : - is_sheaf_for P R := -begin - rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, - split, - { intros x t₁ t₂ ht₁ ht₂, - exact hS.is_separated_for _ _ _ (is_amalgamation_restrict h x t₁ ht₁) - (is_amalgamation_restrict h x t₂ ht₂) }, - { intros x hx, - use hS.amalgamate _ (hx.restrict h), - intros W j hj, - apply (trans hj).ext, - intros Y f hf, - rw [←functor_to_types.map_comp_apply, ←op_comp, - hS.valid_glue (hx.restrict h) _ hf, family_of_elements.restrict, - ←hx (𝟙 _) f _ _ (id_comp _)], - simp }, -end - -/-- -If `P` is a sheaf for every pullback of the sieve `S`, then `P` is a sheaf for any presieve which -contains `S`. -This is closely related to [Elephant] C2.1.6. --/ -lemma is_sheaf_for_subsieve (P : Cᵒᵖ ⥤ Type v) {S : sieve X} {R : presieve X} - (h : (S : presieve X) ≤ R) - (trans : Π ⦃Y⦄ (f : Y ⟶ X), is_sheaf_for P (S.pullback f)) : - is_sheaf_for P R := -is_sheaf_for_subsieve_aux P h (by simpa using trans (𝟙 _)) (λ Y f hf, (trans f).is_separated_for) +noncomputable theory -/-- A presheaf is separated for a topology if it is separated for every sieve in the topology. -/ -def is_separated (P : Cᵒᵖ ⥤ Type v) : Prop := -∀ {X} (S : sieve X), S ∈ J X → is_separated_for P S +-- We follow https://stacks.math.columbia.edu/tag/00VL definition 00VR -/-- -A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology. +def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := ∀ X : A, +presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) -If the given topology is given by a pretopology, `is_sheaf_for_pretopology` shows it suffices to -check the sheaf condition at presieves in the pretopology. --/ -def is_sheaf (P : Cᵒᵖ ⥤ Type v) : Prop := -∀ ⦃X⦄ (S : sieve X), S ∈ J X → is_sheaf_for P S +end presheaf -lemma is_sheaf.is_sheaf_for {P : Cᵒᵖ ⥤ Type v} (hp : is_sheaf J P) - (R : presieve X) (hr : generate R ∈ J X) : is_sheaf_for P R := -(is_sheaf_for_iff_generate R).2 $ hp _ hr -lemma is_sheaf_of_le (P : Cᵒᵖ ⥤ Type v) {J₁ J₂ : grothendieck_topology C} : - J₁ ≤ J₂ → is_sheaf J₂ P → is_sheaf J₁ P := -λ h t X S hS, t S (h _ hS) +#exit +-- under here is the equalizer story, which is equivalent if A has products (and doesn't +-- make sense otherwise). It's described between 00VQ and 00VR in stacks. +-- we need [category.{u} A] possibly -lemma is_separated_of_is_sheaf (P : Cᵒᵖ ⥤ Type v) (h : is_sheaf J P) : is_separated J P := -λ X S hS, (h S hS).is_separated_for +variables {C : Type u} [small_category C] [has_pullbacks C] -/-- The property of being a sheaf is preserved by isomorphism. -/ -lemma is_sheaf_iso {P' : Cᵒᵖ ⥤ Type v} (i : P ≅ P') (h : is_sheaf J P) : is_sheaf J P' := -λ X S hS, is_sheaf_for_iso i (h S hS) +variables {A : Type u'} [category.{v} A] +variable [has_products A] -lemma is_sheaf_of_yoneda (h : ∀ {X} (S : sieve X), S ∈ J X → yoneda_sheaf_condition P S) : - is_sheaf J P := -λ X S hS, is_sheaf_for_iff_yoneda_sheaf_condition.2 (h _ hS) +def first_obj : A := +∏ (λ (f : Σ Y, {f : Y ⟶ X // R f}), P.obj (op f.1)) /-- -For a topology generated by a basis, it suffices to check the sheaf condition on the basis -presieves only. +The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which +contains the data used to check a family of elements for a presieve is compatible. -/ -lemma is_sheaf_pretopology [has_pullbacks C] (K : pretopology C) : - is_sheaf (K.to_grothendieck C) P ↔ (∀ {X : C} (R : presieve X), R ∈ K X → is_sheaf_for P R) := -begin - split, - { intros PJ X R hR, - rw is_sheaf_for_iff_generate, - apply PJ (sieve.generate R) ⟨_, hR, le_generate R⟩ }, - { rintro PK X S ⟨R, hR, RS⟩, - have gRS : ⇑(generate R) ≤ S, - { apply gi_generate.gc.monotone_u, - rwa sets_iff_generate }, - apply is_sheaf_for_subsieve P gRS _, - intros Y f, - rw [← pullback_arrows_comm, ← is_sheaf_for_iff_generate], - exact PK (pullback_arrows f R) (K.pullbacks f R hR) } -end - -end presieve - -namespace equalizer - -variables {C : Type v} [small_category C] (P : Cᵒᵖ ⥤ Type v) {X : C} (R : presieve X) (S : sieve X) - -noncomputable theory +def second_obj : A := +∏ (λ (fg : (Σ Y, {f : Y ⟶ X // R f}) × (Σ Z, {g : Z ⟶ X // R g})), + P.obj (op (pullback fg.1.2.1 fg.2.2.1))) -/-- -The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram -of https://stacks.math.columbia.edu/tag/00VM. --/ -def first_obj : Type v := -∏ (λ (f : Σ Y, {f : Y ⟶ X // R f}), P.obj (op f.1)) +/-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VL. -/ +def first_map : first_obj P R ⟶ second_obj P R := +pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) -/-- Show that `first_obj` is isomorphic to `family_of_elements`. -/ -@[simps] -def first_obj_eq_family : first_obj P R ≅ R.family_of_elements P := -{ hom := λ t Y f hf, pi.π (λ (f : Σ Y, {f : Y ⟶ X // R f}), P.obj (op f.1)) ⟨_, _, hf⟩ t, - inv := pi.lift (λ f x, x _ f.2.2), - hom_inv_id' := - begin - ext ⟨Y, f, hf⟩ p, - simpa, - end, - inv_hom_id' := - begin - ext x Y f hf, - apply limits.types.limit.lift_π_apply, - end } - -instance : inhabited (first_obj P (⊥ : presieve X)) := -((first_obj_eq_family P _).to_equiv).inhabited +/-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VL. -/ +def second_map : first_obj P R ⟶ second_obj P R := +pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) /-- The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram @@ -727,86 +67,16 @@ of https://stacks.math.columbia.edu/tag/00VM. def fork_map : P.obj (op X) ⟶ first_obj P R := pi.lift (λ f, P.map f.2.1.op) -/-! -This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and -the definition of `is_sheaf_for`. --/ -namespace sieve - -/-- -The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used -to check a family is compatible. --/ -def second_obj : Type v := -∏ (λ (f : Σ Y Z (g : Z ⟶ Y), {f' : Y ⟶ X // S f'}), P.obj (op f.2.1)) - -/-- The map `p` of Equations (3,4) [MM92]. -/ -def first_map : first_obj P S ⟶ second_obj P S := -pi.lift (λ fg, pi.π _ (⟨_, _, S.downward_closed fg.2.2.2.2 fg.2.2.1⟩ : Σ Y, {f : Y ⟶ X // S f})) - -instance : inhabited (second_obj P (⊥ : sieve X)) := ⟨first_map _ _ (default _)⟩ - -/-- The map `a` of Equations (3,4) [MM92]. -/ -def second_map : first_obj P S ⟶ second_obj P S := -pi.lift (λ fg, pi.π _ ⟨_, fg.2.2.2⟩ ≫ P.map fg.2.2.1.op) - -lemma w : fork_map P S ≫ first_map P S = fork_map P S ≫ second_map P S := +lemma w : fork_map P R ≫ first_map P R = fork_map P R ≫ second_map P R := begin apply limit.hom_ext, - rintro ⟨Y, Z, g, f, hf⟩, - simp [first_map, second_map, fork_map], -end - -/-- -The family of elements given by `x : first_obj P S` is compatible iff `first_map` and `second_map` -map it to the same point. --/ -lemma compatible_iff (x : first_obj P S) : - ((first_obj_eq_family P S).hom x).compatible ↔ first_map P S x = second_map P S x := -begin - rw presieve.compatible_iff_sieve_compatible, - split, - { intro t, - ext ⟨Y, Z, g, f, hf⟩, - simpa [first_map, second_map] using t _ g hf }, - { intros t Y Z f g hf, - rw types.limit_ext_iff at t, - simpa [first_map, second_map] using t ⟨Y, Z, g, f, hf⟩ } -end - -/-- `P` is a sheaf for `S`, iff the fork given by `w` is an equalizer. -/ -lemma equalizer_sheaf_condition : - presieve.is_sheaf_for P S ↔ nonempty (is_limit (fork.of_ι _ (w P S))) := -begin - rw [types.type_equalizer_iff_unique, - ← equiv.forall_congr_left (first_obj_eq_family P S).to_equiv.symm], - simp_rw ← compatible_iff, - simp only [inv_hom_id_apply, iso.to_equiv_symm_fun], - apply ball_congr, - intros x tx, - apply exists_unique_congr, - intro t, - rw ← iso.to_equiv_symm_fun, - rw equiv.eq_symm_apply, - split, - { intros q, - ext Y f hf, - simpa [first_obj_eq_family, fork_map] using q _ _ }, - { intros q Y f hf, - rw ← q, - simp [first_obj_eq_family, fork_map] } + rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩, + simp only [first_map, second_map, fork_map], + simp only [limit.lift_π, limit.lift_π_assoc, assoc, fan.mk_π_app, subtype.coe_mk, + subtype.val_eq_coe], + rw [← P.map_comp, ← op_comp, pullback.condition], + simp, end - -end sieve - -/-! -This section establishes the equivalence between the sheaf condition of -https://stacks.math.columbia.edu/tag/00VM and the definition of `is_sheaf_for`. --/ -namespace presieve - -variables [has_pullbacks C] - /-- The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which contains the data used to check a family of elements for a presieve is compatible. @@ -836,70 +106,19 @@ begin simp, end -/-- -The family of elements given by `x : first_obj P S` is compatible iff `first_map` and `second_map` -map it to the same point. --/ -lemma compatible_iff (x : first_obj P R) : - ((first_obj_eq_family P R).hom x).compatible ↔ first_map P R x = second_map P R x := -begin - rw presieve.pullback_compatible_iff, - split, - { intro t, - ext ⟨⟨Y, f, hf⟩, Z, g, hg⟩, - simpa [first_map, second_map] using t hf hg }, - { intros t Y Z f g hf hg, - rw types.limit_ext_iff at t, - simpa [first_map, second_map] using t ⟨⟨Y, f, hf⟩, Z, g, hg⟩ } -end +-- definition 3 in -/-- -`P` is a sheaf for `R`, iff the fork given by `w` is an equalizer. -See https://stacks.math.columbia.edu/tag/00VM. +-- let's go with sites definition +def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := + + +/- +A sheaf of abelian groups is a presheaf F : C^op => AbGroup such that for every X : AbGroup, the +presheaf of types given by sending U to the homset X -> F U is a sheaf. +https://stacks.math.columbia.edu/tag/00VR -/ -lemma sheaf_condition : - R.is_sheaf_for P ↔ nonempty (is_limit (fork.of_ι _ (w P R))) := -begin - rw types.type_equalizer_iff_unique, - erw ← equiv.forall_congr_left (first_obj_eq_family P R).to_equiv.symm, - simp_rw [← compatible_iff, ← iso.to_equiv_fun, equiv.apply_symm_apply], - apply ball_congr, - intros x hx, - apply exists_unique_congr, - intros t, - rw equiv.eq_symm_apply, - split, - { intros q, - ext Y f hf, - simpa [fork_map] using q _ _ }, - { intros q Y f hf, - rw ← q, - simp [fork_map] } -end -end presieve -end equalizer -variables {C : Type u} [category.{v} C] -variables (J : grothendieck_topology C) -/-- The category of sheaves on a grothendieck topology. -/ -@[derive category] -def Sheaf (J : grothendieck_topology C) : Type (max u (v+1)) := -{P : Cᵒᵖ ⥤ Type v // presieve.is_sheaf J P} - -instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := -⟨⟨(functor.const _).obj punit, - λ X S hS, - begin - simp only [grothendieck_topology.bot_covering] at hS, - subst hS, - apply presieve.is_sheaf_for_top_sieve, - end⟩⟩ - -/-- The inclusion functor from sheaves to presheaves. -/ -@[simps {rhs_md := semireducible}, derive [full, faithful]] -def Sheaf_to_presheaf : Sheaf J ⥤ (Cᵒᵖ ⥤ Type v) := -full_subcategory_inclusion (presieve.is_sheaf J) - -end category_theory + +variables {X Y : C} {S : sieve X} {R : presieve X} diff --git a/src/category_theory/sites/sheaf_of_types.lean b/src/category_theory/sites/sheaf_of_types.lean new file mode 100644 index 0000000000000..84b69b8d2141f --- /dev/null +++ b/src/category_theory/sites/sheaf_of_types.lean @@ -0,0 +1,905 @@ +/- +Copyright (c) 2020 Bhavik Mehta. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bhavik Mehta +-/ + +import category_theory.sites.pretopology +import category_theory.limits.shapes.types +import category_theory.full_subcategory + +/-! +# Sheaves on a Grothendieck topology + +Defines the notion of a sheaf on a Grothendieck topology, as well as a range of equivalent +conditions useful in different situations. + +First define what it means for a presheaf `P : Cᵒᵖ ⥤ Type v` to be a sheaf *for* a particular +presieve `R` on `X`: +* A *family of elements* `x` for `P` at `R` is an element `x_f` of `P Y` for every `f : Y ⟶ X` in + `R`. See `family_of_elements`. +* The family `x` is *compatible* if, for any `f₁ : Y₁ ⟶ X` and `f₂ : Y₂ ⟶ X` both in `R`, + and any `g₁ : Z ⟶ Y₁` and `g₂ : Z ⟶ Y₂` such that `g₁ ≫ f₁ = g₂ ≫ f₂`, the restriction of + `x_f₁` along `g₁` agrees with the restriction of `x_f₂` along `g₂`. + See `family_of_elements.compatible`. +* An *amalgamation* `t` for the family is an element of `P X` such that for every `f : Y ⟶ X` in + `R`, the restriction of `t` on `f` is `x_f`. + See `family_of_elements.is_amalgamation`. +We then say `P` is *separated* for `R` if every compatible family has at most one amalgamation, +and it is a *sheaf* for `R` if every compatible family has a unique amalgamation. +See `is_separated_for` and `is_sheaf_for`. + +In the special case where `R` is a sieve, the compatibility condition can be simplified: +* The family `x` is *compatible* if, for any `f : Y ⟶ X` in `R` and `g : Z ⟶ Y`, the restriction of + `x_f` along `g` agrees with `x_(g ≫ f)` (which is well defined since `g ≫ f` is in `R`). +See `family_of_elements.sieve_compatible` and `compatible_iff_sieve_compatible`. + +In the special case where `C` has pullbacks, the compatibility condition can be simplified: +* The family `x` is *compatible* if, for any `f : Y ⟶ X` and `g : Z ⟶ X` both in `R`, + the restriction of `x_f` along `π₁ : pullback f g ⟶ Y` agrees with the restriction of `x_g` + along `π₂ : pullback f g ⟶ Z`. +See `family_of_elements.pullback_compatible` and `pullback_compatible_iff`. + +Now given a Grothendieck topology `J`, `P` is a sheaf if it is a sheaf for every sieve in the +topology. See `is_sheaf`. + +In the case where the topology is generated by a basis, it suffices to check `P` is a sheaf for +every sieve in the pretopology. See `is_sheaf_pretopology`. + +We also provide equivalent conditions to satisfy alternate definitions given in the literature. + +* Stacks: In `equalizer.presieve.sheaf_condition`, the sheaf condition at a presieve is shown to be + equivalent to that of https://stacks.math.columbia.edu/tag/00VM (and combined with + `is_sheaf_pretopology`, this shows the notions of `is_sheaf` are exactly equivalent.) + + The condition of https://stacks.math.columbia.edu/tag/00Z8 is virtually identical to the + statement of `yoneda_condition_iff_sheaf_condition` (since the bijection described there carries + the same information as the unique existence.) + +* Maclane-Moerdijk [MM92]: Using `compatible_iff_sieve_compatible`, the definitions of `is_sheaf` + are equivalent. There are also alternate definitions given: + - Yoneda condition: Defined in `yoneda_sheaf_condition` and equivalence in + `yoneda_condition_iff_sheaf_condition`. + - Equalizer condition (Equation 3): Defined in the `equalizer.sieve` namespace, and equivalence + in `equalizer.sieve.sheaf_condition`. + - Matching family for presieves with pullback: `pullback_compatible_iff`. + - Sheaf for a pretopology (Prop 1): `is_sheaf_pretopology` combined with the previous. + - Sheaf for a pretopology as equalizer (Prop 1, bis): `equalizer.presieve.sheaf_condition` + combined with the previous. + +## Implementation + +The sheaf condition is given as a proposition, rather than a subsingleton in `Type (max u v)`. +This doesn't seem to make a big difference, other than making a couple of definitions noncomputable, +but it means that equivalent conditions can be given as `↔` statements rather than `≃` statements, +which can be convenient. + +## References + +* [MM92]: *Sheaves in geometry and logic*, Saunders MacLane, and Ieke Moerdijk: + Chapter III, Section 4. +* [Elephant]: *Sketches of an Elephant*, P. T. Johnstone: C2.1. +* https://stacks.math.columbia.edu/tag/00VL (sheaves on a pretopology or site) +* https://stacks.math.columbia.edu/tag/00ZB (sheaves on a topology) + +-/ + +universes v u +namespace category_theory + +open opposite category_theory category limits sieve classical + +namespace presieve + +variables {C : Type u} [category.{v} C] + +variables {P : Cᵒᵖ ⥤ Type v} +variables {X Y : C} {S : sieve X} {R : presieve X} +variables (J J₂ : grothendieck_topology C) + +/-- +A family of elements for a presheaf `P` given a collection of arrows `R` with fixed codomain `X` +consists of an element of `P Y` for every `f : Y ⟶ X` in `R`. +A presheaf is a sheaf (resp, separated) if every *compatible* family of elements has exactly one +(resp, at most one) amalgamation. + +This data is referred to as a `family` in [MM92], Chapter III, Section 4. It is also a concrete +version of the elements of the middle object in https://stacks.math.columbia.edu/tag/00VM which is +more useful for direct calculations. It is also used implicitly in Definition C2.1.2 in [Elephant]. +-/ +def family_of_elements (P : Cᵒᵖ ⥤ Type v) (R : presieve X) := +Π ⦃Y : C⦄ (f : Y ⟶ X), R f → P.obj (op Y) + +instance : inhabited (family_of_elements P (⊥ : presieve X)) := ⟨λ Y f, false.elim⟩ + +/-- +A family of elements for a presheaf on the presieve `R₂` can be restricted to a smaller presieve +`R₁`. +-/ +def family_of_elements.restrict {R₁ R₂ : presieve X} (h : R₁ ≤ R₂) : + family_of_elements P R₂ → family_of_elements P R₁ := +λ x Y f hf, x f (h _ hf) + +/-- +A family of elements for the arrow set `R` is *compatible* if for any `f₁ : Y₁ ⟶ X` and +`f₂ : Y₂ ⟶ X` in `R`, and any `g₁ : Z ⟶ Y₁` and `g₂ : Z ⟶ Y₂`, if the square `g₁ ≫ f₁ = g₂ ≫ f₂` +commutes then the elements of `P Z` obtained by restricting the element of `P Y₁` along `g₁` and +restricting the element of `P Y₂` along `g₂` are the same. + +In special cases, this condition can be simplified, see `pullback_compatible_iff` and +`compatible_iff_sieve_compatible`. + +This is referred to as a "compatible family" in Definition C2.1.2 of [Elephant], and on nlab: +https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents +-/ +def family_of_elements.compatible (x : family_of_elements P R) : Prop := +∀ ⦃Y₁ Y₂ Z⦄ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ + (h₁ : R f₁) (h₂ : R f₂), g₁ ≫ f₁ = g₂ ≫ f₂ → P.map g₁.op (x f₁ h₁) = P.map g₂.op (x f₂ h₂) + +/-- +If the category `C` has pullbacks, this is an alternative condition for a family of elements to be +compatible: For any `f : Y ⟶ X` and `g : Z ⟶ X` in the presieve `R`, the restriction of the +given elements for `f` and `g` to the pullback agree. +This is equivalent to being compatible (provided `C` has pullbacks), shown in +`pullback_compatible_iff`. + +This is the definition for a "matching" family given in [MM92], Chapter III, Section 4, +Equation (5). Viewing the type `family_of_elements` as the middle object of the fork in +https://stacks.math.columbia.edu/tag/00VM, this condition expresses that `pr₀* (x) = pr₁* (x)`, +using the notation defined there. +-/ +def family_of_elements.pullback_compatible (x : family_of_elements P R) [has_pullbacks C] : Prop := +∀ ⦃Y₁ Y₂⦄ ⦃f₁ : Y₁ ⟶ X⦄ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : R f₁) (h₂ : R f₂), + P.map (pullback.fst : pullback f₁ f₂ ⟶ _).op (x f₁ h₁) = P.map pullback.snd.op (x f₂ h₂) + +lemma pullback_compatible_iff (x : family_of_elements P R) [has_pullbacks C] : + x.compatible ↔ x.pullback_compatible := +begin + split, + { intros t Y₁ Y₂ f₁ f₂ hf₁ hf₂, + apply t, + apply pullback.condition }, + { intros t Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ comm, + rw [←pullback.lift_fst _ _ comm, op_comp, functor_to_types.map_comp_apply, t hf₁ hf₂, + ←functor_to_types.map_comp_apply, ←op_comp, pullback.lift_snd] } +end + +/-- The restriction of a compatible family is compatible. -/ +lemma family_of_elements.compatible.restrict {R₁ R₂ : presieve X} (h : R₁ ≤ R₂) + {x : family_of_elements P R₂} : x.compatible → (x.restrict h).compatible := +λ q Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm, q g₁ g₂ (h _ h₁) (h _ h₂) comm + +/-- +Extend a family of elements to the sieve generated by an arrow set. +This is the construction described as "easy" in Lemma C2.1.3 of [Elephant]. +-/ +noncomputable def family_of_elements.sieve_extend (x : family_of_elements P R) : + family_of_elements P (generate R) := +λ Z f hf, P.map (some (some_spec hf)).op (x _ (some_spec (some_spec (some_spec hf))).1) + +/-- The extension of a compatible family to the generated sieve is compatible. -/ +lemma family_of_elements.compatible.sieve_extend (x : family_of_elements P R) (hx : x.compatible) : + x.sieve_extend.compatible := +begin + intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm, + rw [←(some_spec (some_spec (some_spec h₁))).2, ←(some_spec (some_spec (some_spec h₂))).2, + ←assoc, ←assoc] at comm, + dsimp [family_of_elements.sieve_extend], + rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply], + apply hx _ _ _ _ comm, +end + +/-- The extension of a family agrees with the original family. -/ +lemma extend_agrees {x : family_of_elements P R} (t : x.compatible) {f : Y ⟶ X} (hf : R f) : + x.sieve_extend f ⟨_, 𝟙 _, f, hf, id_comp _⟩ = x f hf := +begin + have h : (generate R) f := ⟨_, _, _, hf, id_comp _⟩, + change P.map (some (some_spec h)).op (x _ _) = x f hf, + rw t (some (some_spec h)) (𝟙 _) _ hf _, + { simp }, + simp_rw [id_comp], + apply (some_spec (some_spec (some_spec h))).2, +end + +/-- The restriction of an extension is the original. -/ +@[simp] +lemma restrict_extend {x : family_of_elements P R} (t : x.compatible) : + x.sieve_extend.restrict (le_generate R) = x := +begin + ext Y f hf, + exact extend_agrees t hf, +end + +/-- +If the arrow set for a family of elements is actually a sieve (i.e. it is downward closed) then the +consistency condition can be simplified. +This is an equivalent condition, see `compatible_iff_sieve_compatible`. + +This is the notion of "matching" given for families on sieves given in [MM92], Chapter III, +Section 4, Equation 1, and nlab: https://ncatlab.org/nlab/show/matching+family. +See also the discussion before Lemma C2.1.4 of [Elephant]. +-/ +def family_of_elements.sieve_compatible (x : family_of_elements P S) : Prop := +∀ ⦃Y Z⦄ (f : Y ⟶ X) (g : Z ⟶ Y) (hf), x (g ≫ f) (S.downward_closed hf g) = P.map g.op (x f hf) + +lemma compatible_iff_sieve_compatible (x : family_of_elements P S) : + x.compatible ↔ x.sieve_compatible := +begin + split, + { intros h Y Z f g hf, + simpa using h (𝟙 _) g (S.downward_closed hf g) hf (id_comp _) }, + { intros h Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ k, + simp_rw [← h f₁ g₁ h₁, k, h f₂ g₂ h₂] } +end + +lemma family_of_elements.compatible.to_sieve_compatible {x : family_of_elements P S} + (t : x.compatible) : x.sieve_compatible := +(compatible_iff_sieve_compatible x).1 t + +/-- +Two compatible families on the sieve generated by a presieve `R` are equal if and only if they are +equal when restricted to `R`. +-/ +lemma restrict_inj {x₁ x₂ : family_of_elements P (generate R)} + (t₁ : x₁.compatible) (t₂ : x₂.compatible) : + x₁.restrict (le_generate R) = x₂.restrict (le_generate R) → x₁ = x₂ := +begin + intro h, + ext Z f ⟨Y, f, g, hg, rfl⟩, + rw compatible_iff_sieve_compatible at t₁ t₂, + erw [t₁ g f ⟨_, _, g, hg, id_comp _⟩, t₂ g f ⟨_, _, g, hg, id_comp _⟩], + congr' 1, + apply congr_fun (congr_fun (congr_fun h _) g) hg, +end + +/-- +Given a family of elements `x` for the sieve `S` generated by a presieve `R`, if `x` is restricted +to `R` and then extended back up to `S`, the resulting extension equals `x`. +-/ +@[simp] +lemma extend_restrict {x : family_of_elements P (generate R)} (t : x.compatible) : + (x.restrict (le_generate R)).sieve_extend = x := +begin + apply restrict_inj, + { exact (t.restrict (le_generate R)).sieve_extend _ }, + { exact t }, + rw restrict_extend, + exact t.restrict (le_generate R), +end + +/-- +The given element `t` of `P.obj (op X)` is an *amalgamation* for the family of elements `x` if every +restriction `P.map f.op t = x_f` for every arrow `f` in the presieve `R`. + +This is the definition given in https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents, +and https://ncatlab.org/nlab/show/matching+family, as well as [MM92], Chapter III, Section 4, +equation (2). +-/ +def family_of_elements.is_amalgamation (x : family_of_elements P R) + (t : P.obj (op X)) : Prop := +∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : R f), P.map f.op t = x f h + +lemma is_compatible_of_exists_amalgamation (x : family_of_elements P R) + (h : ∃ t, x.is_amalgamation t) : x.compatible := +begin + cases h with t ht, + intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ comm, + rw [←ht _ h₁, ←ht _ h₂, ←functor_to_types.map_comp_apply, ←op_comp, comm], + simp, +end + +lemma is_amalgamation_restrict {R₁ R₂ : presieve X} (h : R₁ ≤ R₂) + (x : family_of_elements P R₂) (t : P.obj (op X)) (ht : x.is_amalgamation t) : + (x.restrict h).is_amalgamation t := +λ Y f hf, ht f (h Y hf) + +lemma is_amalgamation_sieve_extend {R : presieve X} + (x : family_of_elements P R) (t : P.obj (op X)) (ht : x.is_amalgamation t) : + x.sieve_extend.is_amalgamation t := +begin + intros Y f hf, + dsimp [family_of_elements.sieve_extend], + rw [←ht _, ←functor_to_types.map_comp_apply, ←op_comp, (some_spec (some_spec (some_spec hf))).2], +end + +/-- A presheaf is separated for a presieve if there is at most one amalgamation. -/ +def is_separated_for (P : Cᵒᵖ ⥤ Type v) (R : presieve X) : Prop := +∀ (x : family_of_elements P R) (t₁ t₂), + x.is_amalgamation t₁ → x.is_amalgamation t₂ → t₁ = t₂ + +lemma is_separated_for.ext {R : presieve X} (hR : is_separated_for P R) + {t₁ t₂ : P.obj (op X)} (h : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (hf : R f), P.map f.op t₁ = P.map f.op t₂) : +t₁ = t₂ := +hR (λ Y f hf, P.map f.op t₂) t₁ t₂ (λ Y f hf, h hf) (λ Y f hf, rfl) + +lemma is_separated_for_iff_generate : + is_separated_for P R ↔ is_separated_for P (generate R) := +begin + split, + { intros h x t₁ t₂ ht₁ ht₂, + apply h (x.restrict (le_generate R)) t₁ t₂ _ _, + { exact is_amalgamation_restrict _ x t₁ ht₁ }, + { exact is_amalgamation_restrict _ x t₂ ht₂ } }, + { intros h x t₁ t₂ ht₁ ht₂, + apply h (x.sieve_extend), + { exact is_amalgamation_sieve_extend x t₁ ht₁ }, + { exact is_amalgamation_sieve_extend x t₂ ht₂ } } +end + +lemma is_separated_for_top (P : Cᵒᵖ ⥤ Type v) : is_separated_for P (⊤ : presieve X) := +λ x t₁ t₂ h₁ h₂, +begin + have q₁ := h₁ (𝟙 X) (by simp), + have q₂ := h₂ (𝟙 X) (by simp), + simp only [op_id, functor_to_types.map_id_apply] at q₁ q₂, + rw [q₁, q₂], +end + +/-- +We define `P` to be a sheaf for the presieve `R` if every compatible family has a unique +amalgamation. + +This is the definition of a sheaf for the given presieve given in C2.1.2 of [Elephant], and +https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents. Using `compatible_iff_sieve_compatible`, +this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4. +-/ +def is_sheaf_for (P : Cᵒᵖ ⥤ Type v) (R : presieve X) : Prop := +∀ (x : family_of_elements P R), x.compatible → ∃! t, x.is_amalgamation t + +/-- +This is an equivalent condition to be a sheaf, which is useful for the abstraction to local +operators on elementary toposes. However this definition is defined only for sieves, not presieves. +The equivalence between this and `is_sheaf_for` is given in `yoneda_condition_iff_sheaf_condition`. +This version is also useful to establish that being a sheaf is preserved under isomorphism of +presheaves. + +See the discussion before Equation (3) of [MM92], Chapter III, Section 4. See also C2.1.4 of +[Elephant]. This is also a direct reformulation of https://stacks.math.columbia.edu/tag/00Z8. +-/ +def yoneda_sheaf_condition (P : Cᵒᵖ ⥤ Type v) (S : sieve X) : Prop := +∀ (f : S.functor ⟶ P), ∃! g, S.functor_inclusion ≫ g = f + +/-- +(Implementation). This is a (primarily internal) equivalence between natural transformations +and compatible families. + +Cf the discussion after Lemma 7.47.10 in https://stacks.math.columbia.edu/tag/00YW. See also +the proof of C2.1.4 of [Elephant], and the discussion in [MM92], Chapter III, Section 4. +-/ +def nat_trans_equiv_compatible_family : + (S.functor ⟶ P) ≃ {x : family_of_elements P S // x.compatible} := +{ to_fun := λ α, + begin + refine ⟨λ Y f hf, _, _⟩, + { apply α.app (op Y) ⟨_, hf⟩ }, + { rw compatible_iff_sieve_compatible, + intros Y Z f g hf, + dsimp, + rw ← functor_to_types.naturality _ _ α g.op, + refl } + end, + inv_fun := λ t, + { app := λ Y f, t.1 _ f.2, + naturality' := λ Y Z g, + begin + ext ⟨f, hf⟩, + apply t.2.to_sieve_compatible _, + end }, + left_inv := λ α, + begin + ext X ⟨_, _⟩, + refl + end, + right_inv := + begin + rintro ⟨x, hx⟩, + refl, + end } + +/-- (Implementation). A lemma useful to prove `yoneda_condition_iff_sheaf_condition`. -/ +lemma extension_iff_amalgamation (x : S.functor ⟶ P) (g : yoneda.obj X ⟶ P) : + S.functor_inclusion ≫ g = x ↔ + (nat_trans_equiv_compatible_family x).1.is_amalgamation (yoneda_equiv g) := +begin + change _ ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S f), P.map f.op (yoneda_equiv g) = x.app (op Y) ⟨f, h⟩, + split, + { rintro rfl Y f hf, + rw yoneda_equiv_naturality, + dsimp, + simp }, -- See note [dsimp, simp]. + { intro h, + ext Y ⟨f, hf⟩, + have : _ = x.app Y _ := h f hf, + rw yoneda_equiv_naturality at this, + rw ← this, + dsimp, + simp }, -- See note [dsimp, simp]. +end + +/-- +The yoneda version of the sheaf condition is equivalent to the sheaf condition. + +C2.1.4 of [Elephant]. +-/ +lemma is_sheaf_for_iff_yoneda_sheaf_condition : + is_sheaf_for P S ↔ yoneda_sheaf_condition P S := +begin + rw [is_sheaf_for, yoneda_sheaf_condition], + simp_rw [extension_iff_amalgamation], + rw equiv.forall_congr_left' nat_trans_equiv_compatible_family, + rw subtype.forall, + apply ball_congr, + intros x hx, + rw equiv.exists_unique_congr_left _, + simp, +end + +/-- +If `P` is a sheaf for the sieve `S` on `X`, a natural transformation from `S` (viewed as a functor) +to `P` can be (uniquely) extended to all of `yoneda.obj X`. + + f + S → P + ↓ ↗ + yX + +-/ +noncomputable def is_sheaf_for.extend (h : is_sheaf_for P S) (f : S.functor ⟶ P) : + yoneda.obj X ⟶ P := +classical.some (is_sheaf_for_iff_yoneda_sheaf_condition.1 h f).exists + +/-- +Show that the extension of `f : S.functor ⟶ P` to all of `yoneda.obj X` is in fact an extension, ie +that the triangle below commutes, provided `P` is a sheaf for `S` + + f + S → P + ↓ ↗ + yX + +-/ +@[simp, reassoc] +lemma is_sheaf_for.functor_inclusion_comp_extend (h : is_sheaf_for P S) (f : S.functor ⟶ P) : + S.functor_inclusion ≫ h.extend f = f := +classical.some_spec (is_sheaf_for_iff_yoneda_sheaf_condition.1 h f).exists + +/-- The extension of `f` to `yoneda.obj X` is unique. -/ +lemma is_sheaf_for.unique_extend (h : is_sheaf_for P S) {f : S.functor ⟶ P} (t : yoneda.obj X ⟶ P) + (ht : S.functor_inclusion ≫ t = f) : + t = h.extend f := +((is_sheaf_for_iff_yoneda_sheaf_condition.1 h f).unique ht (h.functor_inclusion_comp_extend f)) + +/-- +If `P` is a sheaf for the sieve `S` on `X`, then if two natural transformations from `yoneda.obj X` +to `P` agree when restricted to the subfunctor given by `S`, they are equal. +-/ +lemma is_sheaf_for.hom_ext (h : is_sheaf_for P S) (t₁ t₂ : yoneda.obj X ⟶ P) + (ht : S.functor_inclusion ≫ t₁ = S.functor_inclusion ≫ t₂) : + t₁ = t₂ := +(h.unique_extend t₁ ht).trans (h.unique_extend t₂ rfl).symm + +/-- `P` is a sheaf for `R` iff it is separated for `R` and there exists an amalgamation. -/ +lemma is_separated_for_and_exists_is_amalgamation_iff_sheaf_for : + is_separated_for P R ∧ (∀ (x : family_of_elements P R), x.compatible → ∃ t, x.is_amalgamation t) ↔ + is_sheaf_for P R := +begin + rw [is_separated_for, ←forall_and_distrib], + apply forall_congr, + intro x, + split, + { intros z hx, exact exists_unique_of_exists_of_unique (z.2 hx) z.1 }, + { intros h, + refine ⟨_, (exists_of_exists_unique ∘ h)⟩, + intros t₁ t₂ ht₁ ht₂, + apply (h _).unique ht₁ ht₂, + exact is_compatible_of_exists_amalgamation x ⟨_, ht₂⟩ } +end + +/-- +If `P` is separated for `R` and every family has an amalgamation, then `P` is a sheaf for `R`. +-/ +lemma is_separated_for.is_sheaf_for (t : is_separated_for P R) : + (∀ (x : family_of_elements P R), x.compatible → ∃ t, x.is_amalgamation t) → + is_sheaf_for P R := +begin + rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, + exact and.intro t, +end + +/-- If `P` is a sheaf for `R`, it is separated for `R`. -/ +lemma is_sheaf_for.is_separated_for : is_sheaf_for P R → is_separated_for P R := +λ q, (is_separated_for_and_exists_is_amalgamation_iff_sheaf_for.2 q).1 + +/-- Get the amalgamation of the given compatible family, provided we have a sheaf. -/ +noncomputable def is_sheaf_for.amalgamate + (t : is_sheaf_for P R) (x : family_of_elements P R) (hx : x.compatible) : + P.obj (op X) := +classical.some (t x hx).exists + +lemma is_sheaf_for.is_amalgamation + (t : is_sheaf_for P R) {x : family_of_elements P R} (hx : x.compatible) : + x.is_amalgamation (t.amalgamate x hx) := +classical.some_spec (t x hx).exists + +@[simp] +lemma is_sheaf_for.valid_glue + (t : is_sheaf_for P R) {x : family_of_elements P R} (hx : x.compatible) (f : Y ⟶ X) (Hf : R f) : + P.map f.op (t.amalgamate x hx) = x f Hf := +t.is_amalgamation hx f Hf + +/-- C2.1.3 in [Elephant] -/ +lemma is_sheaf_for_iff_generate (R : presieve X) : + is_sheaf_for P R ↔ is_sheaf_for P (generate R) := +begin + rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, + rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, + rw ← is_separated_for_iff_generate, + apply and_congr (iff.refl _), + split, + { intros q x hx, + apply exists_imp_exists _ (q _ (hx.restrict (le_generate R))), + intros t ht, + simpa [hx] using is_amalgamation_sieve_extend _ _ ht }, + { intros q x hx, + apply exists_imp_exists _ (q _ (hx.sieve_extend _)), + intros t ht, + simpa [hx] using is_amalgamation_restrict (le_generate R) _ _ ht }, +end + +/-- +Every presheaf is a sheaf for the family {𝟙 X}. + +[Elephant] C2.1.5(i) +-/ +lemma is_sheaf_for_singleton_iso (P : Cᵒᵖ ⥤ Type v) : + is_sheaf_for P (presieve.singleton (𝟙 X)) := +begin + intros x hx, + refine ⟨x _ (presieve.singleton_self _), _, _⟩, + { rintro _ _ ⟨rfl, rfl⟩, + simp }, + { intros t ht, + simpa using ht _ (presieve.singleton_self _) } +end + +/-- +Every presheaf is a sheaf for the maximal sieve. + +[Elephant] C2.1.5(ii) +-/ +lemma is_sheaf_for_top_sieve (P : Cᵒᵖ ⥤ Type v) : + is_sheaf_for P ((⊤ : sieve X) : presieve X) := +begin + rw ← generate_of_singleton_split_epi (𝟙 X), + rw ← is_sheaf_for_iff_generate, + apply is_sheaf_for_singleton_iso, +end + +/-- +If `P` is a sheaf for `S`, and it is iso to `P'`, then `P'` is a sheaf for `S`. This shows that +"being a sheaf for a presieve" is a mathematical or hygenic property. +-/ +lemma is_sheaf_for_iso {P' : Cᵒᵖ ⥤ Type v} (i : P ≅ P') : is_sheaf_for P R → is_sheaf_for P' R := +begin + rw [is_sheaf_for_iff_generate R, is_sheaf_for_iff_generate R], + intro h, + rw [is_sheaf_for_iff_yoneda_sheaf_condition], + intro f, + refine ⟨h.extend (f ≫ i.inv) ≫ i.hom, by simp, _⟩, + intros g' hg', + rw [← i.comp_inv_eq, h.unique_extend (g' ≫ i.inv) (by rw reassoc_of hg')], +end + +/-- +If a presieve `R` on `X` has a subsieve `S` such that: + +* `P` is a sheaf for `S`. +* For every `f` in `R`, `P` is separated for the pullback of `S` along `f`, + +then `P` is a sheaf for `R`. + +This is closely related to [Elephant] C2.1.6(i). +-/ +lemma is_sheaf_for_subsieve_aux (P : Cᵒᵖ ⥤ Type v) {S : sieve X} {R : presieve X} + (h : (S : presieve X) ≤ R) + (hS : is_sheaf_for P S) + (trans : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, R f → is_separated_for P (S.pullback f)) : + is_sheaf_for P R := +begin + rw ← is_separated_for_and_exists_is_amalgamation_iff_sheaf_for, + split, + { intros x t₁ t₂ ht₁ ht₂, + exact hS.is_separated_for _ _ _ (is_amalgamation_restrict h x t₁ ht₁) + (is_amalgamation_restrict h x t₂ ht₂) }, + { intros x hx, + use hS.amalgamate _ (hx.restrict h), + intros W j hj, + apply (trans hj).ext, + intros Y f hf, + rw [←functor_to_types.map_comp_apply, ←op_comp, + hS.valid_glue (hx.restrict h) _ hf, family_of_elements.restrict, + ←hx (𝟙 _) f _ _ (id_comp _)], + simp }, +end + +/-- +If `P` is a sheaf for every pullback of the sieve `S`, then `P` is a sheaf for any presieve which +contains `S`. +This is closely related to [Elephant] C2.1.6. +-/ +lemma is_sheaf_for_subsieve (P : Cᵒᵖ ⥤ Type v) {S : sieve X} {R : presieve X} + (h : (S : presieve X) ≤ R) + (trans : Π ⦃Y⦄ (f : Y ⟶ X), is_sheaf_for P (S.pullback f)) : + is_sheaf_for P R := +is_sheaf_for_subsieve_aux P h (by simpa using trans (𝟙 _)) (λ Y f hf, (trans f).is_separated_for) + +/-- A presheaf is separated for a topology if it is separated for every sieve in the topology. -/ +def is_separated (P : Cᵒᵖ ⥤ Type v) : Prop := +∀ {X} (S : sieve X), S ∈ J X → is_separated_for P S + +/-- +A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology. + +If the given topology is given by a pretopology, `is_sheaf_for_pretopology` shows it suffices to +check the sheaf condition at presieves in the pretopology. +-/ +def is_sheaf (P : Cᵒᵖ ⥤ Type v) : Prop := +∀ ⦃X⦄ (S : sieve X), S ∈ J X → is_sheaf_for P S + +lemma is_sheaf.is_sheaf_for {P : Cᵒᵖ ⥤ Type v} (hp : is_sheaf J P) + (R : presieve X) (hr : generate R ∈ J X) : is_sheaf_for P R := +(is_sheaf_for_iff_generate R).2 $ hp _ hr + +lemma is_sheaf_of_le (P : Cᵒᵖ ⥤ Type v) {J₁ J₂ : grothendieck_topology C} : + J₁ ≤ J₂ → is_sheaf J₂ P → is_sheaf J₁ P := +λ h t X S hS, t S (h _ hS) + +lemma is_separated_of_is_sheaf (P : Cᵒᵖ ⥤ Type v) (h : is_sheaf J P) : is_separated J P := +λ X S hS, (h S hS).is_separated_for + +/-- The property of being a sheaf is preserved by isomorphism. -/ +lemma is_sheaf_iso {P' : Cᵒᵖ ⥤ Type v} (i : P ≅ P') (h : is_sheaf J P) : is_sheaf J P' := +λ X S hS, is_sheaf_for_iso i (h S hS) + +lemma is_sheaf_of_yoneda (h : ∀ {X} (S : sieve X), S ∈ J X → yoneda_sheaf_condition P S) : + is_sheaf J P := +λ X S hS, is_sheaf_for_iff_yoneda_sheaf_condition.2 (h _ hS) + +/-- +For a topology generated by a basis, it suffices to check the sheaf condition on the basis +presieves only. +-/ +lemma is_sheaf_pretopology [has_pullbacks C] (K : pretopology C) : + is_sheaf (K.to_grothendieck C) P ↔ (∀ {X : C} (R : presieve X), R ∈ K X → is_sheaf_for P R) := +begin + split, + { intros PJ X R hR, + rw is_sheaf_for_iff_generate, + apply PJ (sieve.generate R) ⟨_, hR, le_generate R⟩ }, + { rintro PK X S ⟨R, hR, RS⟩, + have gRS : ⇑(generate R) ≤ S, + { apply gi_generate.gc.monotone_u, + rwa sets_iff_generate }, + apply is_sheaf_for_subsieve P gRS _, + intros Y f, + rw [← pullback_arrows_comm, ← is_sheaf_for_iff_generate], + exact PK (pullback_arrows f R) (K.pullbacks f R hR) } +end + +end presieve + +namespace equalizer + +variables {C : Type v} [small_category C] (P : Cᵒᵖ ⥤ Type v) {X : C} (R : presieve X) (S : sieve X) + +noncomputable theory + +/-- +The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram +of https://stacks.math.columbia.edu/tag/00VM. +-/ +def first_obj : Type v := +∏ (λ (f : Σ Y, {f : Y ⟶ X // R f}), P.obj (op f.1)) + +/-- Show that `first_obj` is isomorphic to `family_of_elements`. -/ +@[simps] +def first_obj_eq_family : first_obj P R ≅ R.family_of_elements P := +{ hom := λ t Y f hf, pi.π (λ (f : Σ Y, {f : Y ⟶ X // R f}), P.obj (op f.1)) ⟨_, _, hf⟩ t, + inv := pi.lift (λ f x, x _ f.2.2), + hom_inv_id' := + begin + ext ⟨Y, f, hf⟩ p, + simpa, + end, + inv_hom_id' := + begin + ext x Y f hf, + apply limits.types.limit.lift_π_apply, + end } + +instance : inhabited (first_obj P (⊥ : presieve X)) := +((first_obj_eq_family P _).to_equiv).inhabited + +/-- +The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram +of https://stacks.math.columbia.edu/tag/00VM. +-/ +def fork_map : P.obj (op X) ⟶ first_obj P R := +pi.lift (λ f, P.map f.2.1.op) + +/-! +This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and +the definition of `is_sheaf_for`. +-/ +namespace sieve + +/-- +The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used +to check a family is compatible. +-/ +def second_obj : Type v := +∏ (λ (f : Σ Y Z (g : Z ⟶ Y), {f' : Y ⟶ X // S f'}), P.obj (op f.2.1)) + +/-- The map `p` of Equations (3,4) [MM92]. -/ +def first_map : first_obj P S ⟶ second_obj P S := +pi.lift (λ fg, pi.π _ (⟨_, _, S.downward_closed fg.2.2.2.2 fg.2.2.1⟩ : Σ Y, {f : Y ⟶ X // S f})) + +instance : inhabited (second_obj P (⊥ : sieve X)) := ⟨first_map _ _ (default _)⟩ + +/-- The map `a` of Equations (3,4) [MM92]. -/ +def second_map : first_obj P S ⟶ second_obj P S := +pi.lift (λ fg, pi.π _ ⟨_, fg.2.2.2⟩ ≫ P.map fg.2.2.1.op) + +lemma w : fork_map P S ≫ first_map P S = fork_map P S ≫ second_map P S := +begin + apply limit.hom_ext, + rintro ⟨Y, Z, g, f, hf⟩, + simp [first_map, second_map, fork_map], +end + +/-- +The family of elements given by `x : first_obj P S` is compatible iff `first_map` and `second_map` +map it to the same point. +-/ +lemma compatible_iff (x : first_obj P S) : + ((first_obj_eq_family P S).hom x).compatible ↔ first_map P S x = second_map P S x := +begin + rw presieve.compatible_iff_sieve_compatible, + split, + { intro t, + ext ⟨Y, Z, g, f, hf⟩, + simpa [first_map, second_map] using t _ g hf }, + { intros t Y Z f g hf, + rw types.limit_ext_iff at t, + simpa [first_map, second_map] using t ⟨Y, Z, g, f, hf⟩ } +end + +/-- `P` is a sheaf for `S`, iff the fork given by `w` is an equalizer. -/ +lemma equalizer_sheaf_condition : + presieve.is_sheaf_for P S ↔ nonempty (is_limit (fork.of_ι _ (w P S))) := +begin + rw [types.type_equalizer_iff_unique, + ← equiv.forall_congr_left (first_obj_eq_family P S).to_equiv.symm], + simp_rw ← compatible_iff, + simp only [inv_hom_id_apply, iso.to_equiv_symm_fun], + apply ball_congr, + intros x tx, + apply exists_unique_congr, + intro t, + rw ← iso.to_equiv_symm_fun, + rw equiv.eq_symm_apply, + split, + { intros q, + ext Y f hf, + simpa [first_obj_eq_family, fork_map] using q _ _ }, + { intros q Y f hf, + rw ← q, + simp [first_obj_eq_family, fork_map] } +end + +end sieve + +/-! +This section establishes the equivalence between the sheaf condition of +https://stacks.math.columbia.edu/tag/00VM and the definition of `is_sheaf_for`. +-/ +namespace presieve + +variables [has_pullbacks C] + +/-- +The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which +contains the data used to check a family of elements for a presieve is compatible. +-/ +def second_obj : Type v := +∏ (λ (fg : (Σ Y, {f : Y ⟶ X // R f}) × (Σ Z, {g : Z ⟶ X // R g})), + P.obj (op (pullback fg.1.2.1 fg.2.2.1))) + +/-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VL. -/ +def first_map : first_obj P R ⟶ second_obj P R := +pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) + +instance : inhabited (second_obj P (⊥ : presieve X)) := ⟨first_map _ _ (default _)⟩ + +/-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VL. -/ +def second_map : first_obj P R ⟶ second_obj P R := +pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) + +lemma w : fork_map P R ≫ first_map P R = fork_map P R ≫ second_map P R := +begin + apply limit.hom_ext, + rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩, + simp only [first_map, second_map, fork_map], + simp only [limit.lift_π, limit.lift_π_assoc, assoc, fan.mk_π_app, subtype.coe_mk, + subtype.val_eq_coe], + rw [← P.map_comp, ← op_comp, pullback.condition], + simp, +end + +/-- +The family of elements given by `x : first_obj P S` is compatible iff `first_map` and `second_map` +map it to the same point. +-/ +lemma compatible_iff (x : first_obj P R) : + ((first_obj_eq_family P R).hom x).compatible ↔ first_map P R x = second_map P R x := +begin + rw presieve.pullback_compatible_iff, + split, + { intro t, + ext ⟨⟨Y, f, hf⟩, Z, g, hg⟩, + simpa [first_map, second_map] using t hf hg }, + { intros t Y Z f g hf hg, + rw types.limit_ext_iff at t, + simpa [first_map, second_map] using t ⟨⟨Y, f, hf⟩, Z, g, hg⟩ } +end + +/-- +`P` is a sheaf for `R`, iff the fork given by `w` is an equalizer. +See https://stacks.math.columbia.edu/tag/00VM. +-/ +lemma sheaf_condition : + R.is_sheaf_for P ↔ nonempty (is_limit (fork.of_ι _ (w P R))) := +begin + rw types.type_equalizer_iff_unique, + erw ← equiv.forall_congr_left (first_obj_eq_family P R).to_equiv.symm, + simp_rw [← compatible_iff, ← iso.to_equiv_fun, equiv.apply_symm_apply], + apply ball_congr, + intros x hx, + apply exists_unique_congr, + intros t, + rw equiv.eq_symm_apply, + split, + { intros q, + ext Y f hf, + simpa [fork_map] using q _ _ }, + { intros q Y f hf, + rw ← q, + simp [fork_map] } +end + +end presieve +end equalizer + +variables {C : Type u} [category.{v} C] +variables (J : grothendieck_topology C) + +/-- The category of sheaves on a grothendieck topology. -/ +@[derive category] +def Sheaf (J : grothendieck_topology C) : Type (max u (v+1)) := +{P : Cᵒᵖ ⥤ Type v // presieve.is_sheaf J P} + +instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := +⟨⟨(functor.const _).obj punit, + λ X S hS, + begin + simp only [grothendieck_topology.bot_covering] at hS, + subst hS, + apply presieve.is_sheaf_for_top_sieve, + end⟩⟩ + +/-- The inclusion functor from sheaves to presheaves. -/ +@[simps {rhs_md := semireducible}, derive [full, faithful]] +def Sheaf_to_presheaf : Sheaf J ⥤ (Cᵒᵖ ⥤ Type v) := +full_subcategory_inclusion (presieve.is_sheaf J) + +end category_theory From e8009e120965c7bfe9326bd37758ac2df5b78019 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 19 Dec 2020 16:41:45 +0000 Subject: [PATCH 02/21] sheaf challenge! --- src/category_theory/sites/sheaf.lean | 88 +++++++++++----------------- 1 file changed, 34 insertions(+), 54 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index f7018700dd08c..12febfe9942e0 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -1,73 +1,82 @@ --- sheaves taking values in a category - import category_theory.sites.sheaf_of_types import category_theory.concrete_category +-- sheaves taking values in objects of a category + universes v v' u' u +noncomputable theory + namespace category_theory open opposite category_theory category limits sieve classical +namespace presheaf + variables {C : Type u} [category.{v} C] variables {A : Type u'} [category.{v} A] -variables (P : Cᵒᵖ ⥤ A) - -variables {U : C} (R : presieve U) - variables (J : grothendieck_topology C) -namespace presheaf +-- We follow https://stacks.math.columbia.edu/tag/00VL definition 00VR + +/- +A sheaf of abelian groups is a presheaf F : C^op => AbGroup such that for every X : AbGroup, the +presheaf of types given by sending U to the homset X -> F U is a sheaf. +https://stacks.math.columbia.edu/tag/00VR +-/ -noncomputable theory --- We follow https://stacks.math.columbia.edu/tag/00VL definition 00VR def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := ∀ X : A, presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) end presheaf +namespace presheaf -#exit -- under here is the equalizer story, which is equivalent if A has products (and doesn't -- make sense otherwise). It's described between 00VQ and 00VR in stacks. -- we need [category.{u} A] possibly -variables {C : Type u} [small_category C] [has_pullbacks C] +variables {C : Type v} [small_category C] [has_pullbacks C] -variables {A : Type u'} [category.{v} A] -variable [has_products A] +variables {A : Type u} [category.{v} A] [has_products A] + +variables (J : grothendieck_topology C) + +variables {U : C} (R : presieve U) + +variables (P : Cᵒᵖ ⥤ A) def first_obj : A := -∏ (λ (f : Σ Y, {f : Y ⟶ X // R f}), P.obj (op f.1)) +∏ (λ (f : Σ V, {f : V ⟶ U // R f}), P.obj (op f.1)) /-- The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which contains the data used to check a family of elements for a presieve is compatible. -/ def second_obj : A := -∏ (λ (fg : (Σ Y, {f : Y ⟶ X // R f}) × (Σ Z, {g : Z ⟶ X // R g})), +∏ (λ (fg : (Σ V, {f : V ⟶ U // R f}) × (Σ W, {g : W ⟶ U // R g})), P.obj (op (pullback fg.1.2.1 fg.2.2.1))) /-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VL. -/ -def first_map : first_obj P R ⟶ second_obj P R := +def first_map : first_obj R P ⟶ second_obj R P := pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) /-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VL. -/ -def second_map : first_obj P R ⟶ second_obj P R := +def second_map : first_obj R P ⟶ second_obj R P := pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) /-- The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram of https://stacks.math.columbia.edu/tag/00VM. -/ -def fork_map : P.obj (op X) ⟶ first_obj P R := +def fork_map : P.obj (op U) ⟶ first_obj R P := pi.lift (λ f, P.map f.2.1.op) -lemma w : fork_map P R ≫ first_map P R = fork_map P R ≫ second_map P R := +lemma w : fork_map R P ≫ first_map R P = fork_map R P ≫ second_map R P := begin apply limit.hom_ext, rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩, @@ -77,47 +86,18 @@ begin rw [← P.map_comp, ← op_comp, pullback.condition], simp, end -/-- -The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which -contains the data used to check a family of elements for a presieve is compatible. --/ -def second_obj : Type v := -∏ (λ (fg : (Σ Y, {f : Y ⟶ X // R f}) × (Σ Z, {g : Z ⟶ X // R g})), - P.obj (op (pullback fg.1.2.1 fg.2.2.1))) - -/-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VL. -/ -def first_map : first_obj P R ⟶ second_obj P R := -pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) -instance : inhabited (second_obj P (⊥ : presieve X)) := ⟨first_map _ _ (default _)⟩ +-- definition 3 in Bhaviks list -/-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VL. -/ -def second_map : first_obj P R ⟶ second_obj P R := -pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) +def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), +nonempty (is_limit (fork.of_ι _ (w R P))) -lemma w : fork_map P R ≫ first_map P R = fork_map P R ≫ second_map P R := +theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : +is_sheaf J P ↔ is_sheaf' J P := begin - apply limit.hom_ext, - rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩, - simp only [first_map, second_map, fork_map], - simp only [limit.lift_π, limit.lift_π_assoc, assoc, fan.mk_π_app, subtype.coe_mk, - subtype.val_eq_coe], - rw [← P.map_comp, ← op_comp, pullback.condition], - simp, + sorry end --- definition 3 in - --- let's go with sites definition -def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := - - -/- -A sheaf of abelian groups is a presheaf F : C^op => AbGroup such that for every X : AbGroup, the -presheaf of types given by sending U to the homset X -> F U is a sheaf. -https://stacks.math.columbia.edu/tag/00VR --/ - From 0569965d3f4cd6432b0e24ba615434edc0c45435 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 19 Dec 2020 16:42:50 +0000 Subject: [PATCH 03/21] compiles with big sorry --- src/category_theory/sites/sheaf.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 12febfe9942e0..390c9390033b5 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -98,7 +98,6 @@ begin sorry end +end presheaf - - -variables {X Y : C} {S : sieve X} {R : presieve X} +end category_theory From a5f49a3c2e052a1bfacb54070892542e6d7cf46e Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 19 Dec 2020 16:46:45 +0000 Subject: [PATCH 04/21] tidy proof --- src/category_theory/sites/sheaf.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 390c9390033b5..cf15be82fa164 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -80,15 +80,12 @@ lemma w : fork_map R P ≫ first_map R P = fork_map R P ≫ second_map R P := begin apply limit.hom_ext, rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩, - simp only [first_map, second_map, fork_map], - simp only [limit.lift_π, limit.lift_π_assoc, assoc, fan.mk_π_app, subtype.coe_mk, - subtype.val_eq_coe], + simp only [first_map, second_map, fork_map, limit.lift_π, limit.lift_π_assoc, assoc, + fan.mk_π_app, subtype.coe_mk, subtype.val_eq_coe], rw [← P.map_comp, ← op_comp, pullback.condition], simp, end --- definition 3 in Bhaviks list - def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), nonempty (is_limit (fork.of_ι _ (w R P))) From d9c96c747a1c27ef9a82e20eb8357f40653d9847 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 20 Dec 2020 21:04:48 +0000 Subject: [PATCH 05/21] switching computer WIP --- src/category_theory/sites/sheaf.lean | 80 +++++++++++++++++-- src/category_theory/sites/sheaf_of_types.lean | 6 +- 2 files changed, 78 insertions(+), 8 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index cf15be82fa164..d81ac3a1df70e 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -22,18 +22,86 @@ variables (J : grothendieck_topology C) -- We follow https://stacks.math.columbia.edu/tag/00VL definition 00VR /- -A sheaf of abelian groups is a presheaf F : C^op => AbGroup such that for every X : AbGroup, the -presheaf of types given by sending U to the homset X -> F U is a sheaf. +A sheaf of A is a presheaf P : C^op => A such that for every X : A, the +presheaf of types given by sending U : C to Hom_{A}(X, P U) is a sheaf of types. + https://stacks.math.columbia.edu/tag/00VR -/ - - def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := ∀ X : A, presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) + +/-! + +## practice + +-/ + +#check coyoneda.obj (op punit.{v+1}) + +lemma practice (P : Cᵒᵖ ⥤ Type v) : P ≅ (P ⋙ coyoneda.obj (op punit.{v+1})) := +{ hom := { app := λ X a _, a }, + inv := { app := λ X f, f punit.star},-- Hom (*, P X) → P X}, + hom_inv_id' := by tidy, + inv_hom_id' := by tidy } + +example (P Q : Cᵒᵖ ⥤ Type v) (h : P ≅ Q) : presieve.is_sheaf J P → presieve.is_sheaf J Q := +begin + exact presieve.is_sheaf_iso J h, +end + end presheaf +variables {C : Type u} [category.{v} C] +variables (J : grothendieck_topology C) +variables (A : Type u') [category.{v} A] + +/-- The category of sheaves on a grothendieck topology. -/ +@[derive category] +def Sheaf : Type* := +{P : Cᵒᵖ ⥤ A // presheaf.is_sheaf J P} + +-- instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := +-- ⟨⟨(functor.const _).obj punit, +-- λ X S hS, +-- begin +-- simp only [grothendieck_topology.bot_covering] at hS, +-- subst hS, +-- apply presieve.is_sheaf_for_top_sieve, +-- end⟩⟩ + +/-- The inclusion functor from sheaves to presheaves. -/ +@[simps {rhs_md := semireducible}, derive [full, faithful]] +def Sheaf_to_presheaf : Sheaf J A ⥤ (Cᵒᵖ ⥤ A) := +full_subcategory_inclusion (presheaf.is_sheaf J) + +theorem Sheaf_is_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) (hP : presheaf.is_sheaf J P) : + presieve.is_sheaf J P := +begin + specialize hP punit, + apply presieve.is_sheaf_iso J, + apply practice, +end + + +theorem Sheaf_of_types_equiv_Sheaf : Sheaf J (Type v) ≌ SheafOfTypes J := +{ functor := { obj := λ S, ⟨S.1, _⟩, + map := _, + map_id' := _, + map_comp' := _ }, + inverse := _, + unit_iso := _, + counit_iso := _, + --functor_unit_iso_comp' := _ } +} + +end category_theory + +namespace category_theory + +open opposite category_theory category limits sieve classical + namespace presheaf -- under here is the equalizer story, which is equivalent if A has products (and doesn't @@ -92,7 +160,9 @@ nonempty (is_limit (fork.of_ι _ (w R P))) theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : is_sheaf J P ↔ is_sheaf' J P := begin - sorry + split, + { sorry }, + { sorry } end end presheaf diff --git a/src/category_theory/sites/sheaf_of_types.lean b/src/category_theory/sites/sheaf_of_types.lean index 84b69b8d2141f..39f9cac7ce0a4 100644 --- a/src/category_theory/sites/sheaf_of_types.lean +++ b/src/category_theory/sites/sheaf_of_types.lean @@ -885,10 +885,10 @@ variables (J : grothendieck_topology C) /-- The category of sheaves on a grothendieck topology. -/ @[derive category] -def Sheaf (J : grothendieck_topology C) : Type (max u (v+1)) := +def SheafOfTypes (J : grothendieck_topology C) : Type (max u (v+1)) := {P : Cᵒᵖ ⥤ Type v // presieve.is_sheaf J P} -instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := +instance : inhabited (SheafOfTypes (⊥ : grothendieck_topology C)) := ⟨⟨(functor.const _).obj punit, λ X S hS, begin @@ -899,7 +899,7 @@ instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := /-- The inclusion functor from sheaves to presheaves. -/ @[simps {rhs_md := semireducible}, derive [full, faithful]] -def Sheaf_to_presheaf : Sheaf J ⥤ (Cᵒᵖ ⥤ Type v) := +def SheafOfTypes_to_presheaf : SheafOfTypes J ⥤ (Cᵒᵖ ⥤ Type v) := full_subcategory_inclusion (presieve.is_sheaf J) end category_theory From 13fe05cfacf29693951381a9f4ada64006b7048a Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 20 Dec 2020 21:40:29 +0000 Subject: [PATCH 06/21] more stuff --- src/category_theory/sites/sheaf.lean | 20 +++++++++++++++++++ src/category_theory/sites/sheaf_of_types.lean | 5 +++-- 2 files changed, 23 insertions(+), 2 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index d81ac3a1df70e..ae01bc3073169 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -1,6 +1,26 @@ +/- +Copyright (c) 2020 Kevin Buzzard. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Buzzard +-/ + import category_theory.sites.sheaf_of_types import category_theory.concrete_category +/-! +# Sheaves taking values in a category + +If C is a category with a Grothendieck topology, we define the notion of a sheaf +taking values in an arbitrary category `A`. We follow the definition in +https://stacks.math.columbia.edu/tag/00VR , noting that the presheaf of sets "defined above" +can be seen in the comments between tags 00VQ and 00VR on the +page https://stacks.math.columbia.edu/tag/00VL . The advantage of this definition is that +we need no assumptions whatsoever on `A` other than the assumption that the morphisms +in `C` and `A` live in the same universe. + +TODO: Everything. + +-/ -- sheaves taking values in objects of a category universes v v' u' u diff --git a/src/category_theory/sites/sheaf_of_types.lean b/src/category_theory/sites/sheaf_of_types.lean index 39f9cac7ce0a4..af50f5044aaf4 100644 --- a/src/category_theory/sites/sheaf_of_types.lean +++ b/src/category_theory/sites/sheaf_of_types.lean @@ -9,9 +9,10 @@ import category_theory.limits.shapes.types import category_theory.full_subcategory /-! -# Sheaves on a Grothendieck topology +# Sheaves of types on a Grothendieck topology -Defines the notion of a sheaf on a Grothendieck topology, as well as a range of equivalent +Defines the notion of a sheaf of types (usually called a sheaf of sets by mathematicians) +on a category equipped with a Grothendieck topology, as well as a range of equivalent conditions useful in different situations. First define what it means for a presheaf `P : Cᵒᵖ ⥤ Type v` to be a sheaf *for* a particular From 9cfd21cb669957c8e568ced14a25f7fd8937169d Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 20 Dec 2020 21:45:28 +0000 Subject: [PATCH 07/21] finally happy --- src/category_theory/yoneda.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/category_theory/yoneda.lean b/src/category_theory/yoneda.lean index 369c2270d358b..e933f8a5777b3 100644 --- a/src/category_theory/yoneda.lean +++ b/src/category_theory/yoneda.lean @@ -127,6 +127,13 @@ If `coyoneda.map f` is an isomorphism, so was `f`. def is_iso {X Y : Cᵒᵖ} (f : X ⟶ Y) [is_iso (coyoneda.map f)] : is_iso f := is_iso_of_fully_faithful coyoneda f +-- No need to use Cᵒᵖ here, works with any category +/-- A Type-valued presheaf `P` is isomorphic to the composition of `P` with the + coyoneda functor coming from `punit`. -/ +def iso_comp_punit (P : C ⥤ Type v₁) : P ≅ (P ⋙ coyoneda.obj (op punit.{v₁+1})) := +{ hom := { app := λ X a _, a }, + inv := { app := λ X f, f punit.star} } + end coyoneda /-- From 3cfef10dc98d74ad0455961fb2d7d559d8019267 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 20 Dec 2020 22:00:31 +0000 Subject: [PATCH 08/21] merge mathlib --- src/category_theory/sites/sheaf.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index ae01bc3073169..03f2f4493daf9 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -59,6 +59,7 @@ presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) -/ #check coyoneda.obj (op punit.{v+1}) +#check iso_comp_punit lemma practice (P : Cᵒᵖ ⥤ Type v) : P ≅ (P ⋙ coyoneda.obj (op punit.{v+1})) := { hom := { app := λ X a _, a }, From bcb1612c2b73eae8c9f772c7118d9f43f8eaf944 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 15:19:28 +0000 Subject: [PATCH 09/21] start merge --- src/category_theory/yoneda.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/category_theory/yoneda.lean b/src/category_theory/yoneda.lean index e933f8a5777b3..52d80f1b2d8ce 100644 --- a/src/category_theory/yoneda.lean +++ b/src/category_theory/yoneda.lean @@ -130,9 +130,9 @@ is_iso_of_fully_faithful coyoneda f -- No need to use Cᵒᵖ here, works with any category /-- A Type-valued presheaf `P` is isomorphic to the composition of `P` with the coyoneda functor coming from `punit`. -/ -def iso_comp_punit (P : C ⥤ Type v₁) : P ≅ (P ⋙ coyoneda.obj (op punit.{v₁+1})) := -{ hom := { app := λ X a _, a }, - inv := { app := λ X f, f punit.star} } +def iso_comp_punit (P : C ⥤ Type v₁) : (P ⋙ coyoneda.obj (op punit.{v₁+1})) ≅ P := +{ hom := { app := λ X f, f punit.star}, + inv := { app := λ X a _, a } } end coyoneda From 50b3dcadcb5bdd7b1f5ad00ac77edbc27e794914 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 15:25:23 +0000 Subject: [PATCH 10/21] remove --- src/category_theory/sites/sheaf.lean | 191 --------------------------- 1 file changed, 191 deletions(-) delete mode 100644 src/category_theory/sites/sheaf.lean diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean deleted file mode 100644 index 03f2f4493daf9..0000000000000 --- a/src/category_theory/sites/sheaf.lean +++ /dev/null @@ -1,191 +0,0 @@ -/- -Copyright (c) 2020 Kevin Buzzard. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kevin Buzzard --/ - -import category_theory.sites.sheaf_of_types -import category_theory.concrete_category - -/-! -# Sheaves taking values in a category - -If C is a category with a Grothendieck topology, we define the notion of a sheaf -taking values in an arbitrary category `A`. We follow the definition in -https://stacks.math.columbia.edu/tag/00VR , noting that the presheaf of sets "defined above" -can be seen in the comments between tags 00VQ and 00VR on the -page https://stacks.math.columbia.edu/tag/00VL . The advantage of this definition is that -we need no assumptions whatsoever on `A` other than the assumption that the morphisms -in `C` and `A` live in the same universe. - -TODO: Everything. - --/ --- sheaves taking values in objects of a category - -universes v v' u' u - -noncomputable theory - -namespace category_theory - -open opposite category_theory category limits sieve classical - -namespace presheaf - -variables {C : Type u} [category.{v} C] - -variables {A : Type u'} [category.{v} A] - -variables (J : grothendieck_topology C) - --- We follow https://stacks.math.columbia.edu/tag/00VL definition 00VR - -/- -A sheaf of A is a presheaf P : C^op => A such that for every X : A, the -presheaf of types given by sending U : C to Hom_{A}(X, P U) is a sheaf of types. - -https://stacks.math.columbia.edu/tag/00VR --/ - -def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := ∀ X : A, -presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) - - -/-! - -## practice - --/ - -#check coyoneda.obj (op punit.{v+1}) -#check iso_comp_punit - -lemma practice (P : Cᵒᵖ ⥤ Type v) : P ≅ (P ⋙ coyoneda.obj (op punit.{v+1})) := -{ hom := { app := λ X a _, a }, - inv := { app := λ X f, f punit.star},-- Hom (*, P X) → P X}, - hom_inv_id' := by tidy, - inv_hom_id' := by tidy } - -example (P Q : Cᵒᵖ ⥤ Type v) (h : P ≅ Q) : presieve.is_sheaf J P → presieve.is_sheaf J Q := -begin - exact presieve.is_sheaf_iso J h, -end - -end presheaf - -variables {C : Type u} [category.{v} C] -variables (J : grothendieck_topology C) -variables (A : Type u') [category.{v} A] - -/-- The category of sheaves on a grothendieck topology. -/ -@[derive category] -def Sheaf : Type* := -{P : Cᵒᵖ ⥤ A // presheaf.is_sheaf J P} - --- instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := --- ⟨⟨(functor.const _).obj punit, --- λ X S hS, --- begin --- simp only [grothendieck_topology.bot_covering] at hS, --- subst hS, --- apply presieve.is_sheaf_for_top_sieve, --- end⟩⟩ - -/-- The inclusion functor from sheaves to presheaves. -/ -@[simps {rhs_md := semireducible}, derive [full, faithful]] -def Sheaf_to_presheaf : Sheaf J A ⥤ (Cᵒᵖ ⥤ A) := -full_subcategory_inclusion (presheaf.is_sheaf J) - -theorem Sheaf_is_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) (hP : presheaf.is_sheaf J P) : - presieve.is_sheaf J P := -begin - specialize hP punit, - apply presieve.is_sheaf_iso J, - apply practice, -end - - -theorem Sheaf_of_types_equiv_Sheaf : Sheaf J (Type v) ≌ SheafOfTypes J := -{ functor := { obj := λ S, ⟨S.1, _⟩, - map := _, - map_id' := _, - map_comp' := _ }, - inverse := _, - unit_iso := _, - counit_iso := _, - --functor_unit_iso_comp' := _ } -} - -end category_theory - -namespace category_theory - -open opposite category_theory category limits sieve classical - -namespace presheaf - --- under here is the equalizer story, which is equivalent if A has products (and doesn't --- make sense otherwise). It's described between 00VQ and 00VR in stacks. --- we need [category.{u} A] possibly - -variables {C : Type v} [small_category C] [has_pullbacks C] - -variables {A : Type u} [category.{v} A] [has_products A] - -variables (J : grothendieck_topology C) - -variables {U : C} (R : presieve U) - -variables (P : Cᵒᵖ ⥤ A) - -def first_obj : A := -∏ (λ (f : Σ V, {f : V ⟶ U // R f}), P.obj (op f.1)) - -/-- -The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which -contains the data used to check a family of elements for a presieve is compatible. --/ -def second_obj : A := -∏ (λ (fg : (Σ V, {f : V ⟶ U // R f}) × (Σ W, {g : W ⟶ U // R g})), - P.obj (op (pullback fg.1.2.1 fg.2.2.1))) - -/-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VL. -/ -def first_map : first_obj R P ⟶ second_obj R P := -pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) - -/-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VL. -/ -def second_map : first_obj R P ⟶ second_obj R P := -pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) - -/-- -The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram -of https://stacks.math.columbia.edu/tag/00VM. --/ -def fork_map : P.obj (op U) ⟶ first_obj R P := -pi.lift (λ f, P.map f.2.1.op) - -lemma w : fork_map R P ≫ first_map R P = fork_map R P ≫ second_map R P := -begin - apply limit.hom_ext, - rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩, - simp only [first_map, second_map, fork_map, limit.lift_π, limit.lift_π_assoc, assoc, - fan.mk_π_app, subtype.coe_mk, subtype.val_eq_coe], - rw [← P.map_comp, ← op_comp, pullback.condition], - simp, -end - -def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), -nonempty (is_limit (fork.of_ι _ (w R P))) - -theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : -is_sheaf J P ↔ is_sheaf' J P := -begin - split, - { sorry }, - { sorry } -end - -end presheaf - -end category_theory From 8ca69624b5927701a3c289cf91f6485354f41aaa Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 15:26:41 +0000 Subject: [PATCH 11/21] restore --- src/category_theory/sites/sheaf.lean | 191 +++++++++++++++++++++++++++ 1 file changed, 191 insertions(+) create mode 100644 src/category_theory/sites/sheaf.lean diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean new file mode 100644 index 0000000000000..03f2f4493daf9 --- /dev/null +++ b/src/category_theory/sites/sheaf.lean @@ -0,0 +1,191 @@ +/- +Copyright (c) 2020 Kevin Buzzard. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kevin Buzzard +-/ + +import category_theory.sites.sheaf_of_types +import category_theory.concrete_category + +/-! +# Sheaves taking values in a category + +If C is a category with a Grothendieck topology, we define the notion of a sheaf +taking values in an arbitrary category `A`. We follow the definition in +https://stacks.math.columbia.edu/tag/00VR , noting that the presheaf of sets "defined above" +can be seen in the comments between tags 00VQ and 00VR on the +page https://stacks.math.columbia.edu/tag/00VL . The advantage of this definition is that +we need no assumptions whatsoever on `A` other than the assumption that the morphisms +in `C` and `A` live in the same universe. + +TODO: Everything. + +-/ +-- sheaves taking values in objects of a category + +universes v v' u' u + +noncomputable theory + +namespace category_theory + +open opposite category_theory category limits sieve classical + +namespace presheaf + +variables {C : Type u} [category.{v} C] + +variables {A : Type u'} [category.{v} A] + +variables (J : grothendieck_topology C) + +-- We follow https://stacks.math.columbia.edu/tag/00VL definition 00VR + +/- +A sheaf of A is a presheaf P : C^op => A such that for every X : A, the +presheaf of types given by sending U : C to Hom_{A}(X, P U) is a sheaf of types. + +https://stacks.math.columbia.edu/tag/00VR +-/ + +def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := ∀ X : A, +presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) + + +/-! + +## practice + +-/ + +#check coyoneda.obj (op punit.{v+1}) +#check iso_comp_punit + +lemma practice (P : Cᵒᵖ ⥤ Type v) : P ≅ (P ⋙ coyoneda.obj (op punit.{v+1})) := +{ hom := { app := λ X a _, a }, + inv := { app := λ X f, f punit.star},-- Hom (*, P X) → P X}, + hom_inv_id' := by tidy, + inv_hom_id' := by tidy } + +example (P Q : Cᵒᵖ ⥤ Type v) (h : P ≅ Q) : presieve.is_sheaf J P → presieve.is_sheaf J Q := +begin + exact presieve.is_sheaf_iso J h, +end + +end presheaf + +variables {C : Type u} [category.{v} C] +variables (J : grothendieck_topology C) +variables (A : Type u') [category.{v} A] + +/-- The category of sheaves on a grothendieck topology. -/ +@[derive category] +def Sheaf : Type* := +{P : Cᵒᵖ ⥤ A // presheaf.is_sheaf J P} + +-- instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := +-- ⟨⟨(functor.const _).obj punit, +-- λ X S hS, +-- begin +-- simp only [grothendieck_topology.bot_covering] at hS, +-- subst hS, +-- apply presieve.is_sheaf_for_top_sieve, +-- end⟩⟩ + +/-- The inclusion functor from sheaves to presheaves. -/ +@[simps {rhs_md := semireducible}, derive [full, faithful]] +def Sheaf_to_presheaf : Sheaf J A ⥤ (Cᵒᵖ ⥤ A) := +full_subcategory_inclusion (presheaf.is_sheaf J) + +theorem Sheaf_is_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) (hP : presheaf.is_sheaf J P) : + presieve.is_sheaf J P := +begin + specialize hP punit, + apply presieve.is_sheaf_iso J, + apply practice, +end + + +theorem Sheaf_of_types_equiv_Sheaf : Sheaf J (Type v) ≌ SheafOfTypes J := +{ functor := { obj := λ S, ⟨S.1, _⟩, + map := _, + map_id' := _, + map_comp' := _ }, + inverse := _, + unit_iso := _, + counit_iso := _, + --functor_unit_iso_comp' := _ } +} + +end category_theory + +namespace category_theory + +open opposite category_theory category limits sieve classical + +namespace presheaf + +-- under here is the equalizer story, which is equivalent if A has products (and doesn't +-- make sense otherwise). It's described between 00VQ and 00VR in stacks. +-- we need [category.{u} A] possibly + +variables {C : Type v} [small_category C] [has_pullbacks C] + +variables {A : Type u} [category.{v} A] [has_products A] + +variables (J : grothendieck_topology C) + +variables {U : C} (R : presieve U) + +variables (P : Cᵒᵖ ⥤ A) + +def first_obj : A := +∏ (λ (f : Σ V, {f : V ⟶ U // R f}), P.obj (op f.1)) + +/-- +The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which +contains the data used to check a family of elements for a presieve is compatible. +-/ +def second_obj : A := +∏ (λ (fg : (Σ V, {f : V ⟶ U // R f}) × (Σ W, {g : W ⟶ U // R g})), + P.obj (op (pullback fg.1.2.1 fg.2.2.1))) + +/-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VL. -/ +def first_map : first_obj R P ⟶ second_obj R P := +pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) + +/-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VL. -/ +def second_map : first_obj R P ⟶ second_obj R P := +pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) + +/-- +The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram +of https://stacks.math.columbia.edu/tag/00VM. +-/ +def fork_map : P.obj (op U) ⟶ first_obj R P := +pi.lift (λ f, P.map f.2.1.op) + +lemma w : fork_map R P ≫ first_map R P = fork_map R P ≫ second_map R P := +begin + apply limit.hom_ext, + rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩, + simp only [first_map, second_map, fork_map, limit.lift_π, limit.lift_π_assoc, assoc, + fan.mk_π_app, subtype.coe_mk, subtype.val_eq_coe], + rw [← P.map_comp, ← op_comp, pullback.condition], + simp, +end + +def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), +nonempty (is_limit (fork.of_ι _ (w R P))) + +theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : +is_sheaf J P ↔ is_sheaf' J P := +begin + split, + { sorry }, + { sorry } +end + +end presheaf + +end category_theory From 5073fb3d03e779704b819c75223e64c2b90546b6 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 16:19:40 +0000 Subject: [PATCH 12/21] sheaf of types equiv sheaf --- src/category_theory/sites/sheaf.lean | 64 ++++++++++++++-------------- 1 file changed, 33 insertions(+), 31 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 03f2f4493daf9..5d4255d419d79 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -47,10 +47,8 @@ presheaf of types given by sending U : C to Hom_{A}(X, P U) is a sheaf of types. https://stacks.math.columbia.edu/tag/00VR -/ - -def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := ∀ X : A, -presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) - +def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := +∀ X : A, presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) /-! @@ -58,27 +56,13 @@ presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) -/ -#check coyoneda.obj (op punit.{v+1}) -#check iso_comp_punit - -lemma practice (P : Cᵒᵖ ⥤ Type v) : P ≅ (P ⋙ coyoneda.obj (op punit.{v+1})) := -{ hom := { app := λ X a _, a }, - inv := { app := λ X f, f punit.star},-- Hom (*, P X) → P X}, - hom_inv_id' := by tidy, - inv_hom_id' := by tidy } - -example (P Q : Cᵒᵖ ⥤ Type v) (h : P ≅ Q) : presieve.is_sheaf J P → presieve.is_sheaf J Q := -begin - exact presieve.is_sheaf_iso J h, -end - end presheaf variables {C : Type u} [category.{v} C] variables (J : grothendieck_topology C) variables (A : Type u') [category.{v} A] -/-- The category of sheaves on a grothendieck topology. -/ +/-- The category of sheaves taking values in `A` on a grothendieck topology. -/ @[derive category] def Sheaf : Type* := {P : Cᵒᵖ ⥤ A // presheaf.is_sheaf J P} @@ -101,21 +85,39 @@ theorem Sheaf_is_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) (hP : presheaf.is_sheaf J presieve.is_sheaf J P := begin specialize hP punit, - apply presieve.is_sheaf_iso J, - apply practice, + apply presieve.is_sheaf_iso J _ hP, + apply coyoneda.iso_comp_punit, end +theorem SheafOfTypes_is_Sheaf (P : Cᵒᵖ ⥤ Type v) (hP : presieve.is_sheaf J P) : + presheaf.is_sheaf J P := +begin + intros X Y S hS z hz, + change ∃! (t : X ⟶ _), _, + refine ⟨λ x, (hP S hS).amalgamate (λ Z f hf, z f hf x) _, _, _⟩, + { intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h, + exact congr_fun (hz g₁ g₂ hf₁ hf₂ h) x }, + { intros Z f hf, + ext x, + apply presieve.is_sheaf_for.valid_glue }, + { intros y hy, + ext x, + apply (hP S hS).is_separated_for.ext, + intros Y' f hf, + rw presieve.is_sheaf_for.valid_glue _ _ _ hf, + rw ← hy _ hf, + refl } +end -theorem Sheaf_of_types_equiv_Sheaf : Sheaf J (Type v) ≌ SheafOfTypes J := -{ functor := { obj := λ S, ⟨S.1, _⟩, - map := _, - map_id' := _, - map_comp' := _ }, - inverse := _, - unit_iso := _, - counit_iso := _, - --functor_unit_iso_comp' := _ } -} +def Sheaf_of_types_equiv_Sheaf : Sheaf J (Type v) ≌ SheafOfTypes J := +{ functor := + { obj := λ S, ⟨S.1, Sheaf_is_SheafOfTypes _ _ S.2⟩, + map := λ S₁ S₂ f, f }, + inverse := + { obj := λ S, ⟨S.1, SheafOfTypes_is_Sheaf _ _ S.2⟩, + map := λ S₁ S₂ f, f }, + unit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy), + counit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy) } end category_theory From 9aca3e57a250f1e6deaaef941cd853913c2758f5 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 17:49:38 +0000 Subject: [PATCH 13/21] no more sorries --- src/category_theory/sites/sheaf.lean | 66 ++++++++++++++++++++++----- src/category_theory/sites/sieves.lean | 3 ++ 2 files changed, 58 insertions(+), 11 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 5d4255d419d79..9da51e61eddf9 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -1,10 +1,13 @@ /- -Copyright (c) 2020 Kevin Buzzard. All rights reserved. +Copyright (c) 2020 Kevin Buzzard, Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kevin Buzzard +Authors: Kevin Buzzard, Bhavik Mehta -/ import category_theory.sites.sheaf_of_types +import category_theory.limits.yoneda +import category_theory.limits.preserves.shapes.equalizers +import category_theory.limits.preserves.shapes.products import category_theory.concrete_category /-! @@ -50,12 +53,6 @@ https://stacks.math.columbia.edu/tag/00VR def is_sheaf (P : Cᵒᵖ ⥤ A) : Prop := ∀ X : A, presieve.is_sheaf J (P ⋙ coyoneda.obj (op X)) -/-! - -## practice - --/ - end presheaf variables {C : Type u} [category.{v} C] @@ -131,7 +128,7 @@ namespace presheaf -- make sense otherwise). It's described between 00VQ and 00VR in stacks. -- we need [category.{u} A] possibly -variables {C : Type v} [small_category C] [has_pullbacks C] +variables {C : Type v} [small_category C] variables {A : Type u} [category.{v} A] [has_products A] @@ -144,6 +141,8 @@ variables (P : Cᵒᵖ ⥤ A) def first_obj : A := ∏ (λ (f : Σ V, {f : V ⟶ U // R f}), P.obj (op f.1)) +variables [has_pullbacks C] + /-- The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which contains the data used to check a family of elements for a presieve is compatible. @@ -180,12 +179,57 @@ end def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), nonempty (is_limit (fork.of_ι _ (w R P))) +def is_sheaf_for_is_sheaf_for' (P : Cᵒᵖ ⥤ A) (X) (U : C) (R : presieve U) : + is_limit ((coyoneda.obj X).map_cone (fork.of_ι _ (w R P))) ≃ + is_limit (fork.of_ι _ (equalizer.presieve.w (P ⋙ coyoneda.obj X) R)) := +begin + apply equiv.trans (is_limit_map_cone_fork_equiv _ _) _, + apply (is_limit.postcompose_hom_equiv _ _).symm.trans (is_limit.equiv_iso_limit _), + { apply nat_iso.of_components _ _, + { rintro (_ | _), + { apply preserves_product.iso (coyoneda.obj X) }, + { apply preserves_product.iso (coyoneda.obj X) } }, + { rintro _ _ (_ | _), + { ext : 1, + dsimp [equalizer.presieve.first_map, first_map], + simp only [limit.lift_π, map_lift_pi_comparison, assoc, fan.mk_π_app, functor.map_comp], + erw limit.lift_π, + erw pi_comparison_comp_π_assoc, + simp }, + { ext : 1, + dsimp [equalizer.presieve.second_map, second_map], + simp only [limit.lift_π, map_lift_pi_comparison, assoc, fan.mk_π_app, functor.map_comp], + erw limit.lift_π, + erw pi_comparison_comp_π_assoc, + simp }, + { dsimp, + simp } } }, + { refine fork.ext (iso.refl _) _, + dsimp [equalizer.fork_map, fork_map], + simp } + +end + theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : is_sheaf J P ↔ is_sheaf' J P := begin split, - { sorry }, - { sorry } + { intros h U R hR, + refine ⟨_⟩, + apply coyoneda_jointly_reflects_limits, + intro X, + have q : presieve.is_sheaf_for (P ⋙ coyoneda.obj X) _ := h X.unop _ hR, + rw ←presieve.is_sheaf_for_iff_generate at q, + rw equalizer.presieve.sheaf_condition at q, + replace q := classical.choice q, + apply (is_sheaf_for_is_sheaf_for' _ _ _ _).symm q }, + { intros h U X S hS, + rw equalizer.presieve.sheaf_condition, + refine ⟨_⟩, + refine is_sheaf_for_is_sheaf_for' _ _ _ _ _, + apply is_limit_of_preserves, + apply classical.choice (h _ S _), + simpa } end end presheaf diff --git a/src/category_theory/sites/sieves.lean b/src/category_theory/sites/sieves.lean index 2043ff7498b63..26e24356350de 100644 --- a/src/category_theory/sites/sieves.lean +++ b/src/category_theory/sites/sieves.lean @@ -225,6 +225,9 @@ def gi_generate : galois_insertion (generate : presieve X → sieve X) arrows := lemma le_generate (R : presieve X) : R ≤ generate R := gi_generate.gc.le_u_l R +@[simp] lemma generate_sieve (S : sieve X) : generate S = S := +gi_generate.l_u_eq S + /-- If the identity arrow is in a sieve, the sieve is maximal. -/ lemma id_mem_iff_eq_top : S (𝟙 X) ↔ S = ⊤ := ⟨λ h, top_unique $ λ Y f _, by simpa using downward_closed _ h f, From 05e8a9e97eabff1f0cf87b9ce84cf2a7e0f5c829 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 18:01:15 +0000 Subject: [PATCH 14/21] lint --- src/category_theory/sites/sheaf.lean | 39 +++++++++++----------------- 1 file changed, 15 insertions(+), 24 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 9da51e61eddf9..aaf466da7c26f 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -13,18 +13,13 @@ import category_theory.concrete_category /-! # Sheaves taking values in a category -If C is a category with a Grothendieck topology, we define the notion of a sheaf -taking values in an arbitrary category `A`. We follow the definition in -https://stacks.math.columbia.edu/tag/00VR , noting that the presheaf of sets "defined above" -can be seen in the comments between tags 00VQ and 00VR on the -page https://stacks.math.columbia.edu/tag/00VL . The advantage of this definition is that -we need no assumptions whatsoever on `A` other than the assumption that the morphisms -in `C` and `A` live in the same universe. - -TODO: Everything. - +If C is a category with a Grothendieck topology, we define the notion of a sheaf taking values in +an arbitrary category `A`. We follow the definition in https://stacks.math.columbia.edu/tag/00VR, +noting that the presheaf of sets "defined above" can be seen in the comments between tags 00VQ and +00VR on the page https://stacks.math.columbia.edu/tag/00VL. The advantage of this definition is +that we need no assumptions whatsoever on `A` other than the assumption that the morphisms in `C` +and `A` live in the same universe. -/ --- sheaves taking values in objects of a category universes v v' u' u @@ -37,14 +32,12 @@ open opposite category_theory category limits sieve classical namespace presheaf variables {C : Type u} [category.{v} C] - variables {A : Type u'} [category.{v} A] - variables (J : grothendieck_topology C) -- We follow https://stacks.math.columbia.edu/tag/00VL definition 00VR -/- +/-- A sheaf of A is a presheaf P : C^op => A such that for every X : A, the presheaf of types given by sending U : C to Hom_{A}(X, P U) is a sheaf of types. @@ -64,15 +57,6 @@ variables (A : Type u') [category.{v} A] def Sheaf : Type* := {P : Cᵒᵖ ⥤ A // presheaf.is_sheaf J P} --- instance : inhabited (Sheaf (⊥ : grothendieck_topology C)) := --- ⟨⟨(functor.const _).obj punit, --- λ X S hS, --- begin --- simp only [grothendieck_topology.bot_covering] at hS, --- subst hS, --- apply presieve.is_sheaf_for_top_sieve, --- end⟩⟩ - /-- The inclusion functor from sheaves to presheaves. -/ @[simps {rhs_md := semireducible}, derive [full, faithful]] def Sheaf_to_presheaf : Sheaf J A ⥤ (Cᵒᵖ ⥤ A) := @@ -106,7 +90,11 @@ begin refl } end -def Sheaf_of_types_equiv_Sheaf : Sheaf J (Type v) ≌ SheafOfTypes J := +/-- +The category of sheaves taking values in Type is the same as the category of set-valued sheaves. +-/ +@[simps] +def Sheaf_equiv_SheafOfTypes : Sheaf J (Type v) ≌ SheafOfTypes J := { functor := { obj := λ S, ⟨S.1, Sheaf_is_SheafOfTypes _ _ S.2⟩, map := λ S₁ S₂ f, f }, @@ -116,6 +104,9 @@ def Sheaf_of_types_equiv_Sheaf : Sheaf J (Type v) ≌ SheafOfTypes J := unit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy), counit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy) } +instance : inhabited (Sheaf (⊥ : grothendieck_topology C) (Type v)) := +⟨(SheafOfTypes_equiv_Sheaf _).inverse.obj (default _)⟩ + end category_theory namespace category_theory From c8c85bbddef026704a2c1770d42a413b0b66217f Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 18:02:03 +0000 Subject: [PATCH 15/21] fix --- src/category_theory/sites/sheaf.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index aaf466da7c26f..8050997c1b751 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -105,7 +105,7 @@ def Sheaf_equiv_SheafOfTypes : Sheaf J (Type v) ≌ SheafOfTypes J := counit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy) } instance : inhabited (Sheaf (⊥ : grothendieck_topology C) (Type v)) := -⟨(SheafOfTypes_equiv_Sheaf _).inverse.obj (default _)⟩ +⟨(Sheaf_equiv_SheafOfTypes _).inverse.obj (default _)⟩ end category_theory From 28a46153ff8a1c39e61b8b1dbe183749def708e1 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 18:13:22 +0000 Subject: [PATCH 16/21] tab --- src/category_theory/sites/sheaf.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 8050997c1b751..007eb915250a4 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -202,7 +202,7 @@ begin end theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : -is_sheaf J P ↔ is_sheaf' J P := + is_sheaf J P ↔ is_sheaf' J P := begin split, { intros h U R hR, From 2b58c0469aa8cd495b66420b623dbb366711cdfb Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 23:34:15 +0000 Subject: [PATCH 17/21] more things --- src/category_theory/sites/sheaf.lean | 100 +++++++++++++++------------ 1 file changed, 56 insertions(+), 44 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 007eb915250a4..305b4304b82b3 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -62,32 +62,25 @@ def Sheaf : Type* := def Sheaf_to_presheaf : Sheaf J A ⥤ (Cᵒᵖ ⥤ A) := full_subcategory_inclusion (presheaf.is_sheaf J) -theorem Sheaf_is_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) (hP : presheaf.is_sheaf J P) : - presieve.is_sheaf J P := +lemma Sheaf_iff_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) : + presheaf.is_sheaf J P ↔ presieve.is_sheaf J P := begin - specialize hP punit, - apply presieve.is_sheaf_iso J _ hP, - apply coyoneda.iso_comp_punit, -end - -theorem SheafOfTypes_is_Sheaf (P : Cᵒᵖ ⥤ Type v) (hP : presieve.is_sheaf J P) : - presheaf.is_sheaf J P := -begin - intros X Y S hS z hz, - change ∃! (t : X ⟶ _), _, - refine ⟨λ x, (hP S hS).amalgamate (λ Z f hf, z f hf x) _, _, _⟩, - { intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h, - exact congr_fun (hz g₁ g₂ hf₁ hf₂ h) x }, - { intros Z f hf, - ext x, - apply presieve.is_sheaf_for.valid_glue }, - { intros y hy, - ext x, - apply (hP S hS).is_separated_for.ext, - intros Y' f hf, - rw presieve.is_sheaf_for.valid_glue _ _ _ hf, - rw ← hy _ hf, - refl } + split, + { intros hP, + apply presieve.is_sheaf_iso J (coyoneda.iso_comp_punit _) (hP punit) }, + { intros hP X Y S hS z hz, + refine ⟨λ x, (hP S hS).amalgamate (λ Z f hf, z f hf x) _, _, _⟩, + { intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h, + exact congr_fun (hz g₁ g₂ hf₁ hf₂ h) x }, + { intros Z f hf, + ext x, + apply presieve.is_sheaf_for.valid_glue }, + { intros y hy, + ext x, + apply (hP S hS).is_separated_for.ext, + intros Y' f hf, + rw [presieve.is_sheaf_for.valid_glue _ _ _ hf, ← hy _ hf], + refl } } end /-- @@ -96,10 +89,10 @@ The category of sheaves taking values in Type is the same as the category of set @[simps] def Sheaf_equiv_SheafOfTypes : Sheaf J (Type v) ≌ SheafOfTypes J := { functor := - { obj := λ S, ⟨S.1, Sheaf_is_SheafOfTypes _ _ S.2⟩, + { obj := λ S, ⟨S.1, (Sheaf_iff_SheafOfTypes _ _).1 S.2⟩, map := λ S₁ S₂ f, f }, inverse := - { obj := λ S, ⟨S.1, SheafOfTypes_is_Sheaf _ _ S.2⟩, + { obj := λ S, ⟨S.1, (Sheaf_iff_SheafOfTypes _ _).2 S.2⟩, map := λ S₁ S₂ f, f }, unit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy), counit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy) } @@ -117,16 +110,11 @@ namespace presheaf -- under here is the equalizer story, which is equivalent if A has products (and doesn't -- make sense otherwise). It's described between 00VQ and 00VR in stacks. --- we need [category.{u} A] possibly variables {C : Type v} [small_category C] - variables {A : Type u} [category.{v} A] [has_products A] - variables (J : grothendieck_topology C) - variables {U : C} (R : presieve U) - variables (P : Cᵒᵖ ⥤ A) def first_obj : A := @@ -170,37 +158,35 @@ end def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), nonempty (is_limit (fork.of_ι _ (w R P))) -def is_sheaf_for_is_sheaf_for' (P : Cᵒᵖ ⥤ A) (X) (U : C) (R : presieve U) : - is_limit ((coyoneda.obj X).map_cone (fork.of_ι _ (w R P))) ≃ - is_limit (fork.of_ι _ (equalizer.presieve.w (P ⋙ coyoneda.obj X) R)) := +/-- Impl. An auxiliary lemma to convert between sheaf conditions. -/ +def is_sheaf_for_is_sheaf_for' (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type v) + [Π J, preserves_limits_of_shape (discrete J) s] (U : C) (R : presieve U) : + is_limit (s.map_cone (fork.of_ι _ (w R P))) ≃ + is_limit (fork.of_ι _ (equalizer.presieve.w (P ⋙ s) R)) := begin apply equiv.trans (is_limit_map_cone_fork_equiv _ _) _, apply (is_limit.postcompose_hom_equiv _ _).symm.trans (is_limit.equiv_iso_limit _), { apply nat_iso.of_components _ _, { rintro (_ | _), - { apply preserves_product.iso (coyoneda.obj X) }, - { apply preserves_product.iso (coyoneda.obj X) } }, + { apply preserves_product.iso s }, + { apply preserves_product.iso s } }, { rintro _ _ (_ | _), { ext : 1, dsimp [equalizer.presieve.first_map, first_map], simp only [limit.lift_π, map_lift_pi_comparison, assoc, fan.mk_π_app, functor.map_comp], - erw limit.lift_π, - erw pi_comparison_comp_π_assoc, - simp }, + erw pi_comparison_comp_π_assoc }, { ext : 1, dsimp [equalizer.presieve.second_map, second_map], simp only [limit.lift_π, map_lift_pi_comparison, assoc, fan.mk_π_app, functor.map_comp], - erw limit.lift_π, - erw pi_comparison_comp_π_assoc, - simp }, + erw pi_comparison_comp_π_assoc }, { dsimp, simp } } }, { refine fork.ext (iso.refl _) _, dsimp [equalizer.fork_map, fork_map], simp } - end +/-- The equalizer definition of a sheaf given by `is_sheaf'` is equivalent to `is_sheaf`. -/ theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : is_sheaf J P ↔ is_sheaf' J P := begin @@ -223,6 +209,32 @@ begin simpa } end +/-- +For a concrete category `(A, s)` where the forgetful functor `s : A ⥤ Type v` preserves limits and +reflects isomorphisms, and `A` has limits, an `A`-valued presheaf `P : Cᵒᵖ ⥤ A` is a sheaf iff its +underlying `Type`-valued presheaf `P ⋙ s : Cᵒᵖ ⥤ Type` is a sheaf. +-/ +lemma sheaf_cond3 (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type v) + [has_limits A] [preserves_limits s] [faithful s] [reflects_isomorphisms s] : + is_sheaf J P ↔ is_sheaf J (P ⋙ s) := +begin + rw is_sheaf_iff_is_sheaf', + rw is_sheaf_iff_is_sheaf', + apply forall_congr (λ U, _), + apply ball_congr (λ R hR, _), + letI : reflects_limits s := reflects_limits_of_reflects_isomorphisms, + have : is_limit (s.map_cone (fork.of_ι _ (w R P))) ≃ is_limit (fork.of_ι _ (w R (P ⋙ s))) := + is_sheaf_for_is_sheaf_for' P s U R, + rw ← equiv.nonempty_iff_nonempty this, + split, + { apply nonempty.map, + intro t, + apply is_limit_of_preserves s t }, + { apply nonempty.map _, + intro t, + apply is_limit_of_reflects s t } +end + end presheaf end category_theory From e2a6e3f6e92e37000cbb5976f6845e64353fdb7d Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 27 Jan 2021 23:51:56 +0000 Subject: [PATCH 18/21] doc --- src/category_theory/sites/sheaf.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 305b4304b82b3..d00b29874f15b 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -213,6 +213,10 @@ end For a concrete category `(A, s)` where the forgetful functor `s : A ⥤ Type v` preserves limits and reflects isomorphisms, and `A` has limits, an `A`-valued presheaf `P : Cᵒᵖ ⥤ A` is a sheaf iff its underlying `Type`-valued presheaf `P ⋙ s : Cᵒᵖ ⥤ Type` is a sheaf. + +Note this lemma applies for "algebraic" categories, eg groups, abelian groups and rings, but not +for the category of topological spaces, topological rings, etc since reflecting isomorphisms doesn't +hold. -/ lemma sheaf_cond3 (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type v) [has_limits A] [preserves_limits s] [faithful s] [reflects_isomorphisms s] : From 6ac14dd9673aaca8cd3be76a0ae9a084b319f7ca Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 20 Apr 2021 17:02:56 +0100 Subject: [PATCH 19/21] Kevin suggestions --- src/category_theory/sites/sheaf.lean | 44 ++++++++++++++++------------ 1 file changed, 26 insertions(+), 18 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index d00b29874f15b..21cad23184c16 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -67,7 +67,7 @@ lemma Sheaf_iff_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) : begin split, { intros hP, - apply presieve.is_sheaf_iso J (coyoneda.iso_comp_punit _) (hP punit) }, + exact presieve.is_sheaf_iso J (coyoneda.iso_comp_punit _) (hP punit) }, { intros hP X Y S hS z hz, refine ⟨λ x, (hP S hS).amalgamate (λ Z f hf, z f hf x) _, _, _⟩, { intros Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ h, @@ -108,15 +108,20 @@ open opposite category_theory category limits sieve classical namespace presheaf --- under here is the equalizer story, which is equivalent if A has products (and doesn't --- make sense otherwise). It's described between 00VQ and 00VR in stacks. +-- Under here is the equalizer story, which is equivalent if A has products (and doesn't +-- make sense otherwise). It's described in https://stacks.math.columbia.edu/tag/00VL, +-- between 00VQ and 00VR. variables {C : Type v} [small_category C] -variables {A : Type u} [category.{v} A] [has_products A] +variables {A : Type u} [category.{v} A] variables (J : grothendieck_topology C) variables {U : C} (R : presieve U) variables (P : Cᵒᵖ ⥤ A) +section + +variables [has_products A] + def first_obj : A := ∏ (λ (f : Σ V, {f : V ⟶ U // R f}), P.obj (op f.1)) @@ -130,11 +135,11 @@ def second_obj : A := ∏ (λ (fg : (Σ V, {f : V ⟶ U // R f}) × (Σ W, {g : W ⟶ U // R g})), P.obj (op (pullback fg.1.2.1 fg.2.2.1))) -/-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VL. -/ +/-- The map `pr₀*` of https://stacks.math.columbia.edu/tag/00VM. -/ def first_map : first_obj R P ⟶ second_obj R P := pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) -/-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VL. -/ +/-- The map `pr₁*` of https://stacks.math.columbia.edu/tag/00VM. -/ def second_map : first_obj R P ⟶ second_obj R P := pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) @@ -158,7 +163,7 @@ end def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), nonempty (is_limit (fork.of_ι _ (w R P))) -/-- Impl. An auxiliary lemma to convert between sheaf conditions. -/ +/-- (Implementation). An auxiliary lemma to convert between sheaf conditions. -/ def is_sheaf_for_is_sheaf_for' (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type v) [Π J, preserves_limits_of_shape (discrete J) s] (U : C) (R : presieve U) : is_limit (s.map_cone (fork.of_ι _ (w R P))) ≃ @@ -187,7 +192,7 @@ begin end /-- The equalizer definition of a sheaf given by `is_sheaf'` is equivalent to `is_sheaf`. -/ -theorem is_sheaf_iff_is_sheaf' (P : Cᵒᵖ ⥤ A) : +theorem is_sheaf_iff_is_sheaf' : is_sheaf J P ↔ is_sheaf' J P := begin split, @@ -209,6 +214,12 @@ begin simpa } end +end + +section concrete + +variables [has_pullbacks C] + /-- For a concrete category `(A, s)` where the forgetful functor `s : A ⥤ Type v` preserves limits and reflects isomorphisms, and `A` has limits, an `A`-valued presheaf `P : Cᵒᵖ ⥤ A` is a sheaf iff its @@ -218,27 +229,24 @@ Note this lemma applies for "algebraic" categories, eg groups, abelian groups an for the category of topological spaces, topological rings, etc since reflecting isomorphisms doesn't hold. -/ -lemma sheaf_cond3 (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type v) +lemma is_sheaf_iff_is_sheaf_forget (s : A ⥤ Type v) [has_limits A] [preserves_limits s] [faithful s] [reflects_isomorphisms s] : is_sheaf J P ↔ is_sheaf J (P ⋙ s) := begin - rw is_sheaf_iff_is_sheaf', - rw is_sheaf_iff_is_sheaf', + rw [is_sheaf_iff_is_sheaf', is_sheaf_iff_is_sheaf'], apply forall_congr (λ U, _), apply ball_congr (λ R hR, _), letI : reflects_limits s := reflects_limits_of_reflects_isomorphisms, have : is_limit (s.map_cone (fork.of_ι _ (w R P))) ≃ is_limit (fork.of_ι _ (w R (P ⋙ s))) := is_sheaf_for_is_sheaf_for' P s U R, - rw ← equiv.nonempty_iff_nonempty this, + rw ←equiv.nonempty_iff_nonempty this, split, - { apply nonempty.map, - intro t, - apply is_limit_of_preserves s t }, - { apply nonempty.map _, - intro t, - apply is_limit_of_reflects s t } + { exact nonempty.map (λ t, is_limit_of_preserves s t) }, + { exact nonempty.map (λ t, is_limit_of_reflects s t) } end +end concrete + end presheaf end category_theory From dfad260ea3779b84594525ac8eeff616bc2ef700 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 20 Apr 2021 17:12:02 +0100 Subject: [PATCH 20/21] improve module doc --- src/category_theory/sites/sheaf.lean | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 21cad23184c16..3de7e5c3f5482 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -19,6 +19,23 @@ noting that the presheaf of sets "defined above" can be seen in the comments bet 00VR on the page https://stacks.math.columbia.edu/tag/00VL. The advantage of this definition is that we need no assumptions whatsoever on `A` other than the assumption that the morphisms in `C` and `A` live in the same universe. + +* An `A`-valued presheaf `P : Cᵒᵖ ⥤ A` is defined to be a sheaf (for the topology `J`) iff for + every `X : A`, the type-valued presheaves of sets given by sending `U : Cᵒᵖ` to `Hom_{A}(X, P U)` + are all sheaves of sets, see `category_theory.presheaf.is_sheaf`. +* When `A = Type`, this recovers the basic definition of sheaves of sets, see + `category_theory.is_sheaf_iff_is_sheaf_of_type`. +* An alternate definition when `C` is small, has pullbacks and `A` has products is given by an + equalizer condition `category_theory.presheaf.is_sheaf'`. This is equivalent to the earlier + definition, shown in `category_theory.presheaf.is_sheaf_iff_is_sheaf'`. +* When `A = Type`, this is *definitionally* equal to the equalizer condition for presieves in + `category_theory.sites.sheaf_of_types`. +* When `A` has limits and there is a functor `s : A ⥤ Type` which is faithful, reflects isomorphisms + and preserves limits, then `P : C^op ⥤ A` is a sheaf iff the underlying presheaf of types + `P ⋙ s : C^op ⥤ Type` is a sheaf (`category_theory.presheaf.is_sheaf_iff_is_sheaf_forget`). + Cf https://stacks.math.columbia.edu/tag/0073, which is a weaker version of this statement (it's + only over spaces, not sites) and https://stacks.math.columbia.edu/tag/00YR (a), which + additionally assumes filtered colimits. -/ universes v v' u' u @@ -62,7 +79,7 @@ def Sheaf : Type* := def Sheaf_to_presheaf : Sheaf J A ⥤ (Cᵒᵖ ⥤ A) := full_subcategory_inclusion (presheaf.is_sheaf J) -lemma Sheaf_iff_SheafOfTypes (P : Cᵒᵖ ⥤ Type v) : +lemma is_sheaf_iff_is_sheaf_of_type (P : Cᵒᵖ ⥤ Type v) : presheaf.is_sheaf J P ↔ presieve.is_sheaf J P := begin split, @@ -89,10 +106,10 @@ The category of sheaves taking values in Type is the same as the category of set @[simps] def Sheaf_equiv_SheafOfTypes : Sheaf J (Type v) ≌ SheafOfTypes J := { functor := - { obj := λ S, ⟨S.1, (Sheaf_iff_SheafOfTypes _ _).1 S.2⟩, + { obj := λ S, ⟨S.1, (is_sheaf_iff_is_sheaf_of_type _ _).1 S.2⟩, map := λ S₁ S₂ f, f }, inverse := - { obj := λ S, ⟨S.1, (Sheaf_iff_SheafOfTypes _ _).2 S.2⟩, + { obj := λ S, ⟨S.1, (is_sheaf_iff_is_sheaf_of_type _ _).2 S.2⟩, map := λ S₁ S₂ f, f }, unit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy), counit_iso := nat_iso.of_components (λ X, ⟨𝟙 _, 𝟙 _, by tidy, by tidy⟩) (by tidy) } From f793025a3a46aa1280692c20927f91195af4b199 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Fri, 30 Apr 2021 03:22:22 +0100 Subject: [PATCH 21/21] fix build --- src/category_theory/sites/sheaf.lean | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean index 3de7e5c3f5482..aec549949d100 100644 --- a/src/category_theory/sites/sheaf.lean +++ b/src/category_theory/sites/sheaf.lean @@ -139,9 +139,20 @@ section variables [has_products A] +/-- +The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram +of https://stacks.math.columbia.edu/tag/00VM. +-/ def first_obj : A := ∏ (λ (f : Σ V, {f : V ⟶ U // R f}), P.obj (op f.1)) +/-- +The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram +of https://stacks.math.columbia.edu/tag/00VM. +-/ +def fork_map : P.obj (op U) ⟶ first_obj R P := +pi.lift (λ f, P.map f.2.1.op) + variables [has_pullbacks C] /-- @@ -160,13 +171,6 @@ pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.fst.op) def second_map : first_obj R P ⟶ second_obj R P := pi.lift (λ fg, pi.π _ _ ≫ P.map pullback.snd.op) -/-- -The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram -of https://stacks.math.columbia.edu/tag/00VM. --/ -def fork_map : P.obj (op U) ⟶ first_obj R P := -pi.lift (λ f, P.map f.2.1.op) - lemma w : fork_map R P ≫ first_map R P = fork_map R P ≫ second_map R P := begin apply limit.hom_ext, @@ -177,6 +181,10 @@ begin simp, end +/-- +An alternative definition of the sheaf condition in terms of equalizers. This is shown to be +equivalent in `category_theory.presheaf.is_sheaf_iff_is_sheaf'`. +-/ def is_sheaf' (P : Cᵒᵖ ⥤ A) : Prop := ∀ (U : C) (R : presieve U) (hR : generate R ∈ J U), nonempty (is_limit (fork.of_ι _ (w R P))) @@ -247,7 +255,7 @@ for the category of topological spaces, topological rings, etc since reflecting hold. -/ lemma is_sheaf_iff_is_sheaf_forget (s : A ⥤ Type v) - [has_limits A] [preserves_limits s] [faithful s] [reflects_isomorphisms s] : + [has_limits A] [preserves_limits s] [reflects_isomorphisms s] : is_sheaf J P ↔ is_sheaf J (P ⋙ s) := begin rw [is_sheaf_iff_is_sheaf', is_sheaf_iff_is_sheaf'],