mathlib3 documentation

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 #

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

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
@[reducible]

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

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