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 #

source
def category_theory.locally_cover_dense {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] (K : category_theory.grothendieck_topology D) (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
source
theorem category_theory.locally_cover_dense.pushforward_cover_iff_cover_pullback {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {G : C ⥤ D} {K : category_theory.grothendieck_topology D} [category_theory.full G] [category_theory.faithful G] (Hld : category_theory.locally_cover_dense K G) {X : C} (S : category_theory.sieve X) :
⇑K (G.obj X) (category_theory.sieve.functor_pushforward G S) ↔ ∃ (T : ↥(⇑K (G.obj X))), category_theory.sieve.functor_pullback G T.val = S
source
def category_theory.locally_cover_dense.induced_topology {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {G : C ⥤ D} {K : category_theory.grothendieck_topology D} [category_theory.full G] [category_theory.faithful G] (Hld : category_theory.locally_cover_dense K G) :
category_theory.grothendieck_topology C

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

G is cover-lifting wrt the induced topology.

source
theorem category_theory.locally_cover_dense.induced_topology_cover_preserving {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {G : C ⥤ D} {K : category_theory.grothendieck_topology D} [category_theory.full G] [category_theory.faithful G] (Hld : category_theory.locally_cover_dense K G) :
category_theory.cover_preserving Hld.induced_topology K G

G is cover-preserving wrt the induced topology.

source
theorem category_theory.cover_dense.locally_cover_dense {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {G : C ⥤ D} {K : category_theory.grothendieck_topology D} [category_theory.full G] (H : category_theory.cover_dense K G) :
category_theory.locally_cover_dense K G
source
@[reducible]
def category_theory.cover_dense.induced_topology {C : Type u_1} [category_theory.category C] {D : Type u_3} [category_theory.category D] {G : C ⥤ D} {K : category_theory.grothendieck_topology D} [category_theory.full G] [category_theory.faithful G] (H : category_theory.cover_dense K G) :
category_theory.grothendieck_topology C

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

source
theorem category_theory.over_forget_locally_cover_dense {C : Type u_1} [category_theory.category C] (J : category_theory.grothendieck_topology C) (X : C) :
category_theory.locally_cover_dense J (category_theory.over.forget X)
source
noncomputable def category_theory.cover_dense.Sheaf_equiv {C : Type v} [category_theory.small_category C] {D : Type v} [category_theory.small_category D] {G : C ⥤ D} {K : category_theory.grothendieck_topology D} (A : Type u) [category_theory.category A] [category_theory.full G] [category_theory.faithful G] (H : category_theory.cover_dense K G) [category_theory.limits.has_limits A] :
category_theory.Sheaf H.induced_topology A ≌ category_theory.Sheaf 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