Induced Topology #
We say that a functor G : C ⥤ (D, K) is locally dense if for each covering sieve T in D of
some X : C, T ∩ mor(C) generates a covering sieve of X in D. A locally dense fully faithful
functor then induces a topology on C via { T ∩ mor(C) | T ∈ K }. Note that this is equal to
the collection of sieves on C whose image generates a covering sieve. This construction would
make C both cover-lifting and cover-preserving.
Some typical examples are full and cover-dense functors (for example the functor from a basis of a
topological space X into Opens X). The functor Over X ⥤ C is also locally dense, and the
induced topology can then be used to construct the big sites associated to a scheme.
Given a fully faithful cover-dense functor G : C ⥤ (D, K) between small sites, we then have
Sheaf (H.inducedTopology) A ≌ Sheaf K A. This is known as the comparison lemma.
References #
- [Joh02]: Sketches of an Elephant, P. T. Johnstone: C2.2.
- https://ncatlab.org/nlab/show/dense+sub-site
- https://ncatlab.org/nlab/show/comparison+lemma
We say that a functor C ⥤ D into a site is "locally dense" if
for each covering sieve T in D, T ∩ mor(C) generates a covering sieve in D.
- functorPushforward_functorPullback_mem ⦃X : C⦄ (T : ↑(K (G.obj X))) : Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ K (G.obj X)
Instances
If G is locally fully faithful and locally cover dense, G is cover-preserving w.r.t. the
restricted topology.
Alias of CategoryTheory.Functor.coverPreserving_restrictedTopology.
If G is locally fully faithful and locally cover dense, G is cover-preserving w.r.t. the
restricted topology.
If a functor G : C ⥤ (D, K) is locally fully faithful and locally dense, S is
a covering in the restricted topology on C if its image generates a K-cover.
Alias of CategoryTheory.Functor.mem_restrictedTopology_iff.
If a functor G : C ⥤ (D, K) is locally fully faithful and locally dense, S is
a covering in the restricted topology on C if its image generates a K-cover.
G is cover-lifting w.r.t. the induced topology.
Cover-dense functors induce an equivalence of categories of sheaves.
This is known as the comparison lemma. It requires that the sites are small and the value category is complete.
Equations
Instances For
Alias of CategoryTheory.Precoverage.toGrothendieck_comap_eq_restrictedTopology.
Alias of CategoryTheory.Precoverage.toGrothendieck_comap_le_restrictedTopology.