# mathlib3documentation

category_theory.sites.induced_topology

# Induced Topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.induced_topology) A ≌ Sheaf K A. This is known as the comparison lemma.

## References #

def category_theory.locally_cover_dense {C : Type u_1} {D : Type u_3} (G : C D) :
Prop

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
theorem category_theory.locally_cover_dense.pushforward_cover_iff_cover_pullback {C : Type u_1} {D : Type u_3} {G : C D} (Hld : G) {X : C} (S : category_theory.sieve X) :
K (G.obj X) (T : (K (G.obj X))),
def category_theory.locally_cover_dense.induced_topology {C : Type u_1} {D : Type u_3} {G : C D} (Hld : G) :

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
@[simp]
theorem category_theory.locally_cover_dense.induced_topology_sieves {C : Type u_1} {D : Type u_3} {G : C D} (Hld : G) (X : C) (S : category_theory.sieve X) :
(Hld.induced_topology) X S = K (G.obj X)
theorem category_theory.locally_cover_dense.induced_topology_cover_lifting {C : Type u_1} {D : Type u_3} {G : C D} (Hld : G) :

G is cover-lifting wrt the induced topology.

theorem category_theory.locally_cover_dense.induced_topology_cover_preserving {C : Type u_1} {D : Type u_3} {G : C D} (Hld : G) :

G is cover-preserving wrt the induced topology.

theorem category_theory.cover_dense.locally_cover_dense {C : Type u_1} {D : Type u_3} {G : C D} (H : G) :
@[reducible]
def category_theory.cover_dense.induced_topology {C : Type u_1} {D : Type u_3} {G : C D} (H : G) :

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

noncomputable def category_theory.cover_dense.Sheaf_equiv {C : Type v} {D : Type v} {G : C D} (A : Type u) (H : G)  :

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