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))), CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ K (G.obj X)
Instances
If a functor G : C ⥤ (D, K)
is fully faithful and locally dense,
then the set { T ∩ mor(C) | T ∈ K }
is a grothendieck topology of C
.
Equations
- G.inducedTopology K = { sieves := fun (X : C) (S : CategoryTheory.Sieve X) => K (G.obj X) (CategoryTheory.Sieve.functorPushforward G S), top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }
Instances For
G
is cover-lifting wrt the induced topology.
Equations
- ⋯ = ⋯
G
is cover-preserving wrt the induced topology.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Alias of CategoryTheory.Functor.inducedTopology
.
If a functor G : C ⥤ (D, K)
is fully faithful and locally dense,
then the set { T ∩ mor(C) | T ∈ K }
is a grothendieck topology of C
.
Equations
Instances For
Equations
- ⋯ = ⋯
Cover-dense functors induces 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
- G.sheafInducedTopologyEquivOfIsCoverDense K A = CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G (G.inducedTopology K) K A