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} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor 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

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.LocallyCoverDense.pushforward_cover_iff_cover_pullback {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] (Hld : CategoryTheory.LocallyCoverDense K G) {X : C} (S : CategoryTheory.Sieve X) : K.sieves (G.toPrefunctor.obj X) (CategoryTheory.Sieve.functorPushforward G S) ↔ ∃ (T : ↑(K.sieves (G.toPrefunctor.obj X))), CategoryTheory.Sieve.functorPullback G ↑T = S

@[simp]

theorem CategoryTheory.LocallyCoverDense.inducedTopology_sieves {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] (Hld : CategoryTheory.LocallyCoverDense K G) (X : C) (S : CategoryTheory.Sieve X) : (CategoryTheory.LocallyCoverDense.inducedTopology Hld).sieves X S = K.sieves (G.toPrefunctor.obj X) (CategoryTheory.Sieve.functorPushforward G S)

def CategoryTheory.LocallyCoverDense.inducedTopology {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] (Hld : CategoryTheory.LocallyCoverDense K G) : CategoryTheory.GrothendieckTopology 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

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.LocallyCoverDense.inducedTopology_isCocontinuous {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] (Hld : CategoryTheory.LocallyCoverDense K G) : CategoryTheory.Functor.IsCocontinuous G (CategoryTheory.LocallyCoverDense.inducedTopology Hld) K

G is cover-lifting wrt the induced topology.

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

G is cover-preserving wrt the induced topology.

theorem CategoryTheory.Functor.locallyCoverDense_of_isCoverDense {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Full G] [CategoryTheory.Functor.IsCoverDense G K] : CategoryTheory.LocallyCoverDense K G

@[inline, reducible]

abbrev CategoryTheory.Functor.inducedTopologyOfIsCoverDense {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Full G] [CategoryTheory.Faithful G] [CategoryTheory.Functor.IsCoverDense G K] : CategoryTheory.GrothendieckTopology C

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

Equations

• CategoryTheory.Functor.inducedTopologyOfIsCoverDense G K = CategoryTheory.LocallyCoverDense.inducedTopology (_ : CategoryTheory.LocallyCoverDense K G)

theorem CategoryTheory.over_forget_locallyCoverDense {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : CategoryTheory.LocallyCoverDense J (CategoryTheory.Over.forget X)

instance CategoryTheory.instIsContinuousInducedTopologyOfIsCoverDense {C : Type v} [CategoryTheory.SmallCategory C] {D : Type v} [CategoryTheory.SmallCategory D] {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] [CategoryTheory.Functor.IsCoverDense G K] : CategoryTheory.Functor.IsContinuous G (CategoryTheory.Functor.inducedTopologyOfIsCoverDense G K) K

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instIsCocontinuousInducedTopologyOfIsCoverDense {C : Type v} [CategoryTheory.SmallCategory C] {D : Type v} [CategoryTheory.SmallCategory D] {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Full G] [CategoryTheory.Faithful G] [CategoryTheory.Functor.IsCoverDense G K] : CategoryTheory.Functor.IsCocontinuous G (CategoryTheory.Functor.inducedTopologyOfIsCoverDense G K) K

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense {C : Type v} [CategoryTheory.SmallCategory C] {D : Type v} [CategoryTheory.SmallCategory D] {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Full G] [CategoryTheory.Faithful G] [CategoryTheory.Functor.IsCoverDense G K] [CategoryTheory.Limits.HasLimits A] : CategoryTheory.Sheaf (CategoryTheory.Functor.inducedTopologyOfIsCoverDense G K) A ≌ CategoryTheory.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

• One or more equations did not get rendered due to their size.