From 85d6221d32c37e68f05b2e42cde6cee658dae5e9 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 9 Nov 2022 03:23:30 +0000 Subject: [PATCH] refactor(topology/sheaf_condition): remove redundant constructions (#17378) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The constructions used to prove `is_sheaf_iff_is_sheaf_equalizer_products` in *sites.lean* is redundant because the equivalence can now be achieved via `is_sheaf` (site version) ↔ opens_le_cover ↔ pairwise_intersections ↔ equalizer_products. Refactoring the proof of this equivalence after removal of these constructions, however, requires rearranging the import chain and moving things around, explaining the large diff. The author @justus-springer of the constructions has previously [approved the removal](https://github.com/leanprover-community/mathlib/pull/11706#issuecomment-1024476451) in #11706. The universe levels in *equalizer_products.lean* are also fixed and generalized (a cover of a space should be indexed by a type in the same universe), leading to the addition of a few universe ascriptions. - [x] depends on: #17361 Co-authored-by: erd1 Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- .../sites/cover_preserving.lean | 2 +- src/topology/sheaves/forget.lean | 8 +- src/topology/sheaves/functors.lean | 2 +- src/topology/sheaves/limits.lean | 2 +- src/topology/sheaves/operations.lean | 1 - src/topology/sheaves/sheaf.lean | 10 +- .../sheaf_condition/equalizer_products.lean | 319 ++++++++++++- .../sheaf_condition/opens_le_cover.lean | 164 +------ .../pairwise_intersections.lean | 443 ++++++------------ .../sheaves/sheaf_condition/sites.lean | 367 +-------------- 10 files changed, 483 insertions(+), 835 deletions(-) diff --git a/src/category_theory/sites/cover_preserving.lean b/src/category_theory/sites/cover_preserving.lean index cf3e5ec25c110..27705c8d2d5bb 100644 --- a/src/category_theory/sites/cover_preserving.lean +++ b/src/category_theory/sites/cover_preserving.lean @@ -163,7 +163,7 @@ begin end lemma compatible_preserving_of_downwards_closed (F : C ⥤ D) [full F] [faithful F] - (hF : ∀ {c : C} {d : D} (f : d ⟶ F.obj c), Σ c', F.obj c' ≅ d) : compatible_preserving K F := + (hF : Π {c : C} {d : D} (f : d ⟶ F.obj c), Σ c', F.obj c' ≅ d) : compatible_preserving K F := begin constructor, introv hx he, diff --git a/src/topology/sheaves/forget.lean b/src/topology/sheaves/forget.lean index 4d1543b4af09e..fed5cc40b5b12 100644 --- a/src/topology/sheaves/forget.lean +++ b/src/topology/sheaves/forget.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ import category_theory.limits.preserves.shapes.products -import topology.sheaves.sheaf_condition.sites +import topology.sheaves.sheaf_condition.equalizer_products /-! # Checking the sheaf condition on the underlying presheaf of types. @@ -54,7 +54,7 @@ When `G` preserves limits, the sheaf condition diagram for `F` composed with `G` naturally isomorphic to the sheaf condition diagram for `F ⋙ G`. -/ def diagram_comp_preserves_limits : - diagram F U ⋙ G ≅ diagram (F ⋙ G) U := + diagram F U ⋙ G ≅ diagram.{v} (F ⋙ G) U := begin fapply nat_iso.of_components, rintro ⟨j⟩, @@ -82,7 +82,7 @@ When `G` preserves limits, the image under `G` of the sheaf condition fork for ` is the sheaf condition fork for `F ⋙ G`, postcomposed with the inverse of the natural isomorphism `diagram_comp_preserves_limits`. -/ -def map_cone_fork : G.map_cone (fork F U) ≅ +def map_cone_fork : G.map_cone (fork.{v} F U) ≅ (cones.postcompose (diagram_comp_preserves_limits G F U).inv).obj (fork (F ⋙ G) U) := cones.ext (iso.refl _) (λ j, begin @@ -168,7 +168,7 @@ begin -- image under `G` of the equalizer cone for the sheaf condition diagram. let c := fork (F ⋙ G) U, obtain ⟨hc⟩ := S U, - let d := G.map_cone (equalizer.fork (left_res F U) (right_res F U)), + let d := G.map_cone (equalizer.fork (left_res.{v} F U) (right_res F U)), letI := preserves_smallest_limits_of_preserves_limits G, have hd : is_limit d := preserves_limit.preserves (limit.is_limit _), -- Since both of these are limit cones diff --git a/src/topology/sheaves/functors.lean b/src/topology/sheaves/functors.lean index 573a63b629463..8693dff4d83a3 100644 --- a/src/topology/sheaves/functors.lean +++ b/src/topology/sheaves/functors.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Junyan Xu -/ -import topology.sheaves.sheaf_condition.opens_le_cover +import topology.sheaves.sheaf_condition.pairwise_intersections /-! # functors between categories of sheaves diff --git a/src/topology/sheaves/limits.lean b/src/topology/sheaves/limits.lean index f2dd492e36222..b00a5e1137deb 100644 --- a/src/topology/sheaves/limits.lean +++ b/src/topology/sheaves/limits.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import topology.sheaves.sheaf_condition.sites +import topology.sheaves.sheaf import category_theory.sites.limits import category_theory.adjunction import category_theory.limits.functor_category diff --git a/src/topology/sheaves/operations.lean b/src/topology/sheaves/operations.lean index ecf93ebc1111c..3c413e5b9fdd4 100644 --- a/src/topology/sheaves/operations.lean +++ b/src/topology/sheaves/operations.lean @@ -9,7 +9,6 @@ import algebra.category.Ring.filtered_colimits import algebra.category.Group.limits import ring_theory.localization.basic import topology.sheaves.sheafify -import topology.sheaves.sheaf_condition.sites /-! diff --git a/src/topology/sheaves/sheaf.lean b/src/topology/sheaves/sheaf.lean index 794e94d5c2aa8..16c82235c720e 100644 --- a/src/topology/sheaves/sheaf.lean +++ b/src/topology/sheaves/sheaf.lean @@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import topology.sheaves.sheaf_condition.equalizer_products +import topology.sheaves.presheaf import category_theory.full_subcategory import category_theory.limits.unit import category_theory.sites.sheaf @@ -44,8 +44,6 @@ variables {X : Top.{w}} (F : presheaf C X) {ι : Type v} (U : ι → opens X) namespace presheaf -open sheaf_condition_equalizer_products - /-- The sheaf condition has several different equivalent formulations. The official definition chosen here is in terms of grothendieck topologies so that the results on @@ -64,11 +62,13 @@ The equivalent formulations of the sheaf condition on `presheaf C X` are as foll See `Top.presheaf.is_sheaf_iff_is_sheaf_equalizer_products`. 3. `Top.presheaf.is_sheaf_opens_le_cover`: - Each `F(U)` is the (inverse) limit of all `F(V)` with `V ⊆ U`. + For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows + `F(V₁) ⟶ F(V₂)` for every pair of open sets `V₁ ⊇ V₂` that are contained in some `Uᵢ`. See `Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover`. 4. `Top.presheaf.is_sheaf_pairwise_intersections`: - For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of all `F(Uᵢ)` and all `F(Uᵢ ∩ Uⱼ)`. + For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows + from `F(Uᵢ)` and `F(Uⱼ)` to `F(Uᵢ ∩ Uⱼ)` for each pair `(i, j)`. See `Top.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections`. The following requires `C` to be concrete and complete, and `forget C` to reflect isomorphisms and diff --git a/src/topology/sheaves/sheaf_condition/equalizer_products.lean b/src/topology/sheaves/sheaf_condition/equalizer_products.lean index a81b7f0f9cca7..eb5b673ba8e0d 100644 --- a/src/topology/sheaves/sheaf_condition/equalizer_products.lean +++ b/src/topology/sheaves/sheaf_condition/equalizer_products.lean @@ -3,10 +3,9 @@ Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import category_theory.full_subcategory import category_theory.limits.shapes.equalizers import category_theory.limits.shapes.products -import topology.sheaves.presheaf +import topology.sheaves.sheaf_condition.pairwise_intersections /-! # The sheaf condition in terms of an equalizer of products @@ -16,6 +15,9 @@ e.g. as in https://stacks.math.columbia.edu/tag/0072 in terms of an equalizer diagram where the two objects are `∏ F.obj (U i)` and `∏ F.obj (U i) ⊓ (U j)`. +We show that this sheaf condition is equivalent to the `pairwise_intersections` sheaf condition when +the presheaf is valued in a category with products, and thereby equivalent to the default sheaf +condition. -/ universes v' v u @@ -30,8 +32,8 @@ open topological_space.opens namespace Top -variables {C : Type u} [category.{v} C] [has_products.{v} C] -variables {X : Top.{v'}} (F : presheaf C X) {ι : Type v} (U : ι → opens X) +variables {C : Type u} [category.{v} C] [has_products.{v'} C] +variables {X : Top.{v'}} (F : presheaf C X) {ι : Type v'} (U : ι → opens X) namespace presheaf @@ -49,21 +51,21 @@ def pi_inters : C := ∏ (λ p : ι × ι, F.obj (op (U p.1 ⊓ U p.2))) The morphism `Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j)` whose components are given by the restriction maps from `U i` to `U i ⊓ U j`. -/ -def left_res : pi_opens F U ⟶ pi_inters F U := +def left_res : pi_opens F U ⟶ pi_inters.{v'} F U := pi.lift (λ p : ι × ι, pi.π _ p.1 ≫ F.map (inf_le_left (U p.1) (U p.2)).op) /-- The morphism `Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j)` whose components are given by the restriction maps from `U j` to `U i ⊓ U j`. -/ -def right_res : pi_opens F U ⟶ pi_inters F U := +def right_res : pi_opens F U ⟶ pi_inters.{v'} F U := pi.lift (λ p : ι × ι, pi.π _ p.2 ≫ F.map (inf_le_right (U p.1) (U p.2)).op) /-- The morphism `F.obj U ⟶ Π F.obj (U i)` whose components are given by the restriction maps from `U j` to `U i ⊓ U j`. -/ -def res : F.obj (op (supr U)) ⟶ pi_opens F U := +def res : F.obj (op (supr U)) ⟶ pi_opens.{v'} F U := pi.lift (λ i : ι, F.map (topological_space.opens.le_supr U i).op) @[simp, elementwise] @@ -86,7 +88,7 @@ The equalizer diagram for the sheaf condition. -/ @[reducible] def diagram : walking_parallel_pair ⥤ C := -parallel_pair (left_res F U) (right_res F U) +parallel_pair (left_res.{v'} F U) (right_res F U) /-- The restriction map `F.obj U ⟶ Π F.obj (U i)` gives a cone over the equalizer diagram @@ -110,16 +112,16 @@ variables {F} {G : presheaf C X} /-- Isomorphic presheaves have isomorphic `pi_opens` for any cover `U`. -/ @[simp] -def pi_opens.iso_of_iso (α : F ≅ G) : pi_opens F U ≅ pi_opens G U := +def pi_opens.iso_of_iso (α : F ≅ G) : pi_opens F U ≅ pi_opens.{v'} G U := pi.map_iso (λ X, α.app _) /-- Isomorphic presheaves have isomorphic `pi_inters` for any cover `U`. -/ @[simp] -def pi_inters.iso_of_iso (α : F ≅ G) : pi_inters F U ≅ pi_inters G U := +def pi_inters.iso_of_iso (α : F ≅ G) : pi_inters F U ≅ pi_inters.{v'} G U := pi.map_iso (λ X, α.app _) /-- Isomorphic presheaves have isomorphic sheaf condition diagrams. -/ -def diagram.iso_of_iso (α : F ≅ G) : diagram F U ≅ diagram G U := +def diagram.iso_of_iso (α : F ≅ G) : diagram F U ≅ diagram.{v'} G U := nat_iso.of_components begin rintro ⟨⟩, exact pi_opens.iso_of_iso U α, exact pi_inters.iso_of_iso U α end begin @@ -155,7 +157,300 @@ is the equalizer of the two morphisms `∏ F.obj (U i) ⟶ ∏ F.obj (U i) ⊓ (U j)`. -/ def is_sheaf_equalizer_products (F : presheaf.{v' v u} C X) : Prop := -∀ ⦃ι : Type v⦄ (U : ι → opens X), nonempty (is_limit (sheaf_condition_equalizer_products.fork F U)) +∀ ⦃ι : Type v'⦄ (U : ι → opens X), nonempty (is_limit (sheaf_condition_equalizer_products.fork F U)) + +/-! +The remainder of this file shows that the equalizer_products sheaf condition is equivalent +to the pariwise_intersections sheaf condition. +-/ + +namespace sheaf_condition_pairwise_intersections + +open category_theory.pairwise category_theory.pairwise.hom + +/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +@[simps] +def cone_equiv_functor_obj (c : cone ((diagram U).op ⋙ F)) : + cone (sheaf_condition_equalizer_products.diagram F U) := +{ X := c.X, + π := + { app := λ Z, + walking_parallel_pair.cases_on Z + (pi.lift (λ (i : ι), c.π.app (op (single i)))) + (pi.lift (λ (b : ι × ι), c.π.app (op (pair b.1 b.2)))), + naturality' := λ Y Z f, + begin + cases Y; cases Z; cases f, + { ext i, dsimp, + simp only [limit.lift_π, category.id_comp, fan.mk_π_app, category_theory.functor.map_id, + category.assoc], + dsimp, + simp only [limit.lift_π, category.id_comp, fan.mk_π_app], }, + { ext ⟨i, j⟩, dsimp [sheaf_condition_equalizer_products.left_res], + simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, + category.assoc], + have h := c.π.naturality (quiver.hom.op (hom.left i j)), + dsimp at h, + simpa using h, }, + { ext ⟨i, j⟩, dsimp [sheaf_condition_equalizer_products.right_res], + simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, + category.assoc], + have h := c.π.naturality (quiver.hom.op (hom.right i j)), + dsimp at h, + simpa using h, }, + { ext i, dsimp, + simp only [limit.lift_π, category.id_comp, fan.mk_π_app, category_theory.functor.map_id, + category.assoc], + dsimp, + simp only [limit.lift_π, category.id_comp, fan.mk_π_app], }, + end, }, } + +section +local attribute [tidy] tactic.case_bash + +/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +@[simps] +def cone_equiv_functor : + limits.cone ((diagram U).op ⋙ F) ⥤ + limits.cone (sheaf_condition_equalizer_products.diagram F U) := +{ obj := λ c, cone_equiv_functor_obj F U c, + map := λ c c' f, + { hom := f.hom, + w' := λ j, begin + cases j; + { ext, simp only [limits.fan.mk_π_app, limits.cone_morphism.w, + limits.limit.lift_π, category.assoc, cone_equiv_functor_obj_π_app], }, + end }, }. + +end + +/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +@[simps] +def cone_equiv_inverse_obj + (c : limits.cone (sheaf_condition_equalizer_products.diagram F U)) : + limits.cone ((diagram U).op ⋙ F) := +{ X := c.X, + π := + { app := + begin + intro x, + induction x using opposite.rec, + rcases x with (⟨i⟩|⟨i,j⟩), + { exact c.π.app (walking_parallel_pair.zero) ≫ pi.π _ i, }, + { exact c.π.app (walking_parallel_pair.one) ≫ pi.π _ (i, j), } + end, + naturality' := + begin + intros x y f, + induction x using opposite.rec, + induction y using opposite.rec, + have ef : f = f.unop.op := rfl, + revert ef, + generalize : f.unop = f', + rintro rfl, + rcases x with ⟨i⟩|⟨⟩; rcases y with ⟨⟩|⟨j,j⟩; rcases f' with ⟨⟩, + { dsimp, erw [F.map_id], simp, }, + { dsimp, simp only [category.id_comp, category.assoc], + have h := c.π.naturality (walking_parallel_pair_hom.left), + dsimp [sheaf_condition_equalizer_products.left_res] at h, + simp only [category.id_comp] at h, + have h' := h =≫ pi.π _ (i, j), + rw h', + simp only [category.assoc, limit.lift_π, fan.mk_π_app], + refl, }, + { dsimp, simp only [category.id_comp, category.assoc], + have h := c.π.naturality (walking_parallel_pair_hom.right), + dsimp [sheaf_condition_equalizer_products.right_res] at h, + simp only [category.id_comp] at h, + have h' := h =≫ pi.π _ (j, i), + rw h', + simp, + refl, }, + { dsimp, erw [F.map_id], simp, }, + end, }, } + +/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +@[simps] +def cone_equiv_inverse : + limits.cone (sheaf_condition_equalizer_products.diagram F U) ⥤ + limits.cone ((diagram U).op ⋙ F) := +{ obj := λ c, cone_equiv_inverse_obj F U c, + map := λ c c' f, + { hom := f.hom, + w' := + begin + intro x, + induction x using opposite.rec, + rcases x with (⟨i⟩|⟨i,j⟩), + { dsimp, + dunfold fork.ι, + rw [←(f.w walking_parallel_pair.zero), category.assoc], }, + { dsimp, + rw [←(f.w walking_parallel_pair.one), category.assoc], }, + end }, }. + +/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +@[simps] +def cone_equiv_unit_iso_app + (c : cone ((diagram U).op ⋙ F)) : + (𝟭 (cone ((diagram U).op ⋙ F))).obj c ≅ + (cone_equiv_functor F U ⋙ cone_equiv_inverse F U).obj c := +{ hom := + { hom := 𝟙 _, + w' := λ j, begin + induction j using opposite.rec, rcases j; + { dsimp, simp only [limits.fan.mk_π_app, category.id_comp, limits.limit.lift_π], } + end, }, + inv := + { hom := 𝟙 _, + w' := λ j, begin + induction j using opposite.rec, rcases j; + { dsimp, simp only [limits.fan.mk_π_app, category.id_comp, limits.limit.lift_π], } + end }, + hom_inv_id' := begin + ext, + simp only [category.comp_id, limits.cone.category_comp_hom, limits.cone.category_id_hom], + end, + inv_hom_id' := begin + ext, + simp only [category.comp_id, limits.cone.category_comp_hom, limits.cone.category_id_hom], + end, } + +/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +@[simps] +def cone_equiv_unit_iso : + 𝟭 (limits.cone ((diagram U).op ⋙ F)) ≅ + cone_equiv_functor F U ⋙ cone_equiv_inverse F U := +nat_iso.of_components (cone_equiv_unit_iso_app F U) (by tidy) + +/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +@[simps] +def cone_equiv_counit_iso : + cone_equiv_inverse F U ⋙ cone_equiv_functor F U ≅ + 𝟭 (limits.cone (sheaf_condition_equalizer_products.diagram F U)) := +nat_iso.of_components (λ c, +{ hom := + { hom := 𝟙 _, + w' := + begin + rintro ⟨_|_⟩, + { ext ⟨j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, + { ext ⟨i,j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, + end }, + inv := + { hom := 𝟙 _, + w' := + begin + rintro ⟨_|_⟩, + { ext ⟨j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, + { ext ⟨i,j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, + end, }, + hom_inv_id' := by { ext, dsimp, simp only [category.comp_id], }, + inv_hom_id' := by { ext, dsimp, simp only [category.comp_id], }, }) +(λ c d f, by { ext, dsimp, simp only [category.comp_id, category.id_comp], }) + +/-- +Cones over `diagram U ⋙ F` are the same as a cones over the usual sheaf condition equalizer diagram. +-/ +@[simps] +def cone_equiv : + limits.cone ((diagram U).op ⋙ F) ≌ limits.cone (sheaf_condition_equalizer_products.diagram F U) := +{ functor := cone_equiv_functor F U, + inverse := cone_equiv_inverse F U, + unit_iso := cone_equiv_unit_iso F U, + counit_iso := cone_equiv_counit_iso F U, } + +local attribute [reducible] + sheaf_condition_equalizer_products.res + sheaf_condition_equalizer_products.left_res + +/-- +If `sheaf_condition_equalizer_products.fork` is an equalizer, +then `F.map_cone (cone U)` is a limit cone. +-/ +def is_limit_map_cone_of_is_limit_sheaf_condition_fork + (P : is_limit (sheaf_condition_equalizer_products.fork F U)) : + is_limit (F.map_cone (cocone U).op) := +is_limit.of_iso_limit ((is_limit.of_cone_equiv (cone_equiv F U).symm).symm P) +{ hom := + { hom := 𝟙 _, + w' := + begin + intro x, + induction x using opposite.rec, + rcases x with ⟨⟩, + { dsimp, simp, refl, }, + { dsimp, + simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, + category.assoc], + rw ←F.map_comp, + refl, } + end }, + inv := + { hom := 𝟙 _, + w' := + begin + intro x, + induction x using opposite.rec, + rcases x with ⟨⟩, + { dsimp, simp, refl, }, + { dsimp, + simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, + category.assoc], + rw ←F.map_comp, + refl, } + end }, + hom_inv_id' := by { ext, dsimp, simp only [category.comp_id], }, + inv_hom_id' := by { ext, dsimp, simp only [category.comp_id], }, } + +/-- +If `F.map_cone (cone U)` is a limit cone, +then `sheaf_condition_equalizer_products.fork` is an equalizer. +-/ +def is_limit_sheaf_condition_fork_of_is_limit_map_cone + (Q : is_limit (F.map_cone (cocone U).op)) : + is_limit (sheaf_condition_equalizer_products.fork F U) := +is_limit.of_iso_limit ((is_limit.of_cone_equiv (cone_equiv F U)).symm Q) +{ hom := + { hom := 𝟙 _, + w' := + begin + rintro ⟨⟩, + { dsimp, simp, refl, }, + { dsimp, ext ⟨i, j⟩, + simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, + category.assoc], + rw ←F.map_comp, + refl, } + end }, + inv := + { hom := 𝟙 _, + w' := + begin + rintro ⟨⟩, + { dsimp, simp, refl, }, + { dsimp, ext ⟨i, j⟩, + simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, + category.assoc], + rw ←F.map_comp, + refl, } + end }, + hom_inv_id' := by { ext, dsimp, simp only [category.comp_id], }, + inv_hom_id' := by { ext, dsimp, simp only [category.comp_id], }, } + +end sheaf_condition_pairwise_intersections + +open sheaf_condition_pairwise_intersections + +/-- +The sheaf condition in terms of an equalizer diagram is equivalent +to the default sheaf condition. +-/ +lemma is_sheaf_iff_is_sheaf_equalizer_products (F : presheaf C X) : + F.is_sheaf ↔ F.is_sheaf_equalizer_products := +(is_sheaf_iff_is_sheaf_pairwise_intersections F).trans $ +iff.intro (λ h ι U, ⟨is_limit_sheaf_condition_fork_of_is_limit_map_cone F U (h U).some⟩) + (λ h ι U, ⟨is_limit_map_cone_of_is_limit_sheaf_condition_fork F U (h U).some⟩) end presheaf diff --git a/src/topology/sheaves/sheaf_condition/opens_le_cover.lean b/src/topology/sheaves/sheaf_condition/opens_le_cover.lean index 240ab878ab389..59e5d0758b65f 100644 --- a/src/topology/sheaves/sheaf_condition/opens_le_cover.lean +++ b/src/topology/sheaves/sheaf_condition/opens_le_cover.lean @@ -3,9 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import topology.sheaves.presheaf -import category_theory.limits.final -import topology.sheaves.sheaf_condition.pairwise_intersections +import topology.sheaves.sheaf_condition.sites /-! # Another version of the sheaf condition. @@ -21,6 +19,13 @@ because we don't need to do any case bashing (depending on whether we're looking at single or double intersections, or equivalently whether we're looking at the first or second object in an equalizer diagram). +## Main statement + +`Top.presheaf.is_sheaf_iff_is_sheaf_opens_le_cover`: for a presheaf on a topological space, +the sheaf condition in terms of Grothendieck topology is equivalent to the `opens_le_cover` +sheaf condition. This result will be used to further connect to other sheaf conditions on spaces, +like `pairwise_intersections` and `equalizer_products`. + ## References * This is the definition Lurie uses in [Spectral Algebraic Geometry][LurieSAG]. -/ @@ -29,11 +34,7 @@ universes w v u noncomputable theory -open category_theory -open category_theory.limits -open topological_space -open opposite -open topological_space.opens +open category_theory category_theory.limits topological_space topological_space.opens opposite namespace Top @@ -95,144 +96,6 @@ mapping down to any `V` which is contained in some `U i`.) def is_sheaf_opens_le_cover : Prop := ∀ ⦃ι : Type w⦄ (U : ι → opens X), nonempty (is_limit (F.map_cone (opens_le_cover_cocone U).op)) -namespace sheaf_condition - -open category_theory.pairwise - -/-- -Implementation detail: -the object level of `pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U` --/ -@[simp] -def pairwise_to_opens_le_cover_obj : pairwise ι → opens_le_cover U -| (single i) := ⟨U i, ⟨i, le_rfl⟩⟩ -| (pair i j) := ⟨U i ⊓ U j, ⟨i, inf_le_left⟩⟩ - -open category_theory.pairwise.hom - -/-- -Implementation detail: -the morphism level of `pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U` --/ -def pairwise_to_opens_le_cover_map : - Π {V W : pairwise ι}, - (V ⟶ W) → (pairwise_to_opens_le_cover_obj U V ⟶ pairwise_to_opens_le_cover_obj U W) -| _ _ (id_single i) := 𝟙 _ -| _ _ (id_pair i j) := 𝟙 _ -| _ _ (left i j) := hom_of_le inf_le_left -| _ _ (right i j) := hom_of_le inf_le_right - -/-- -The category of single and double intersections of the `U i` maps into the category -of open sets below some `U i`. --/ -@[simps] -def pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U := -{ obj := pairwise_to_opens_le_cover_obj U, - map := λ V W i, pairwise_to_opens_le_cover_map U i, } - -instance (V : opens_le_cover U) : - nonempty (structured_arrow V (pairwise_to_opens_le_cover U)) := -⟨{ right := single (V.index), hom := V.hom_to_index }⟩ - -/-- -The diagram consisting of the `U i` and `U i ⊓ U j` is cofinal in the diagram -of all opens contained in some `U i`. --/ --- This is a case bash: for each pair of types of objects in `pairwise ι`, --- we have to explicitly construct a zigzag. -instance : functor.final (pairwise_to_opens_le_cover U) := -⟨λ V, is_connected_of_zigzag $ λ A B, begin - rcases A with ⟨⟨⟨⟩⟩, ⟨i⟩|⟨i,j⟩, a⟩; - rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩|⟨i',j'⟩, b⟩; - dsimp at *, - { refine ⟨[ - { left := ⟨⟨⟩⟩, right := pair i i', - hom := (le_inf a.le b.le).hom, }, _], _, rfl⟩, - exact - list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩) - (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) list.chain.nil) }, - { refine ⟨[ - { left := ⟨⟨⟩⟩, right := pair i' i, - hom := (le_inf (b.le.trans inf_le_left) a.le).hom, }, - { left := ⟨⟨⟩⟩, right := single i', - hom := (b.le.trans inf_le_left).hom, }, _], _, rfl⟩, - exact - list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := right i' i, }⟩) - (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i' i, }⟩) - (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i' j', }⟩) list.chain.nil)) }, - { refine ⟨[ - { left := ⟨⟨⟩⟩, right := single i, - hom := (a.le.trans inf_le_left).hom, }, - { left := ⟨⟨⟩⟩, right := pair i i', hom := - (le_inf (a.le.trans inf_le_left) b.le).hom, }, _], _, rfl⟩, - exact - list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i j, }⟩) - (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩) - (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) list.chain.nil)) }, - { refine ⟨[ - { left := ⟨⟨⟩⟩, right := single i, - hom := (a.le.trans inf_le_left).hom, }, - { left := ⟨⟨⟩⟩, right := pair i i', - hom := (le_inf (a.le.trans inf_le_left) (b.le.trans inf_le_left)).hom, }, - { left := ⟨⟨⟩⟩, right := single i', - hom := (b.le.trans inf_le_left).hom, }, _], _, rfl⟩, - exact - list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i j, }⟩) - (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩) - (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) - (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i' j', }⟩) list.chain.nil))), }, -end⟩ - -/-- -The diagram in `opens X` indexed by pairwise intersections from `U` is isomorphic -(in fact, equal) to the diagram factored through `opens_le_cover U`. --/ -def pairwise_diagram_iso : - pairwise.diagram U ≅ - pairwise_to_opens_le_cover U ⋙ full_subcategory_inclusion _ := -{ hom := { app := begin rintro (i|⟨i,j⟩); exact 𝟙 _, end, }, - inv := { app := begin rintro (i|⟨i,j⟩); exact 𝟙 _, end, }, } - -/-- -The cocone `pairwise.cocone U` with cocone point `supr U` over `pairwise.diagram U` is isomorphic -to the cocone `opens_le_cover_cocone U` (with the same cocone point) -after appropriate whiskering and postcomposition. --/ -def pairwise_cocone_iso : - (pairwise.cocone U).op ≅ - (cones.postcompose_equivalence (nat_iso.op (pairwise_diagram_iso U : _) : _)).functor.obj - ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op) := -cones.ext (iso.refl _) (by tidy) - -end sheaf_condition - -open sheaf_condition - -/-- -The sheaf condition -in terms of a limit diagram over all `{ V : opens X // ∃ i, V ≤ U i }` -is equivalent to the reformulation -in terms of a limit diagram over `U i` and `U i ⊓ U j`. --/ -lemma is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections : - F.is_sheaf_opens_le_cover ↔ F.is_sheaf_pairwise_intersections := -forall₂_congr $ λ ι U, equiv.nonempty_congr $ - calc is_limit (F.map_cone (opens_le_cover_cocone U).op) - ≃ is_limit ((F.map_cone (opens_le_cover_cocone U).op).whisker (pairwise_to_opens_le_cover U).op) - : (functor.initial.is_limit_whisker_equiv (pairwise_to_opens_le_cover U).op _).symm -... ≃ is_limit (F.map_cone ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op)) - : is_limit.equiv_iso_limit F.map_cone_whisker.symm -... ≃ is_limit ((cones.postcompose_equivalence _).functor.obj - (F.map_cone ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op))) - : (is_limit.postcompose_hom_equiv _ _).symm -... ≃ is_limit (F.map_cone ((cones.postcompose_equivalence _).functor.obj - ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op))) - : is_limit.equiv_iso_limit (functor.map_cone_postcompose_equivalence_functor _).symm -... ≃ is_limit (F.map_cone (pairwise.cocone U).op) - : is_limit.equiv_iso_limit - ((cones.functoriality _ _).map_iso (pairwise_cocone_iso U : _).symm) - section variables {Y : opens X} (hY : Y = supr U) @@ -314,15 +177,6 @@ begin rw ← (is_limit_opens_le_equiv_generate₂ F S hS).nonempty_congr, apply h }, end -/-- -The sheaf condition in terms of an equalizer diagram is equivalent -to the reformulation in terms of a limit diagram over `U i` and `U i ⊓ U j`. --/ -lemma is_sheaf_iff_is_sheaf_pairwise_intersections : - F.is_sheaf ↔ F.is_sheaf_pairwise_intersections := -by rw [is_sheaf_iff_is_sheaf_opens_le_cover, - is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections] - end end presheaf diff --git a/src/topology/sheaves/sheaf_condition/pairwise_intersections.lean b/src/topology/sheaves/sheaf_condition/pairwise_intersections.lean index 0790ce2f2e377..56368c81bbc3f 100644 --- a/src/topology/sheaves/sheaf_condition/pairwise_intersections.lean +++ b/src/topology/sheaves/sheaf_condition/pairwise_intersections.lean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ -import topology.sheaves.sheaf_condition.sites +import topology.sheaves.sheaf_condition.opens_le_cover +import category_theory.limits.final import category_theory.limits.preserves.basic import category_theory.category.pairwise import category_theory.limits.constructions.binary_products @@ -30,24 +31,22 @@ A presheaf `F : presheaf C X` is a sheaf precisely if it preserves this limit. We express this in two equivalent ways, as * `is_limit (F.map_cone (cone U))`, or * `preserves_limit (diagram U) F` + +We show that this sheaf condition is equivalent to the `opens_le_cover` sheaf condition, and +thereby also equivalent to the default sheaf condition. -/ noncomputable theory universes w v u -open topological_space -open Top -open opposite -open category_theory -open category_theory.limits +open topological_space Top opposite category_theory category_theory.limits -namespace Top.presheaf +variables {C : Type u} [category.{v} C] {X : Top.{w}} -variables {C : Type u} [category.{v} C] +namespace Top.presheaf section -variables {X : Top.{w}} /-- An alternative formulation of the sheaf condition @@ -74,319 +73,166 @@ def is_sheaf_preserves_limit_pairwise_intersections (F : presheaf C X) : Prop := end -/-! -The next part of this file shows that these conditions are equivalent -to the "equalizer products" sheaf condition. --/ +namespace sheaf_condition -variables {X : Top.{v}} [has_products.{v} C] +variables {ι : Type w} (U : ι → opens X) -namespace sheaf_condition_pairwise_intersections +open category_theory.pairwise -open category_theory.pairwise category_theory.pairwise.hom -open sheaf_condition_equalizer_products - -/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ -@[simps] -def cone_equiv_functor_obj (F : presheaf C X) - ⦃ι : Type v⦄ (U : ι → opens ↥X) (c : cone ((diagram U).op ⋙ F)) : - cone (sheaf_condition_equalizer_products.diagram F U) := -{ X := c.X, - π := - { app := λ Z, - walking_parallel_pair.cases_on Z - (pi.lift (λ (i : ι), c.π.app (op (single i)))) - (pi.lift (λ (b : ι × ι), c.π.app (op (pair b.1 b.2)))), - naturality' := λ Y Z f, - begin - cases Y; cases Z; cases f, - { ext i, dsimp, - simp only [limit.lift_π, category.id_comp, fan.mk_π_app, category_theory.functor.map_id, - category.assoc], - dsimp, - simp only [limit.lift_π, category.id_comp, fan.mk_π_app], }, - { ext ⟨i, j⟩, dsimp [sheaf_condition_equalizer_products.left_res], - simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, - category.assoc], - have h := c.π.naturality (quiver.hom.op (hom.left i j)), - dsimp at h, - simpa using h, }, - { ext ⟨i, j⟩, dsimp [sheaf_condition_equalizer_products.right_res], - simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, - category.assoc], - have h := c.π.naturality (quiver.hom.op (hom.right i j)), - dsimp at h, - simpa using h, }, - { ext i, dsimp, - simp only [limit.lift_π, category.id_comp, fan.mk_π_app, category_theory.functor.map_id, - category.assoc], - dsimp, - simp only [limit.lift_π, category.id_comp, fan.mk_π_app], }, - end, }, } +/-- +Implementation detail: +the object level of `pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U` +-/ +@[simp] +def pairwise_to_opens_le_cover_obj : pairwise ι → opens_le_cover U +| (single i) := ⟨U i, ⟨i, le_rfl⟩⟩ +| (pair i j) := ⟨U i ⊓ U j, ⟨i, inf_le_left⟩⟩ -section -local attribute [tidy] tactic.case_bash +open category_theory.pairwise.hom -/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ -@[simps] -def cone_equiv_functor (F : presheaf C X) - ⦃ι : Type v⦄ (U : ι → opens ↥X) : - limits.cone ((diagram U).op ⋙ F) ⥤ - limits.cone (sheaf_condition_equalizer_products.diagram F U) := -{ obj := λ c, cone_equiv_functor_obj F U c, - map := λ c c' f, - { hom := f.hom, - w' := λ j, begin - cases j; - { ext, simp only [limits.fan.mk_π_app, limits.cone_morphism.w, - limits.limit.lift_π, category.assoc, cone_equiv_functor_obj_π_app], }, - end }, }. - -end +/-- +Implementation detail: +the morphism level of `pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U` +-/ +def pairwise_to_opens_le_cover_map : + Π {V W : pairwise ι}, + (V ⟶ W) → (pairwise_to_opens_le_cover_obj U V ⟶ pairwise_to_opens_le_cover_obj U W) +| _ _ (id_single i) := 𝟙 _ +| _ _ (id_pair i j) := 𝟙 _ +| _ _ (left i j) := hom_of_le inf_le_left +| _ _ (right i j) := hom_of_le inf_le_right -/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ -@[simps] -def cone_equiv_inverse_obj (F : presheaf C X) - ⦃ι : Type v⦄ (U : ι → opens ↥X) - (c : limits.cone (sheaf_condition_equalizer_products.diagram F U)) : - limits.cone ((diagram U).op ⋙ F) := -{ X := c.X, - π := - { app := - begin - intro x, - induction x using opposite.rec, - rcases x with (⟨i⟩|⟨i,j⟩), - { exact c.π.app (walking_parallel_pair.zero) ≫ pi.π _ i, }, - { exact c.π.app (walking_parallel_pair.one) ≫ pi.π _ (i, j), } - end, - naturality' := - begin - intros x y f, - induction x using opposite.rec, - induction y using opposite.rec, - have ef : f = f.unop.op := rfl, - revert ef, - generalize : f.unop = f', - rintro rfl, - rcases x with ⟨i⟩|⟨⟩; rcases y with ⟨⟩|⟨j,j⟩; rcases f' with ⟨⟩, - { dsimp, erw [F.map_id], simp, }, - { dsimp, simp only [category.id_comp, category.assoc], - have h := c.π.naturality (walking_parallel_pair_hom.left), - dsimp [sheaf_condition_equalizer_products.left_res] at h, - simp only [category.id_comp] at h, - have h' := h =≫ pi.π _ (i, j), - rw h', - simp only [category.assoc, limit.lift_π, fan.mk_π_app], - refl, }, - { dsimp, simp only [category.id_comp, category.assoc], - have h := c.π.naturality (walking_parallel_pair_hom.right), - dsimp [sheaf_condition_equalizer_products.right_res] at h, - simp only [category.id_comp] at h, - have h' := h =≫ pi.π _ (j, i), - rw h', - simp, - refl, }, - { dsimp, erw [F.map_id], simp, }, - end, }, } - -/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ -@[simps] -def cone_equiv_inverse (F : presheaf C X) - ⦃ι : Type v⦄ (U : ι → opens ↥X) : - limits.cone (sheaf_condition_equalizer_products.diagram F U) ⥤ - limits.cone ((diagram U).op ⋙ F) := -{ obj := λ c, cone_equiv_inverse_obj F U c, - map := λ c c' f, - { hom := f.hom, - w' := - begin - intro x, - induction x using opposite.rec, - rcases x with (⟨i⟩|⟨i,j⟩), - { dsimp, - dunfold fork.ι, - rw [←(f.w walking_parallel_pair.zero), category.assoc], }, - { dsimp, - rw [←(f.w walking_parallel_pair.one), category.assoc], }, - end }, }. - -/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ -@[simps] -def cone_equiv_unit_iso_app (F : presheaf C X) ⦃ι : Type v⦄ (U : ι → opens ↥X) - (c : cone ((diagram U).op ⋙ F)) : - (𝟭 (cone ((diagram U).op ⋙ F))).obj c ≅ - (cone_equiv_functor F U ⋙ cone_equiv_inverse F U).obj c := -{ hom := - { hom := 𝟙 _, - w' := λ j, begin - induction j using opposite.rec, rcases j; - { dsimp, simp only [limits.fan.mk_π_app, category.id_comp, limits.limit.lift_π], } - end, }, - inv := - { hom := 𝟙 _, - w' := λ j, begin - induction j using opposite.rec, rcases j; - { dsimp, simp only [limits.fan.mk_π_app, category.id_comp, limits.limit.lift_π], } - end }, - hom_inv_id' := begin - ext, - simp only [category.comp_id, limits.cone.category_comp_hom, limits.cone.category_id_hom], - end, - inv_hom_id' := begin - ext, - simp only [category.comp_id, limits.cone.category_comp_hom, limits.cone.category_id_hom], - end, } - -/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ +/-- +The category of single and double intersections of the `U i` maps into the category +of open sets below some `U i`. +-/ @[simps] -def cone_equiv_unit_iso (F : presheaf C X) ⦃ι : Type v⦄ (U : ι → opens X) : - 𝟭 (limits.cone ((diagram U).op ⋙ F)) ≅ - cone_equiv_functor F U ⋙ cone_equiv_inverse F U := -nat_iso.of_components (cone_equiv_unit_iso_app F U) (by tidy) +def pairwise_to_opens_le_cover : pairwise ι ⥤ opens_le_cover U := +{ obj := pairwise_to_opens_le_cover_obj U, + map := λ V W i, pairwise_to_opens_le_cover_map U i, } -/-- Implementation of `sheaf_condition_pairwise_intersections.cone_equiv`. -/ -@[simps] -def cone_equiv_counit_iso (F : presheaf C X) ⦃ι : Type v⦄ (U : ι → opens X) : - cone_equiv_inverse F U ⋙ cone_equiv_functor F U ≅ - 𝟭 (limits.cone (sheaf_condition_equalizer_products.diagram F U)) := -nat_iso.of_components (λ c, -{ hom := - { hom := 𝟙 _, - w' := - begin - rintro ⟨_|_⟩, - { ext ⟨j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, - { ext ⟨i,j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, - end }, - inv := - { hom := 𝟙 _, - w' := - begin - rintro ⟨_|_⟩, - { ext ⟨j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, - { ext ⟨i,j⟩, dsimp, simp only [category.id_comp, limits.fan.mk_π_app, limits.limit.lift_π], }, - end, }, - hom_inv_id' := by { ext, dsimp, simp only [category.comp_id], }, - inv_hom_id' := by { ext, dsimp, simp only [category.comp_id], }, }) -(λ c d f, by { ext, dsimp, simp only [category.comp_id, category.id_comp], }) +instance (V : opens_le_cover U) : + nonempty (structured_arrow V (pairwise_to_opens_le_cover U)) := +⟨{ right := single (V.index), hom := V.hom_to_index }⟩ /-- -Cones over `diagram U ⋙ F` are the same as a cones over the usual sheaf condition equalizer diagram. +The diagram consisting of the `U i` and `U i ⊓ U j` is cofinal in the diagram +of all opens contained in some `U i`. -/ -@[simps] -def cone_equiv (F : presheaf C X) ⦃ι : Type v⦄ (U : ι → opens X) : - limits.cone ((diagram U).op ⋙ F) ≌ limits.cone (sheaf_condition_equalizer_products.diagram F U) := -{ functor := cone_equiv_functor F U, - inverse := cone_equiv_inverse F U, - unit_iso := cone_equiv_unit_iso F U, - counit_iso := cone_equiv_counit_iso F U, } +-- This is a case bash: for each pair of types of objects in `pairwise ι`, +-- we have to explicitly construct a zigzag. +instance : functor.final (pairwise_to_opens_le_cover U) := +⟨λ V, is_connected_of_zigzag $ λ A B, begin + rcases A with ⟨⟨⟨⟩⟩, ⟨i⟩|⟨i,j⟩, a⟩; + rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩|⟨i',j'⟩, b⟩; + dsimp at *, + { refine ⟨[ + { left := ⟨⟨⟩⟩, right := pair i i', + hom := (le_inf a.le b.le).hom, }, _], _, rfl⟩, + exact + list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩) + (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) list.chain.nil) }, + { refine ⟨[ + { left := ⟨⟨⟩⟩, right := pair i' i, + hom := (le_inf (b.le.trans inf_le_left) a.le).hom, }, + { left := ⟨⟨⟩⟩, right := single i', + hom := (b.le.trans inf_le_left).hom, }, _], _, rfl⟩, + exact + list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := right i' i, }⟩) + (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i' i, }⟩) + (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i' j', }⟩) list.chain.nil)) }, + { refine ⟨[ + { left := ⟨⟨⟩⟩, right := single i, + hom := (a.le.trans inf_le_left).hom, }, + { left := ⟨⟨⟩⟩, right := pair i i', hom := + (le_inf (a.le.trans inf_le_left) b.le).hom, }, _], _, rfl⟩, + exact + list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i j, }⟩) + (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩) + (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) list.chain.nil)) }, + { refine ⟨[ + { left := ⟨⟨⟩⟩, right := single i, + hom := (a.le.trans inf_le_left).hom, }, + { left := ⟨⟨⟩⟩, right := pair i i', + hom := (le_inf (a.le.trans inf_le_left) (b.le.trans inf_le_left)).hom, }, + { left := ⟨⟨⟩⟩, right := single i', + hom := (b.le.trans inf_le_left).hom, }, _], _, rfl⟩, + exact + list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := left i j, }⟩) + (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i i', }⟩) + (list.chain.cons (or.inl ⟨{ left := 𝟙 _, right := right i i', }⟩) + (list.chain.cons (or.inr ⟨{ left := 𝟙 _, right := left i' j', }⟩) list.chain.nil))), }, +end⟩ -local attribute [reducible] - sheaf_condition_equalizer_products.res - sheaf_condition_equalizer_products.left_res +/-- +The diagram in `opens X` indexed by pairwise intersections from `U` is isomorphic +(in fact, equal) to the diagram factored through `opens_le_cover U`. +-/ +def pairwise_diagram_iso : + pairwise.diagram U ≅ + pairwise_to_opens_le_cover U ⋙ full_subcategory_inclusion _ := +{ hom := { app := begin rintro (i|⟨i,j⟩); exact 𝟙 _, end, }, + inv := { app := begin rintro (i|⟨i,j⟩); exact 𝟙 _, end, }, } /-- -If `sheaf_condition_equalizer_products.fork` is an equalizer, -then `F.map_cone (cone U)` is a limit cone. +The cocone `pairwise.cocone U` with cocone point `supr U` over `pairwise.diagram U` is isomorphic +to the cocone `opens_le_cover_cocone U` (with the same cocone point) +after appropriate whiskering and postcomposition. -/ -def is_limit_map_cone_of_is_limit_sheaf_condition_fork - (F : presheaf C X) ⦃ι : Type v⦄ (U : ι → opens X) - (P : is_limit (sheaf_condition_equalizer_products.fork F U)) : - is_limit (F.map_cone (cocone U).op) := -is_limit.of_iso_limit ((is_limit.of_cone_equiv (cone_equiv F U).symm).symm P) -{ hom := - { hom := 𝟙 _, - w' := - begin - intro x, - induction x using opposite.rec, - rcases x with ⟨⟩, - { dsimp, simp, refl, }, - { dsimp, - simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, - category.assoc], - rw ←F.map_comp, - refl, } - end }, - inv := - { hom := 𝟙 _, - w' := - begin - intro x, - induction x using opposite.rec, - rcases x with ⟨⟩, - { dsimp, simp, refl, }, - { dsimp, - simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, - category.assoc], - rw ←F.map_comp, - refl, } - end }, - hom_inv_id' := by { ext, dsimp, simp only [category.comp_id], }, - inv_hom_id' := by { ext, dsimp, simp only [category.comp_id], }, } +def pairwise_cocone_iso : + (pairwise.cocone U).op ≅ + (cones.postcompose_equivalence (nat_iso.op (pairwise_diagram_iso U : _) : _)).functor.obj + ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op) := +cones.ext (iso.refl _) (by tidy) + +end sheaf_condition + +open sheaf_condition + +variable (F : presheaf C X) /-- -If `F.map_cone (cone U)` is a limit cone, -then `sheaf_condition_equalizer_products.fork` is an equalizer. +The sheaf condition +in terms of a limit diagram over all `{ V : opens X // ∃ i, V ≤ U i }` +is equivalent to the reformulation +in terms of a limit diagram over `U i` and `U i ⊓ U j`. -/ -def is_limit_sheaf_condition_fork_of_is_limit_map_cone - (F : presheaf C X) ⦃ι : Type v⦄ (U : ι → opens X) - (Q : is_limit (F.map_cone (cocone U).op)) : - is_limit (sheaf_condition_equalizer_products.fork F U) := -is_limit.of_iso_limit ((is_limit.of_cone_equiv (cone_equiv F U)).symm Q) -{ hom := - { hom := 𝟙 _, - w' := - begin - rintro ⟨⟩, - { dsimp, simp, refl, }, - { dsimp, ext ⟨i, j⟩, - simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, - category.assoc], - rw ←F.map_comp, - refl, } - end }, - inv := - { hom := 𝟙 _, - w' := - begin - rintro ⟨⟩, - { dsimp, simp, refl, }, - { dsimp, ext ⟨i, j⟩, - simp only [limit.lift_π, limit.lift_π_assoc, category.id_comp, fan.mk_π_app, - category.assoc], - rw ←F.map_comp, - refl, } - end }, - hom_inv_id' := by { ext, dsimp, simp only [category.comp_id], }, - inv_hom_id' := by { ext, dsimp, simp only [category.comp_id], }, } - -end sheaf_condition_pairwise_intersections - -open sheaf_condition_pairwise_intersections +lemma is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections : + F.is_sheaf_opens_le_cover ↔ F.is_sheaf_pairwise_intersections := +forall₂_congr $ λ ι U, equiv.nonempty_congr $ + calc is_limit (F.map_cone (opens_le_cover_cocone U).op) + ≃ is_limit ((F.map_cone (opens_le_cover_cocone U).op).whisker (pairwise_to_opens_le_cover U).op) + : (functor.initial.is_limit_whisker_equiv (pairwise_to_opens_le_cover U).op _).symm +... ≃ is_limit (F.map_cone ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op)) + : is_limit.equiv_iso_limit F.map_cone_whisker.symm +... ≃ is_limit ((cones.postcompose_equivalence _).functor.obj + (F.map_cone ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op))) + : (is_limit.postcompose_hom_equiv _ _).symm +... ≃ is_limit (F.map_cone ((cones.postcompose_equivalence _).functor.obj + ((opens_le_cover_cocone U).op.whisker (pairwise_to_opens_le_cover U).op))) + : is_limit.equiv_iso_limit (functor.map_cone_postcompose_equivalence_functor _).symm +... ≃ is_limit (F.map_cone (pairwise.cocone U).op) + : is_limit.equiv_iso_limit + ((cones.functoriality _ _).map_iso (pairwise_cocone_iso U : _).symm) /-- The sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of a limit diagram over `U i` and `U i ⊓ U j`. -A more general version `is_sheaf_iff_is_sheaf_pairwise_intersections` without -the `has_products` assumption is available in a later file. -/ -lemma is_sheaf_iff_is_sheaf_pairwise_intersections' (F : presheaf C X) : +lemma is_sheaf_iff_is_sheaf_pairwise_intersections : F.is_sheaf ↔ F.is_sheaf_pairwise_intersections := -(is_sheaf_iff_is_sheaf_equalizer_products F).trans $ -iff.intro (λ h ι U, ⟨is_limit_map_cone_of_is_limit_sheaf_condition_fork F U (h U).some⟩) - (λ h ι U, ⟨is_limit_sheaf_condition_fork_of_is_limit_map_cone F U (h U).some⟩) +by rw [is_sheaf_iff_is_sheaf_opens_le_cover, + is_sheaf_opens_le_cover_iff_is_sheaf_pairwise_intersections] /-- The sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of the presheaf preserving the limit of the diagram consisting of the `U i` and `U i ⊓ U j`. -/ -lemma is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections (F : presheaf C X) : +lemma is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections : F.is_sheaf ↔ F.is_sheaf_preserves_limit_pairwise_intersections := begin - rw is_sheaf_iff_is_sheaf_pairwise_intersections', + rw is_sheaf_iff_is_sheaf_pairwise_intersections, split, { intros h ι U, exact ⟨preserves_limit_of_preserves_limit_cone (pairwise.cocone_is_colimit U).op (h U).some⟩ }, @@ -399,7 +245,6 @@ end Top.presheaf namespace Top.sheaf -variables {X : Top.{v}} {C : Type u} [category.{v} C] variables (F : X.sheaf C) (U V : opens X) open category_theory.limits @@ -420,15 +265,12 @@ pullback_cone.mk (F.1.map (hom_of_le le_sup_left).op) (F.1.map (hom_of_le le_sup variable (s : pullback_cone (F.1.map (hom_of_le inf_le_left : U ⊓ V ⟶ _).op) (F.1.map (hom_of_le inf_le_right).op)) -variable [has_products.{v} C] - /-- (Implementation). Every cone over `F(U) ⟶ F(U ⊓ V)` and `F(V) ⟶ F(U ⊓ V)` factors through `F(U ⊔ V)`. -TODO: generalize to `C` without products. -/ def inter_union_pullback_cone_lift : s.X ⟶ F.1.obj (op (U ⊔ V)) := begin - let ι : ulift.{v} walking_pair → opens X := λ j, walking_pair.cases_on j.down U V, + let ι : ulift.{w} walking_pair → opens X := λ j, walking_pair.cases_on j.down U V, have hι : U ⊔ V = supr ι, { ext, rw [opens.coe_supr, set.mem_Union], @@ -437,7 +279,7 @@ begin exacts [⟨⟨walking_pair.left⟩, h⟩, ⟨⟨walking_pair.right⟩, h⟩] }, { rintro ⟨⟨_ | _⟩, h⟩, exacts [or.inl h, or.inr h] } }, - refine (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 ι).some.lift + refine (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 ι).some.lift ⟨s.X, { app := _, naturality' := _ }⟩ ≫ F.1.map (eq_to_hom hι).op, { apply opposite.rec, rintro ((_|_)|(_|_)), @@ -458,9 +300,8 @@ end lemma inter_union_pullback_cone_lift_left : inter_union_pullback_cone_lift F U V s ≫ F.1.map (hom_of_le le_sup_left).op = s.fst := begin - dsimp, erw [category.assoc, ←F.1.map_comp], - exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 _).some.fac _ + exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 _).some.fac _ (op $ pairwise.single (ulift.up walking_pair.left)) end @@ -468,14 +309,14 @@ lemma inter_union_pullback_cone_lift_right : inter_union_pullback_cone_lift F U V s ≫ F.1.map (hom_of_le le_sup_right).op = s.snd := begin erw [category.assoc, ←F.1.map_comp], - exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 _).some.fac _ + exact (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 _).some.fac _ (op $ pairwise.single (ulift.up walking_pair.right)) end /-- For a sheaf `F`, `F(U ⊔ V)` is the pullback of `F(U) ⟶ F(U ⊓ V)` and `F(V) ⟶ F(U ⊓ V)`. -/ def is_limit_pullback_cone : is_limit (inter_union_pullback_cone F U V) := begin - let ι : ulift.{v} walking_pair → opens X := λ ⟨j⟩, walking_pair.cases_on j U V, + let ι : ulift.{w} walking_pair → opens X := λ ⟨j⟩, walking_pair.cases_on j U V, have hι : U ⊔ V = supr ι, { ext, rw [opens.coe_supr, set.mem_Union], @@ -492,7 +333,7 @@ begin { apply inter_union_pullback_cone_lift_right }, { intros m h₁ h₂, rw ← cancel_mono (F.1.map (eq_to_hom hι.symm).op), - apply (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections'.mp F.2 ι).some.hom_ext, + apply (F.presheaf.is_sheaf_iff_is_sheaf_pairwise_intersections.mp F.2 ι).some.hom_ext, apply opposite.rec, rintro ((_|_)|(_|_)); rw [category.assoc, category.assoc], { erw ← F.1.map_comp, diff --git a/src/topology/sheaves/sheaf_condition/sites.lean b/src/topology/sheaves/sheaf_condition/sites.lean index bdc097dae3750..ebc32d829f9d0 100644 --- a/src/topology/sheaves/sheaf_condition/sites.lean +++ b/src/topology/sheaves/sheaf_condition/sites.lean @@ -10,38 +10,27 @@ import category_theory.sites.dense_subsite /-! -# The sheaf condition in terms of sites. +# Coverings and sieves; from sheaves on sites and sheaves on spaces -The theory of sheaves on sites was developed independently from sheaves on spaces in -`category_theory/sites`. In this file, we connect the two theories: We show that for a topological -space `X`, a presheaf `F : (opens X)ᵒᵖ ⥤ C` is a sheaf on the site `opens X` if and only if it is -a sheaf on `X` in terms of `is_sheaf_equalizer_products`. +In this file, we connect coverings in a topological space to sieves in the associated Grothendieck +topology, in preparation of connecting the sheaf condition on sites to the various sheaf conditions +on spaces. -Recall that a presheaf `F : (opens X)ᵒᵖ ⥤ C` is called a *sheaf* on the space `X`, if for every -family of opens `U : ι → opens X`, the object `F.obj (op (supr U))` is the limit of some fork -diagram. On the other hand, `F` is called a *sheaf* on the site `opens X`, if for every open set -`U : opens X` and every presieve `R : presieve U`, the object `F.obj (op U)` is the limit of a -very similar fork diagram. In this file, we will construct the two functions `covering_of_presieve` -and `presieve_of_covering`, which translate between the two concepts. We then prove a bunch of -naturality lemmas relating the two fork diagrams to each other. - -## Main statements -* `is_sheaf_iff_is_sheaf_equalizer_products`. A presheaf `F : (opens X)ᵒᵖ ⥤ C` is a sheaf on the - site `opens X` if and only if it is a sheaf on the space `X`. +We also specialize results about sheaves on sites to sheaves on spaces; we show that the inclusion +functor from a topological basis to `topological_space.opens` is cover_dense, that open maps +induce cover_preserving functors, and that open embeddings induce compatible_preserving functors. -/ noncomputable theory -universes u v w +universes w v u -namespace Top.presheaf +open category_theory topological_space -open category_theory topological_space Top category_theory.limits opposite -open Top.presheaf.sheaf_condition_equalizer_products +namespace Top.presheaf -variables {C : Type u} [category.{v} C] [has_products.{v} C] -variables {X : Top.{v}} (F : presheaf C X) +variables {X : Top.{w}} /-- Given a presieve `R` on `U`, we obtain a covering family of open sets in `X`, by taking as index @@ -58,21 +47,6 @@ namespace covering_of_presieve variables (U : opens X) (R : presieve U) -/-! -In this section, we will relate two different fork diagrams to each other. - -The first one is the defining fork diagram for the sheaf condition in terms of sites, applied to -the presieve `R`. It will henceforth be called the _sites diagram_. Its objects are called -`presheaf.first_obj` and `presheaf.second_obj` and its morphisms are `presheaf.first_map` and -`presheaf.second_obj`. The fork map into this diagram is called `presheaf.fork_map`. - -The second one is the defining fork diagram for the sheaf condition in terms of spaces, applied to -the family of opens `covering_of_presieve U R`. It will henceforth be called the _spaces diagram_. -Its objects are called `pi_opens` and `pi_inters` and its morphisms are `left_res` and `right_res`. -The fork map into this diagram is called `res`. - --/ - /-- If `R` is a presieve in the grothendieck topology on `opens X`, the covering family associated to `R` really is _covering_, i.e. the union of all open sets equals `U`. @@ -90,159 +64,8 @@ begin exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩, end -/-- -The first object in the sites diagram is isomorphic to the first object in the spaces diagram. -Actually, they are even definitionally equal, but it is convenient to give this isomorphism a name. --/ -def first_obj_iso_pi_opens : presheaf.first_obj R F ≅ pi_opens F (covering_of_presieve U R) := -eq_to_iso rfl - -/-- -The isomorphism `first_obj_iso_pi_opens` is compatible with canonical projections out of the -product. --/ -lemma first_obj_iso_pi_opens_π (f : Σ V, {f : V ⟶ U // R f}) : - (first_obj_iso_pi_opens F U R).hom ≫ pi.π _ f = pi.π _ f := -category.id_comp _ - -/-- -The second object in the sites diagram is isomorphic to the second object in the spaces diagram. --/ -def second_obj_iso_pi_inters : - presheaf.second_obj R F ≅ pi_inters F (covering_of_presieve U R) := -has_limit.iso_of_nat_iso $ discrete.nat_iso $ λ i, - F.map_iso (eq_to_iso (complete_lattice.pullback_eq_inf _ _).symm).op - -/-- -The isomorphism `second_obj_iso_pi_inters` is compatible with canonical projections out of the -product. Here, we have to insert an `eq_to_hom` arrow to pass from -`F.obj (op (pullback f.2.1 g.2.1))` to `F.obj (op (f.1 ⊓ g.1))`. --/ -lemma second_obj_iso_pi_inters_π (f g : Σ V, {f : V ⟶ U // R f}) : - (second_obj_iso_pi_inters F U R).hom ≫ pi.π _ (f, g) = - pi.π _ (f, g) ≫ F.map (eq_to_hom (complete_lattice.pullback_eq_inf f.2.1 g.2.1).symm).op := -begin - dunfold second_obj_iso_pi_inters, - rw has_limit.iso_of_nat_iso_hom_π, - refl, -end - -/-- -Composing the fork map of the sites diagram with the isomorphism `first_obj_iso_pi_opens` is the -same as the fork map of the spaces diagram (modulo an `eq_to_hom` arrow). --/ -lemma fork_map_comp_first_obj_iso_pi_opens_eq - (hR : sieve.generate R ∈ opens.grothendieck_topology X U) : - presheaf.fork_map R F ≫ (first_obj_iso_pi_opens F U R).hom = - F.map (eq_to_hom (supr_eq_of_mem_grothendieck U R hR)).op ≫ res F (covering_of_presieve U R) := -begin - ext ⟨f⟩, - rw [category.assoc, category.assoc, first_obj_iso_pi_opens_π], - dunfold presheaf.fork_map res, - rw [limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app, ← F.map_comp], - congr, -end - -/-- -First naturality condition. Under the isomorphisms `first_obj_iso_pi_opens` and -`second_obj_iso_pi_inters`, the map `presheaf.first_map` corresponds to `left_res`. --/ -lemma first_obj_iso_comp_left_res_eq : - presheaf.first_map R F ≫ (second_obj_iso_pi_inters F U R).hom = - (first_obj_iso_pi_opens F U R).hom ≫ left_res F (covering_of_presieve U R) := -begin - ext ⟨f, g⟩, - rw [category.assoc, category.assoc, second_obj_iso_pi_inters_π], - dunfold left_res presheaf.first_map, - rw [limit.lift_π, fan.mk_π_app, limit.lift_π_assoc, fan.mk_π_app, ← category.assoc], - erw [first_obj_iso_pi_opens_π, category.assoc, ← F.map_comp], - refl, -end - -/-- -Second naturality condition. Under the isomorphisms `first_obj_iso_pi_opens` and -`second_obj_iso_pi_inters`, the map `presheaf.second_map` corresponds to `right_res`. --/ -lemma first_obj_iso_comp_right_res_eq : - presheaf.second_map R F ≫ (second_obj_iso_pi_inters F U R).hom = - (first_obj_iso_pi_opens F U R).hom ≫ right_res F (covering_of_presieve U R) := -begin - ext ⟨f, g⟩, - dunfold right_res presheaf.second_map, - rw [category.assoc, category.assoc, second_obj_iso_pi_inters_π, limit.lift_π, fan.mk_π_app, - limit.lift_π_assoc, fan.mk_π_app, ← category.assoc, first_obj_iso_pi_opens_π, category.assoc, - ← F.map_comp], - refl, -end - -/-- The natural isomorphism between the sites diagram and the spaces diagram. -/ -@[simps] -def diagram_nat_iso : parallel_pair (presheaf.first_map R F) (presheaf.second_map R F) ≅ - diagram F (covering_of_presieve U R) := -nat_iso.of_components - (λ i, walking_parallel_pair.cases_on i - (first_obj_iso_pi_opens F U R) - (second_obj_iso_pi_inters F U R)) $ -begin - intros i j f, - cases i, - { cases j, - { cases f, simp }, - { cases f, - { exact first_obj_iso_comp_left_res_eq F U R, }, - { exact first_obj_iso_comp_right_res_eq F U R, } } }, - { cases j, - { cases f, }, - { cases f, simp } }, -end - -/-- -Postcomposing the given fork of the _sites_ diagram with the natural isomorphism between the -diagrams gives us a fork of the _spaces_ diagram. We construct a morphism from this fork to the -given fork of the _spaces_ diagram. This is shown to be an isomorphism below. --/ -@[simps] -def postcompose_diagram_fork_hom (hR : sieve.generate R ∈ opens.grothendieck_topology X U) : - (cones.postcompose (diagram_nat_iso F U R).hom).obj (fork.of_ι _ (presheaf.w R F)) ⟶ - fork F (covering_of_presieve U R) := -fork.mk_hom (F.map (eq_to_hom (supr_eq_of_mem_grothendieck U R hR)).op) - (fork_map_comp_first_obj_iso_pi_opens_eq F U R hR).symm - -instance is_iso_postcompose_diagram_fork_hom_hom - (hR : sieve.generate R ∈ opens.grothendieck_topology X U) : - is_iso (postcompose_diagram_fork_hom F U R hR).hom := -begin - rw [postcompose_diagram_fork_hom_hom, eq_to_hom_map], - apply eq_to_hom.is_iso, -end - -instance is_iso_postcompose_diagram_fork_hom - (hR : sieve.generate R ∈ opens.grothendieck_topology X U) : - is_iso (postcompose_diagram_fork_hom F U R hR) := -cones.cone_iso_of_hom_iso _ - -/-- See `postcompose_diagram_fork_hom`. -/ -def postcompose_diagram_fork_iso (hR : sieve.generate R ∈ opens.grothendieck_topology X U) : - (cones.postcompose (diagram_nat_iso F U R).hom).obj (fork.of_ι _ (presheaf.w R F)) ≅ - fork F (covering_of_presieve U R) := -as_iso (postcompose_diagram_fork_hom F U R hR) - end covering_of_presieve -lemma is_sheaf_of_is_sheaf_equalizer_products (Fsh : F.is_sheaf_equalizer_products) : - F.is_sheaf := -begin - delta is_sheaf, - rw presheaf.is_sheaf_iff_is_sheaf', - intros U R hR, - refine ⟨_⟩, - apply (is_limit.of_cone_equiv (cones.postcompose_equivalence - (covering_of_presieve.diagram_nat_iso F U R : _))).to_fun, - apply (is_limit.equiv_iso_limit - (covering_of_presieve.postcompose_diagram_fork_iso F U R hR)).inv_fun, - exact (Fsh (covering_of_presieve U R)).some, -end - /-- Given a family of opens `U : ι → opens X` and any open `Y : opens X`, we obtain a presieve on `Y` by declaring that a morphism `f : V ⟶ Y` is a member of the presieve if and only if @@ -265,21 +88,6 @@ by { ext Z f, exact ⟨λ ⟨⟨_,_,h⟩,rfl⟩, by convert h, λ h, ⟨⟨Z,f,h namespace presieve_of_covering -/-! -In this section, we will relate two different fork diagrams to each other. - -The first one is the defining fork diagram for the sheaf condition in terms of spaces, applied to -the family of opens `U`. It will henceforth be called the _spaces diagram_. Its objects are called -`pi_opens` and `pi_inters` and its morphisms are `left_res` and `right_res`. The fork map into this -diagram is called `res`. - -The second one is the defining fork diagram for the sheaf condition in terms of sites, applied to -the presieve `presieve_of_covering U`. It will henceforth be called the _sites diagram_. Its objects -are called `presheaf.first_obj` and `presheaf.second_obj` and its morphisms are `presheaf.first_map` -and `presheaf.second_obj`. The fork map into this diagram is called `presheaf.fork_map`. - --/ - variables {ι : Type v} (U : ι → opens X) /-- @@ -309,161 +117,12 @@ def index_of_hom (f : Σ V, {f : V ⟶ supr U // presieve_of_covering U f}) : ι lemma index_of_hom_spec (f : Σ V, {f : V ⟶ supr U // presieve_of_covering U f}) : f.1 = U (index_of_hom U f) := f.2.2.some_spec -/-- -The canonical morphism from the first object in the sites diagram to the first object in the -spaces diagram. Note that this is *not* an isomorphism, as the product `pi_opens F U` may contain -duplicate factors, i.e. `U : ι → opens X` may not be injective. --/ -def first_obj_to_pi_opens : presheaf.first_obj (presieve_of_covering U) F ⟶ pi_opens F U := -pi.lift (λ i, pi.π _ (hom_of_index U i)) - -/-- -The canonical morphism from the first object in the spaces diagram to the first object in the -sites diagram. Note that this is *not* an isomorphism, as the product `pi_opens F U` may contain -duplicate factors, i.e. `U : ι → opens X` may not be injective. --/ -def pi_opens_to_first_obj : pi_opens F U ⟶ - presheaf.first_obj.{v v u} (presieve_of_covering U) F := -pi.lift (λ f, pi.π _ (index_of_hom U f) ≫ F.map (eq_to_hom (index_of_hom_spec U f)).op) - -/-- -Even though `first_obj_to_pi_opens` and `pi_opens_to_first_obj` are not inverse to each other, -applying them both after a fork map `s.ι` does nothing. The intuition here is that a compatible -family `s : Π i : ι, F.obj (op (U i))` does not care about duplicate open sets: -If `U i = U j` the compatible family coincides on the intersection `U i ⊓ U j = U i = U j`, -hence `s i = s j` (module an `eq_to_hom` arrow). --/ -lemma fork_ι_comp_pi_opens_to_first_obj_to_pi_opens_eq - (s : limits.fork (left_res F U) (right_res F U)) : - s.ι ≫ pi_opens_to_first_obj F U ≫ first_obj_to_pi_opens F U = s.ι := -begin - ext ⟨j⟩, - dunfold first_obj_to_pi_opens pi_opens_to_first_obj, - rw [category.assoc, category.assoc, limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app], - -- The issue here is that `index_of_hom U (hom_of_index U j)` need not be equal to `j`. - -- But `U j = U (index_of_hom U (hom_of_index U j))` and hence we obtain the following - -- `eq_to_hom` arrow: - have i_eq : U j ⟶ U j ⊓ U (index_of_hom U (hom_of_index U j)), - { apply eq_to_hom, rw ← index_of_hom_spec U, exact inf_idem.symm, }, - -- Since `s` is a fork, we know that `s.ι ≫ left_res F U = s.ι ≫ right_res F U`. - -- We compose both sides of this equality with the canonical projection at the index pair - -- `(j, index_of_hom U (hom_of_index U j)` and the restriction along `i_eq`. - have := congr_arg (λ f, f ≫ - pi.π (λ p : ι × ι, F.obj (op (U p.1 ⊓ U p.2))) (j, index_of_hom U (hom_of_index U j)) ≫ - F.map i_eq.op) s.condition, - dsimp at this, - rw [category.assoc, category.assoc] at this, - symmetry, - -- We claim that this is equality is our goal - convert this using 2, - { dunfold left_res, - rw [limit.lift_π_assoc, fan.mk_π_app, category.assoc, ← F.map_comp], - erw F.map_id, - rw category.comp_id }, - { dunfold right_res, - rw [limit.lift_π_assoc, fan.mk_π_app, category.assoc, ← F.map_comp], - congr, } -end - -/-- -The canonical morphism from the second object of the spaces diagram to the second object of the -sites diagram. --/ -def pi_inters_to_second_obj : pi_inters F U ⟶ - presheaf.second_obj.{v v u} (presieve_of_covering U) F := -pi.lift (λ f, pi.π _ (index_of_hom U f.fst, index_of_hom U f.snd) ≫ - F.map (eq_to_hom - (by rw [complete_lattice.pullback_eq_inf, ← index_of_hom_spec U, ← index_of_hom_spec U])).op) - -lemma pi_opens_to_first_obj_comp_fist_map_eq : - pi_opens_to_first_obj F U ≫ presheaf.first_map (presieve_of_covering U) F = - left_res F U ≫ pi_inters_to_second_obj F U := -begin - ext ⟨f, g⟩, - dunfold pi_opens_to_first_obj presheaf.first_map left_res pi_inters_to_second_obj, - rw [category.assoc, category.assoc, limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app, - ← category.assoc, ← category.assoc, limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app, - category.assoc, category.assoc, ← F.map_comp, ← F.map_comp], - refl, -end - -lemma pi_opens_to_first_obj_comp_second_map_eq : - pi_opens_to_first_obj F U ≫ presheaf.second_map (presieve_of_covering U) F = - right_res F U ≫ pi_inters_to_second_obj F U := -begin - ext ⟨f, g⟩, - dunfold pi_opens_to_first_obj presheaf.second_map right_res pi_inters_to_second_obj, - rw [category.assoc, category.assoc, limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app, - ← category.assoc, ← category.assoc, limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app, - category.assoc, category.assoc, ← F.map_comp, ← F.map_comp], - refl, -end - -lemma fork_map_comp_first_map_to_pi_opens_eq : - presheaf.fork_map (presieve_of_covering U) F ≫ first_obj_to_pi_opens F U = res F U := -begin - ext i, - dsimp [presheaf.fork_map, first_obj_to_pi_opens, res], - rw [category.assoc, limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app, - limit.lift_π, fan.mk_π_app], - refl, -end - -lemma res_comp_pi_opens_to_first_obj_eq : - res F U ≫ pi_opens_to_first_obj F U = presheaf.fork_map (presieve_of_covering U) F := -begin - ext f, - dunfold res pi_opens_to_first_obj presheaf.fork_map, - rw [category.assoc, limit.lift_π, fan.mk_π_app, limit.lift_π, fan.mk_π_app, ← category.assoc, - limit.lift_π, fan.mk_π_app, ← F.map_comp], - congr, -end - end presieve_of_covering -open presieve_of_covering - -lemma is_sheaf_equalizer_products_of_is_sheaf - (Fsh : F.is_sheaf) : - F.is_sheaf_equalizer_products := -begin - intros ι U, - delta is_sheaf at Fsh, - rw presheaf.is_sheaf_iff_is_sheaf' at Fsh, - -- We know that the sites diagram for `presieve_of_covering U` is a limit fork - obtain ⟨h_limit⟩ := Fsh (supr U) (presieve_of_covering U) - (presieve_of_covering.mem_grothendieck_topology U), - refine ⟨fork.is_limit.mk' _ _⟩, - -- Here, we are given an arbitrary fork of the spaces diagram and need to show that it factors - -- uniquely through our limit fork. - intro s, - -- Composing `s.ι` with `pi_opens_to_first_obj F U` gives a fork of the sites diagram, which - -- must factor through `presheaf.fork_map`. - obtain ⟨l, hl⟩ := fork.is_limit.lift' h_limit (s.ι ≫ pi_opens_to_first_obj F U) _, - swap, - { rw [category.assoc, category.assoc, pi_opens_to_first_obj_comp_fist_map_eq, - pi_opens_to_first_obj_comp_second_map_eq, ← category.assoc, ← category.assoc, s.condition] }, - -- We claim that `l` also gives a factorization of `s.ι` - refine ⟨l, _, _⟩, - { rw [← fork_ι_comp_pi_opens_to_first_obj_to_pi_opens_eq F U s, ← category.assoc, ← hl, - category.assoc, fork.ι_of_ι, fork_map_comp_first_map_to_pi_opens_eq], refl }, - { intros m hm, - apply fork.is_limit.hom_ext h_limit, - rw [hl, fork.ι_of_ι], - simp_rw ← res_comp_pi_opens_to_first_obj_eq, - erw [← category.assoc, hm], }, -end - -lemma is_sheaf_iff_is_sheaf_equalizer_products : - F.is_sheaf ↔ F.is_sheaf_equalizer_products := -iff.intro (is_sheaf_equalizer_products_of_is_sheaf F) (is_sheaf_of_is_sheaf_equalizer_products F) - end Top.presheaf namespace Top.opens -open category_theory topological_space - variables {X : Top} {ι : Type*} lemma cover_dense_iff_is_basis [category ι] (B : ι ⥤ opens X) : @@ -484,7 +143,7 @@ end Top.opens section open_embedding -open category_theory topological_space Top.presheaf opposite +open Top.presheaf opposite variables {C : Type u} [category.{v} C] variables {X Y : Top.{w}} {f : X ⟶ Y} {F : Y.presheaf C} @@ -517,7 +176,7 @@ end open_embedding namespace Top.sheaf -open category_theory topological_space Top opposite +open Top opposite variables {C : Type u} [category.{v} C] variables {X : Top.{w}} {ι : Type*} {B : ι → opens X}