# 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 #

• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.2.
• https://ncatlab.org/nlab/show/dense+sub-site
• https://ncatlab.org/nlab/show/comparison+lemma
def CategoryTheory.LocallyCoverDense {C : Type u_1} [] {D : Type u_2} [] (G : ) :

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.

Equations
• = ∀ ⦃X : C⦄ (T : (K.sieves (G.obj X))), K.sieves (G.obj X)
Instances For
theorem CategoryTheory.LocallyCoverDense.pushforward_cover_iff_cover_pullback {C : Type u_1} [] {D : Type u_2} [] {G : } [G.Full] [G.Faithful] (Hld : ) {X : C} (S : ) :
K.sieves (G.obj X) ∃ (T : (K.sieves (G.obj X))),
@[simp]
theorem CategoryTheory.LocallyCoverDense.inducedTopology_sieves {C : Type u_1} [] {D : Type u_2} [] {G : } [G.Full] [G.Faithful] (Hld : ) (X : C) (S : ) :
Hld.inducedTopology.sieves X S = K.sieves (G.obj X)
def CategoryTheory.LocallyCoverDense.inducedTopology {C : Type u_1} [] {D : Type u_2} [] {G : } [G.Full] [G.Faithful] (Hld : ) :

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
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.LocallyCoverDense.inducedTopology_isCocontinuous {C : Type u_1} [] {D : Type u_2} [] {G : } [G.Full] [G.Faithful] (Hld : ) :
G.IsCocontinuous Hld.inducedTopology K

G is cover-lifting wrt the induced topology.

theorem CategoryTheory.LocallyCoverDense.inducedTopology_coverPreserving {C : Type u_1} [] {D : Type u_2} [] {G : } [G.Full] [G.Faithful] (Hld : ) :
CategoryTheory.CoverPreserving Hld.inducedTopology K G

G is cover-preserving wrt the induced topology.

theorem CategoryTheory.Functor.locallyCoverDense_of_isCoverDense {C : Type u_1} [] {D : Type u_2} [] (G : ) [G.Full] [G.IsCoverDense K] :
@[reducible, inline]
abbrev CategoryTheory.Functor.inducedTopologyOfIsCoverDense {C : Type u_1} [] {D : Type u_2} [] (G : ) [G.Full] [G.Faithful] [G.IsCoverDense K] :

Given a fully faithful cover-dense functor G : C ⥤ (D, K), we may induce a topology on C.

Equations
• G.inducedTopologyOfIsCoverDense K = .inducedTopology
Instances For
instance CategoryTheory.instIsContinuousInducedTopologyOfIsCoverDense {C : Type v} {D : Type v} {G : } [G.Full] [G.Faithful] [G.IsCoverDense K] :
G.IsContinuous (G.inducedTopologyOfIsCoverDense K) K
Equations
• =
instance CategoryTheory.instIsCocontinuousInducedTopologyOfIsCoverDense {C : Type v} {D : Type v} {G : } [G.Full] [G.Faithful] [G.IsCoverDense K] :
G.IsCocontinuous (G.inducedTopologyOfIsCoverDense K) K
Equations
• =
noncomputable def CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense {C : Type v} {D : Type v} {G : } (A : Type u) [G.Full] [G.Faithful] [G.IsCoverDense K] :
CategoryTheory.Sheaf (G.inducedTopologyOfIsCoverDense K) A

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
Instances For