From 50deb67462964ef665283d17e5a575346c188caa Mon Sep 17 00:00:00 2001 From: justus-springer Date: Mon, 6 Sep 2021 14:26:50 +0000 Subject: [PATCH] refactor(topology/sheaves/sheaf_condition): Generalize unique gluing API (#9002) Previously, the sheaf condition in terms of unique gluings has been defined only for type-valued presheaves. This PR generalizes this to arbitrary concrete categories, whose forgetful functor preserves limits and reflects isomorphisms (e.g. algebraic categories like `CommRing`). As a side effect, this solves a TODO in `structure_sheaf.lean`. Co-authored-by: Johan Commelin --- src/algebraic_geometry/structure_sheaf.lean | 6 +- src/topology/sheaves/local_predicate.lean | 2 +- .../sheaf_condition/equalizer_products.lean | 5 +- .../sheaf_condition/unique_gluing.lean | 222 +++++++++++------- src/topology/sheaves/stalks.lean | 4 +- 5 files changed, 148 insertions(+), 91 deletions(-) diff --git a/src/algebraic_geometry/structure_sheaf.lean b/src/algebraic_geometry/structure_sheaf.lean index 3e08de993ea56..28074fcfb787d 100644 --- a/src/algebraic_geometry/structure_sheaf.lean +++ b/src/algebraic_geometry/structure_sheaf.lean @@ -7,7 +7,6 @@ import algebraic_geometry.prime_spectrum import algebra.category.CommRing.colimits import algebra.category.CommRing.limits import topology.sheaves.local_predicate -import topology.sheaves.forget import ring_theory.localization import ring_theory.subring @@ -756,10 +755,7 @@ begin -- Annoyingly, `sheaf.eq_of_locally_eq` requires an open cover indexed by a *type*, so we need to -- coerce our finset `t` to a type first. let tt := ((t : set (basic_open f)) : Type u), - - -- TODO: Add a version of `eq_of_locally_eq` for sheaves valued in representably concrete - -- categories. This will allow us to write `(structure_sheaf R).eq_of_locally_eq` here. - apply (structure_sheaf_in_Type R).eq_of_locally_eq' + apply (structure_sheaf R).eq_of_locally_eq' (λ i : tt, basic_open (h i)) (basic_open f) (λ i : tt, iDh i), { -- This feels a little redundant, since already have `ht_cover` as a hypothesis -- Unfortunately, `ht_cover` uses a bounded union over the set `t`, while here we have the diff --git a/src/topology/sheaves/local_predicate.lean b/src/topology/sheaves/local_predicate.lean index 55abd2fbe7646..3d18685db34fe 100644 --- a/src/topology/sheaves/local_predicate.lean +++ b/src/topology/sheaves/local_predicate.lean @@ -271,7 +271,7 @@ begin obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective' tV, { -- Decompose everything into its constituent parts: dsimp, - simp only [stalk_to_fiber, colimit.ι_desc_apply] at h, + simp only [stalk_to_fiber, types.colimit.ι_desc_apply] at h, specialize w (unop U) (unop V) fU hU fV hV h, rcases w with ⟨W, iU, iV, w⟩, -- and put it back together again in the correct order. diff --git a/src/topology/sheaves/sheaf_condition/equalizer_products.lean b/src/topology/sheaves/sheaf_condition/equalizer_products.lean index 4b82e762ff70c..d17bd3aafd11f 100644 --- a/src/topology/sheaves/sheaf_condition/equalizer_products.lean +++ b/src/topology/sheaves/sheaf_condition/equalizer_products.lean @@ -8,6 +8,7 @@ import category_theory.limits.punit import category_theory.limits.shapes.products import category_theory.limits.shapes.equalizers import category_theory.full_subcategory +import tactic.elementwise /-! # The sheaf condition in terms of an equalizer of products @@ -67,9 +68,11 @@ 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 := pi.lift (λ i : ι, F.map (topological_space.opens.le_supr U i).op) -@[simp] lemma res_π (i : ι) : res F U ≫ limit.π _ i = F.map (opens.le_supr U i).op := +@[simp, elementwise] +lemma res_π (i : ι) : res F U ≫ limit.π _ i = F.map (opens.le_supr U i).op := by rw [res, limit.lift_π, fan.mk_π_app] +@[elementwise] lemma w : res F U ≫ left_res F U = res F U ≫ right_res F U := begin dsimp [res, left_res, right_res], diff --git a/src/topology/sheaves/sheaf_condition/unique_gluing.lean b/src/topology/sheaves/sheaf_condition/unique_gluing.lean index 6e61f220cfd65..e3dd76baefb72 100644 --- a/src/topology/sheaves/sheaf_condition/unique_gluing.lean +++ b/src/topology/sheaves/sheaf_condition/unique_gluing.lean @@ -3,16 +3,23 @@ Copyright (c) 2021 Justus Springer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Justus Springer -/ +import algebra.category.CommRing.limits +import topology.sheaves.forget import topology.sheaves.sheaf import category_theory.limits.shapes.types import category_theory.types /-! -# The sheaf condition for a type-valued presheaf +# The sheaf condition in terms of unique gluings -We provide an alternative formulation of the sheaf condition for type-valued presheaves. +We provide an alternative formulation of the sheaf condition in terms of unique gluings. -A presheaf `F : presheaf (Type u) X` satisfies the sheaf condition if and only if, for every +We work with sheaves valued in a concrete category `C` admitting all limits, whose forgetful +functor `C ⥤ Type` preserves limits and reflects isomorphisms. The usual categories of algebraic +structures, such as `Mon`, `AddCommGroup`, `Ring`, `CommRing` etc. are all examples of this kind of +category. + +A presheaf `F : presheaf C X` satisfies the sheaf condition if and only if, for every compatible family of sections `sf : Π i : ι, F.obj (op (U i))`, there exists a unique gluing `s : F.obj (op (supr U))`. @@ -21,14 +28,15 @@ and `sf j` to `U i ⊓ U j` agree. A section `s : F.obj (op (supr U))` is a glui family `sf`, if `s` restricts to `sf i` on `U i` for all `i : ι` We show that the sheaf condition in terms of unique gluings is equivalent to the definition -in terms of equalizers. +in terms of equalizers. Our approach is as follows: First, we show them to be equivalent for +`Type`-valued presheaves. Then we use that composing a presheaf with a limit-preserving and +isomorphism-reflecting functor leaves the sheaf condition invariant, as shown in +`topology/sheaves/forget.lean`. -/ noncomputable theory -universe u - open Top open Top.presheaf open Top.presheaf.sheaf_condition_equalizer_products @@ -38,16 +46,19 @@ open topological_space open topological_space.opens open opposite +universes u v + +variables {C : Type u} [category.{v} C] [concrete_category.{v} C] + namespace Top namespace presheaf -variables {X : Top.{u}} (F : presheaf (Type u) X) {ι : Type u} (U : ι → opens X) +section + +local attribute [instance] concrete_category.has_coe_to_sort concrete_category.has_coe_to_fun -@[simp] lemma res_π_apply (i : ι) (s : F.obj (op (supr U))) : - limit.π (discrete.functor (λ i : ι, F.obj (op (U i)))) i (res F U s) = - F.map (opens.le_supr U i).op s := -congr_fun (res_π F U i) s +variables {X : Top.{v}} (F : presheaf C X) {ι : Type v} (U : ι → opens X) /-- A family of sections `sf` is compatible, if the restrictions of `sf i` and `sf j` to `U i ⊓ U j` @@ -57,12 +68,45 @@ def is_compatible (sf : Π i : ι, F.obj (op (U i))) : Prop := ∀ i j : ι, F.map (inf_le_left (U i) (U j)).op (sf i) = F.map (inf_le_right (U i) (U j)).op (sf j) /-- -For presheaves of types, terms of `pi_opens F U` are just families of sections +A section `s` is a gluing for a family of sections `sf` if it restricts to `sf i` on `U i`, +for all `i` +-/ +def is_gluing (sf : Π i : ι, F.obj (op (U i))) (s : F.obj (op (supr U))) : Prop := +∀ i : ι, F.map (opens.le_supr U i).op s = sf i + +/-- +The subtype of all gluings for a given family of sections +-/ +@[nolint has_inhabited_instance] +def gluing (sf : Π i : ι, F.obj (op (U i))) : Type v := +{s : F.obj (op (supr U)) // is_gluing F U sf s} + +/-- +The sheaf condition in terms of unique gluings. A presheaf `F : presheaf C X` satisfies this sheaf +condition if and only if, for every compatible family of sections `sf : Π i : ι, F.obj (op (U i))`, +there exists a unique gluing `s : F.obj (op (supr U))`. + +We prove this to be equivalent to the usual one below in +`sheaf_condition_equiv_sheaf_condition_unique_gluing` +-/ +@[derive subsingleton, nolint has_inhabited_instance] +def sheaf_condition_unique_gluing : Type (v+1) := +Π ⦃ι : Type v⦄ (U : ι → opens X) (sf : Π i : ι, F.obj (op (U i))), + is_compatible F U sf → unique (gluing F U sf) + +end + +section type_valued + +variables {X : Top.{v}} (F : presheaf (Type v) X) {ι : Type v} (U : ι → opens X) + +/-- +For presheaves of types, terms of `pi_opens F U` are just families of sections. -/ def pi_opens_iso_sections_family : pi_opens F U ≅ Π i : ι, F.obj (op (U i)) := - limits.is_limit.cone_point_unique_up_to_iso - (limit.is_limit (discrete.functor (λ i : ι, F.obj (op (U i))))) - ((types.product_limit_cone (λ i : ι, F.obj (op (U i)))).is_limit) +limits.is_limit.cone_point_unique_up_to_iso + (limit.is_limit (discrete.functor (λ i : ι, F.obj (op (U i))))) + ((types.product_limit_cone (λ i : ι, F.obj (op (U i)))).is_limit) /-- Under the isomorphism `pi_opens_iso_sections_family`, compatibility of sections is the same @@ -73,23 +117,16 @@ lemma compatible_iff_left_res_eq_right_res (sf : pi_opens F U) : ↔ left_res F U sf = right_res F U sf := begin split ; intros h, - { ext ⟨i,j⟩, + { ext ⟨i, j⟩, rw [left_res, types.limit.lift_π_apply, fan.mk_π_app, right_res, types.limit.lift_π_apply, fan.mk_π_app], exact h i j, }, { intros i j, convert congr_arg (limits.pi.π (λ p : ι × ι, F.obj (op (U p.1 ⊓ U p.2))) (i,j)) h, - {rw [left_res, types.pi_lift_π_apply], refl}, - {rw [right_res, types.pi_lift_π_apply], refl}, } + { rw [left_res, types.pi_lift_π_apply], refl }, + { rw [right_res, types.pi_lift_π_apply], refl } } end -/-- -A section `s` is a gluing for a family of sections `sf` if it restricts to `sf i` on `U i`, -for all `i` --/ -def is_gluing (sf : Π i : ι, F.obj (op (U i))) (s : F.obj (op (supr U))) : Prop := - ∀ i : ι, F.map (opens.le_supr U i).op s = sf i - /-- Under the isomorphism `pi_opens_iso_sections_family`, being a gluing of a family of sections `sf` is the same as lying in the preimage of `res` (the leftmost arrow of the @@ -105,38 +142,18 @@ begin exact h i, }, { intro i, convert congr_arg (limits.pi.π (λ i : ι, F.obj (op (U i))) i) h, - rw [res, types.pi_lift_π_apply] }, + rw [res, types.pi_lift_π_apply], + refl }, end -/-- -The subtype of all gluings for a given family of sections --/ -@[nolint has_inhabited_instance] -def gluing (sf : Π i : ι, F.obj (op (U i))) : Type u := - {s : F.obj (op (supr U)) // is_gluing F U sf s} - -/-- -The sheaf condition of type-valued presheaves in terms of unique gluings. A presheaf -`F : presheaf (Type u) X` satisfies this sheaf condition if and only if, for every -compatible family of sections `sf : Π i : ι, F.obj (op (U i))`, there exists a unique -gluing `s : F.obj (op (supr U))`. - -We prove this to be equivalent to the usual one below in -`sheaf_condition_equiv_sheaf_condition_unique_gluing` --/ -@[derive subsingleton, nolint has_inhabited_instance] -def sheaf_condition_unique_gluing : Type (u+1) := - Π ⦃ι : Type u⦄ (U : ι → opens X) (sf : Π i : ι, F.obj (op (U i))), - is_compatible F U sf → unique (gluing F U sf) - /-- The "equalizer" sheaf condition can be obtained from the sheaf condition -in terms of unique gluings +in terms of unique gluings. -/ -def sheaf_condition_of_sheaf_condition_unique_gluing : +def sheaf_condition_of_sheaf_condition_unique_gluing_types : F.sheaf_condition_unique_gluing → F.sheaf_condition := λ Fsh ι U, begin - refine fork.is_limit.mk' _ (λ s, ⟨_,_,_⟩) ; dsimp, + refine fork.is_limit.mk' _ (λ s, ⟨_, _, _⟩) ; dsimp, { intro x, refine (Fsh U ((pi_opens_iso_sections_family F U).hom (s.ι x)) _).default.1, apply (compatible_iff_left_res_eq_right_res F U (s.ι x)).mpr, @@ -155,9 +172,9 @@ end /-- The sheaf condition in terms of unique gluings can be obtained from the usual -"equalizer" sheaf condition +"equalizer" sheaf condition. -/ -def sheaf_condition_unique_gluing_of_sheaf_condition : +def sheaf_condition_unique_gluing_of_sheaf_condition_types : F.sheaf_condition → F.sheaf_condition_unique_gluing := λ Fsh ι U sf hsf, { default := begin let sf' := (pi_opens_iso_sections_family F U).inv sf, @@ -187,56 +204,86 @@ def sheaf_condition_unique_gluing_of_sheaf_condition : } /-- -The sheaf condition in terms of unique gluings is equivalent to the usual sheaf condition +For type-valued presheaves, the sheaf condition in terms of unique gluings is equivalent to the +usual sheaf condition in terms of equalizer diagrams. +-/ +def sheaf_condition_equiv_sheaf_condition_unique_gluing_types : + F.sheaf_condition ≃ F.sheaf_condition_unique_gluing := +equiv_of_subsingleton_of_subsingleton + F.sheaf_condition_unique_gluing_of_sheaf_condition_types + F.sheaf_condition_of_sheaf_condition_unique_gluing_types + +end type_valued + +section + +local attribute [instance] concrete_category.has_coe_to_sort concrete_category.has_coe_to_fun + +variables [has_limits C] [reflects_isomorphisms (forget C)] [preserves_limits (forget C)] +variables {X : Top.{v}} (F : presheaf C X) {ι : Type v} (U : ι → opens X) + +/-- +For presheaves valued in a concrete category, whose forgetful functor reflects isomorphisms and +preserves limits, the sheaf condition in terms of unique gluings is equivalent to the usual one in terms of equalizer diagrams. -/ def sheaf_condition_equiv_sheaf_condition_unique_gluing : F.sheaf_condition ≃ F.sheaf_condition_unique_gluing := -equiv_of_subsingleton_of_subsingleton - F.sheaf_condition_unique_gluing_of_sheaf_condition - F.sheaf_condition_of_sheaf_condition_unique_gluing +equiv.trans (sheaf_condition_equiv_sheaf_condition_comp (forget C) F) + (sheaf_condition_equiv_sheaf_condition_unique_gluing_types (F ⋙ forget C)) /-- -A slightly more convenient way of obtaining the sheaf condition for type-valued sheaves +A slightly more convenient way of obtaining the sheaf condition for sheaves of algebraic structures. -/ def sheaf_condition_of_exists_unique_gluing - (h : ∀ ⦃ι : Type u⦄ (U : ι → opens X) (sf : Π i : ι, F.obj (op (U i))), - is_compatible F U sf → ∃! s : F.obj (op (supr U)), is_gluing F U sf s) : + (h : ∀ ⦃ι : Type v⦄ (U : ι → opens X) (sf : Π i : ι, F.obj (op (U i))), + is_compatible F U sf → ∃! s : F.obj (op (supr U)), is_gluing F U sf s) : F.sheaf_condition := -sheaf_condition_of_sheaf_condition_unique_gluing F $ λ ι U sf hsf, -{ default := by { +(sheaf_condition_equiv_sheaf_condition_unique_gluing F).inv_fun $ λ ι U sf hsf, +{ default := begin choose gl gl_spec gl_uniq using h U sf hsf, - exact ⟨gl, gl_spec⟩, }, - uniq := by { + exact ⟨gl, gl_spec⟩ + end, + uniq := begin intro s, let t : F.gluing U sf := _, change s = t, ext, choose gl gl_spec gl_uniq using h U sf hsf, refine eq.trans (gl_uniq s.1 _) (gl_uniq t.1 _).symm, - exacts [s.2, t.2] }, + exacts [s.2, t.2] + end, } -end presheaf +end +end presheaf namespace sheaf + open presheaf open category_theory -variables {X : Top.{u}} (F : sheaf (Type u) X) {ι : Type u} (U : ι → opens X) +section + +local attribute [instance] concrete_category.has_coe_to_sort concrete_category.has_coe_to_fun + +variables [has_limits C] [reflects_isomorphisms (concrete_category.forget C)] +variables [preserves_limits (concrete_category.forget C)] + +variables {X : Top.{v}} (F : sheaf C X) {ι : Type v} (U : ι → opens X) /-- -A more convenient way of obtaining a unique gluing of sections for a sheaf +A more convenient way of obtaining a unique gluing of sections for a sheaf. -/ lemma exists_unique_gluing (sf : Π i : ι, F.presheaf.obj (op (U i))) (h : is_compatible F.presheaf U sf ) : ∃! s : F.presheaf.obj (op (supr U)), is_gluing F.presheaf U sf s := begin - have := (sheaf_condition_unique_gluing_of_sheaf_condition _ F.sheaf_condition U sf h), - refine ⟨this.default.1,this.default.2,_⟩, + have := sheaf_condition_equiv_sheaf_condition_unique_gluing _ F.sheaf_condition U sf h, + refine ⟨this.default.1, this.default.2, _⟩, intros s hs, - exact congr_arg subtype.val (this.uniq ⟨s,hs⟩), + exact congr_arg subtype.val (this.uniq ⟨s, hs⟩), end /-- @@ -249,13 +296,16 @@ lemma exists_unique_gluing' (V : opens X) (iUV : Π i : ι, U i ⟶ V) (hcover : begin have V_eq_supr_U : V = supr U := le_antisymm hcover (supr_le (λ i, (iUV i).le)), obtain ⟨gl, gl_spec, gl_uniq⟩ := F.exists_unique_gluing U sf h, - refine ⟨F.presheaf.map (eq_to_hom V_eq_supr_U).op gl, (λ i,_), (λ gl' gl'_spec,_)⟩, - { rw ← functor_to_types.map_comp_apply, + refine ⟨F.presheaf.map (eq_to_hom V_eq_supr_U).op gl, _, _⟩, + { intro i, + rw [← comp_apply, ← F.presheaf.map_comp], exact gl_spec i }, - { convert congr_arg _ (gl_uniq (F.presheaf.map (eq_to_hom V_eq_supr_U.symm).op gl') (λ i,_)) ; - rw ← functor_to_types.map_comp_apply, - { exact (functor_to_types.map_id_apply _ _).symm }, - { convert gl'_spec i }} + { intros gl' gl'_spec, + convert congr_arg _ (gl_uniq (F.presheaf.map (eq_to_hom V_eq_supr_U.symm).op gl') (λ i,_)) ; + rw [← comp_apply, ← F.presheaf.map_comp], + { rw [eq_to_hom_op, eq_to_hom_op, eq_to_hom_trans, eq_to_hom_refl, + F.presheaf.map_id, id_apply] }, + { convert gl'_spec i } } end @[ext] @@ -263,9 +313,13 @@ lemma eq_of_locally_eq (s t : F.presheaf.obj (op (supr U))) (h : ∀ i, F.presheaf.map (opens.le_supr U i).op s = F.presheaf.map (opens.le_supr U i).op t) : s = t := begin - apply (mono_iff_injective _).mp (mono_of_is_limit_parallel_pair (F.sheaf_condition U)), - ext, - simp only [fork_ι, res_π_apply, h], + let sf : Π i : ι, F.presheaf.obj (op (U i)) := λ i, F.presheaf.map (opens.le_supr U i).op s, + have sf_compatible : is_compatible _ U sf, + { intros i j, simp_rw [← comp_apply, ← F.presheaf.map_comp], refl }, + obtain ⟨gl, -, gl_uniq⟩ := F.exists_unique_gluing U sf sf_compatible, + transitivity gl, + { apply gl_uniq, intro i, refl }, + { symmetry, apply gl_uniq, intro i, rw ← h }, end /-- @@ -280,12 +334,14 @@ begin suffices : F.presheaf.map (eq_to_hom V_eq_supr_U.symm).op s = F.presheaf.map (eq_to_hom V_eq_supr_U.symm).op t, { convert congr_arg (F.presheaf.map (eq_to_hom V_eq_supr_U).op) this ; - rw ← functor_to_types.map_comp_apply ; - exact (functor_to_types.map_id_apply _ _).symm }, + rw [← comp_apply, ← F.presheaf.map_comp, eq_to_hom_op, eq_to_hom_op, eq_to_hom_trans, + eq_to_hom_refl, F.presheaf.map_id, id_apply] }, apply eq_of_locally_eq, intro i, - rw [← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply], - convert h i + rw [← comp_apply, ← comp_apply, ← F.presheaf.map_comp], + convert h i, +end + end end sheaf diff --git a/src/topology/sheaves/stalks.lean b/src/topology/sheaves/stalks.lean index e356c5db063f2..4c6458ba50c01 100644 --- a/src/topology/sheaves/stalks.lean +++ b/src/topology/sheaves/stalks.lean @@ -147,7 +147,7 @@ begin { intros x hxU, rw [subtype.val_eq_coe, opens.mem_coe, opens.mem_supr], exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩ }, - { intro x, + { intro x, dsimp, rw [heq, subsingleton.elim (i₁ x) (i₂ x)] } end @@ -218,6 +218,7 @@ begin { use s, apply G.eq_of_locally_eq' V U iVU V_cover, intro x, + dsimp at ⊢ s_spec, rw [← functor_to_types.naturality, s_spec, heq] }, { intros x y, -- What's left to show here is that the secions `sf` are compatible, i.e. they agree on @@ -227,6 +228,7 @@ begin -- Here, we need to use injectivity of the stalk maps. apply (h z).1, erw [stalk_functor_map_germ_apply, stalk_functor_map_germ_apply], + dsimp, rw [functor_to_types.naturality, functor_to_types.naturality, heq, heq, ← functor_to_types.map_comp_apply, ← functor_to_types.map_comp_apply], refl } },