|
| 1 | +/- |
| 2 | +Copyright (c) 2021 Andrew Yang. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Andrew Yang |
| 5 | +-/ |
| 6 | +import category_theory.sites.dense_subsite |
| 7 | + |
| 8 | +/-! |
| 9 | +# Induced Topology |
| 10 | +
|
| 11 | +We say that a functor `G : C ⥤ (D, K)` is locally dense if for each covering sieve `T` in `D` of |
| 12 | +some `X : C`, `T ∩ mor(C)` generates a covering sieve of `X` in `D`. A locally dense fully faithful |
| 13 | +functor then induces a topology on `C` via `{ T ∩ mor(C) | T ∈ K }`. Note that this is equal to |
| 14 | +the collection of sieves on `C` whose image generates a covering sieve. This construction would |
| 15 | +make `C` both cover-lifting and cover-preserving. |
| 16 | +
|
| 17 | +Some typical examples are full and cover-dense functors (for example the functor from a basis of a |
| 18 | +topological space `X` into `opens X`). The functor `over X ⥤ C` is also locally dense, and the |
| 19 | +induced topology can then be used to construct the big sites associated to a scheme. |
| 20 | +
|
| 21 | +Given a fully faithful cover-dense functor `G : C ⥤ (D, K)` between small sites, we then have |
| 22 | +`Sheaf (H.induced_topology) A ≌ Sheaf K A`. This is known as the comparison lemma. |
| 23 | +
|
| 24 | +## References |
| 25 | +
|
| 26 | +* [Elephant]: *Sketches of an Elephant*, P. T. Johnstone: C2.2. |
| 27 | +* https://ncatlab.org/nlab/show/dense+sub-site |
| 28 | +* https://ncatlab.org/nlab/show/comparison+lemma |
| 29 | +
|
| 30 | +-/ |
| 31 | + |
| 32 | +namespace category_theory |
| 33 | + |
| 34 | +universes v u |
| 35 | + |
| 36 | +open limits opposite presieve |
| 37 | + |
| 38 | +section |
| 39 | + |
| 40 | +variables {C : Type*} [category C] {D : Type*} [category D] {G : C ⥤ D} |
| 41 | +variables {J : grothendieck_topology C} {K : grothendieck_topology D} |
| 42 | +variables (A : Type v) [category.{u} A] |
| 43 | + |
| 44 | +-- variables (A) [full G] [faithful G] |
| 45 | + |
| 46 | +/-- |
| 47 | +We say that a functor `C ⥤ D` into a site is "locally dense" if |
| 48 | +for each covering sieve `T` in `D`, `T ∩ mor(C)` generates a covering sieve in `D`. |
| 49 | +-/ |
| 50 | +def locally_cover_dense (K : grothendieck_topology D) (G : C ⥤ D) : Prop := |
| 51 | +∀ ⦃X⦄ (T : K (G.obj X)), (T.val.functor_pullback G).functor_pushforward G ∈ K (G.obj X) |
| 52 | + |
| 53 | +namespace locally_cover_dense |
| 54 | + |
| 55 | +variables [full G] [faithful G] (Hld : locally_cover_dense K G) |
| 56 | + |
| 57 | +include Hld |
| 58 | + |
| 59 | +lemma pushforward_cover_iff_cover_pullback {X : C} (S : sieve X) : |
| 60 | + K _ (S.functor_pushforward G) ↔ ∃ (T : K (G.obj X)), T.val.functor_pullback G = S := |
| 61 | +begin |
| 62 | + split, |
| 63 | + { intros hS, |
| 64 | + exact ⟨⟨_, hS⟩, (sieve.fully_faithful_functor_galois_coinsertion G X).u_l_eq S⟩ }, |
| 65 | + { rintros ⟨T, rfl⟩, |
| 66 | + exact Hld T } |
| 67 | +end |
| 68 | + |
| 69 | +/-- |
| 70 | +If a functor `G : C ⥤ (D, K)` is fully faithful and locally dense, |
| 71 | +then the set `{ T ∩ mor(C) | T ∈ K }` is a grothendieck topology of `C`. |
| 72 | +-/ |
| 73 | +@[simps] |
| 74 | +def induced_topology : |
| 75 | + grothendieck_topology C := |
| 76 | +{ sieves := λ X S, K _ (S.functor_pushforward G), |
| 77 | + top_mem' := λ X, by { change K _ _, rw sieve.functor_pushforward_top, exact K.top_mem _ }, |
| 78 | + pullback_stable' := λ X Y S f hS, |
| 79 | + begin |
| 80 | + have : S.pullback f = ((S.functor_pushforward G).pullback (G.map f)).functor_pullback G, |
| 81 | + { conv_lhs { rw ← (sieve.fully_faithful_functor_galois_coinsertion G X).u_l_eq S }, |
| 82 | + ext, |
| 83 | + change (S.functor_pushforward G) _ ↔ (S.functor_pushforward G) _, |
| 84 | + rw G.map_comp }, |
| 85 | + rw this, |
| 86 | + change K _ _, |
| 87 | + apply Hld ⟨_, K.pullback_stable (G.map f) hS⟩ |
| 88 | + end, |
| 89 | + transitive' := λ X S hS S' H', |
| 90 | + begin |
| 91 | + apply K.transitive hS, |
| 92 | + rintros Y _ ⟨Z, g, i, hg, rfl⟩, |
| 93 | + rw sieve.pullback_comp, |
| 94 | + apply K.pullback_stable i, |
| 95 | + refine K.superset_covering _ (H' hg), |
| 96 | + rintros W _ ⟨Z', g', i', hg, rfl⟩, |
| 97 | + use ⟨Z', g' ≫ g, i', hg, by simp⟩ |
| 98 | + end } |
| 99 | + |
| 100 | +/-- `G` is cover-lifting wrt the induced topology. -/ |
| 101 | +lemma induced_topology_cover_lifting : |
| 102 | + cover_lifting Hld.induced_topology K G := ⟨λ _ S hS, Hld ⟨S, hS⟩⟩ |
| 103 | + |
| 104 | +/-- `G` is cover-preserving wrt the induced topology. -/ |
| 105 | +lemma induced_topology_cover_preserving : |
| 106 | + cover_preserving Hld.induced_topology K G := ⟨λ _ S hS, hS⟩ |
| 107 | + |
| 108 | +end locally_cover_dense |
| 109 | + |
| 110 | +lemma cover_dense.locally_cover_dense [full G] (H : cover_dense K G) : locally_cover_dense K G := |
| 111 | +begin |
| 112 | + intros X T, |
| 113 | + refine K.superset_covering _ (K.bind_covering T.property (λ Y f Hf, H.is_cover Y)), |
| 114 | + rintros Y _ ⟨Z, _, f, hf, ⟨W, g, f', (rfl : _ = _)⟩, rfl⟩, |
| 115 | + use W, use G.preimage (f' ≫ f), use g, |
| 116 | + split, |
| 117 | + simpa using T.val.downward_closed hf f', |
| 118 | + simp, |
| 119 | +end |
| 120 | + |
| 121 | +/-- |
| 122 | +Given a fully faithful cover-dense functor `G : C ⥤ (D, K)`, we may induce a topology on `C`. |
| 123 | +-/ |
| 124 | +abbreviation cover_dense.induced_topology [full G] [faithful G] (H : cover_dense K G) : |
| 125 | + grothendieck_topology C := H.locally_cover_dense.induced_topology |
| 126 | + |
| 127 | +variable (J) |
| 128 | + |
| 129 | +lemma over_forget_locally_cover_dense (X : C) : locally_cover_dense J (over.forget X) := |
| 130 | +begin |
| 131 | + intros Y T, |
| 132 | + convert T.property, |
| 133 | + ext Z f, |
| 134 | + split, |
| 135 | + { rintros ⟨_, _, g', hg, rfl⟩, |
| 136 | + exact T.val.downward_closed hg g' }, |
| 137 | + { intros hf, |
| 138 | + exact ⟨over.mk (f ≫ Y.hom), over.hom_mk f, 𝟙 _, hf, (category.id_comp _).symm⟩ } |
| 139 | +end |
| 140 | + |
| 141 | +end |
| 142 | + |
| 143 | +section small_site |
| 144 | + |
| 145 | +variables {C : Type v} [small_category C] {D : Type v} [small_category D] {G : C ⥤ D} |
| 146 | +variables {J : grothendieck_topology C} {K : grothendieck_topology D} |
| 147 | +variables (A : Type u) [category.{v} A] |
| 148 | + |
| 149 | +/-- |
| 150 | +Cover-dense functors induces an equivalence of categories of sheaves. |
| 151 | +
|
| 152 | +This is known as the comparison lemma. It requires that the sites are small and the value category |
| 153 | +is complete. |
| 154 | +-/ |
| 155 | +noncomputable |
| 156 | +def cover_dense.Sheaf_equiv [full G] [faithful G] (H : cover_dense K G) [has_limits A] : |
| 157 | + Sheaf H.induced_topology A ≌ Sheaf K A := |
| 158 | +H.Sheaf_equiv_of_cover_preserving_cover_lifting |
| 159 | + H.locally_cover_dense.induced_topology_cover_preserving |
| 160 | + H.locally_cover_dense.induced_topology_cover_lifting |
| 161 | + |
| 162 | +end small_site |
| 163 | + |
| 164 | +end category_theory |
0 commit comments