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

class CategoryTheory.Functor.LocallyCoverDense {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) : 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.

• functorPushforward_functorPullback_mem : ∀ ⦃X : C⦄ (T : ↑(K.sieves (G.obj X))), CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ K.sieves (G.obj X)

theorem CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_mem {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} [self : G.LocallyCoverDense K] ⦃X : C⦄ (T : ↑(K.sieves (G.obj X))) : CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPullback G ↑T) ∈ K.sieves (G.obj X)

theorem CategoryTheory.Functor.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) [G.LocallyCoverDense K] [G.Full] [G.Faithful] {X : C} (S : CategoryTheory.Sieve X) : K.sieves (G.obj X) (CategoryTheory.Sieve.functorPushforward G S) ↔ ∃ (T : ↑(K.sieves (G.obj X))), CategoryTheory.Sieve.functorPullback G ↑T = S

@[simp]

theorem CategoryTheory.Functor.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) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] (X : C) (S : CategoryTheory.Sieve X) : (G.inducedTopology K).sieves X S = K.sieves (G.obj X) (CategoryTheory.Sieve.functorPushforward G S)

def CategoryTheory.Functor.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) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] : 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.

instance CategoryTheory.Functor.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) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] : G.IsCocontinuous (G.inducedTopology K) K

G is cover-lifting wrt the induced topology.

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.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) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] : CategoryTheory.CoverPreserving (G.inducedTopology K) K G

G is cover-preserving wrt the induced topology.

@[instance 900]

instance 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) [G.IsLocallyFull K] [G.IsCoverDense K] : G.LocallyCoverDense K

Equations

• ⋯ = ⋯

@[instance 900]

instance CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense {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) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] [G.IsCoverDense K] : CategoryTheory.Functor.IsDenseSubsite (G.inducedTopology K) K G

Equations

• ⋯ = ⋯

@[deprecated CategoryTheory.Functor.inducedTopology]

def 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) [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] : CategoryTheory.GrothendieckTopology C

Alias of CategoryTheory.Functor.inducedTopology.

---

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

• @CategoryTheory.Functor.inducedTopologyOfIsCoverDense = @CategoryTheory.Functor.inducedTopology

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense {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) (A : Type v) [CategoryTheory.Category.{u, v} A] [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K] [G.IsCoverDense K] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] : CategoryTheory.Sheaf (G.inducedTopology 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

• G.sheafInducedTopologyEquivOfIsCoverDense K A = CategoryTheory.Functor.IsDenseSubsite.sheafEquiv G (G.inducedTopology K) K A