Documentation

Mathlib.CategoryTheory.Sites.InducedTopology

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 #

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.

Instances
    @[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 (G.obj X) (CategoryTheory.Sieve.functorPushforward G S)

    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
    Instances For
      @[simp]
      theorem CategoryTheory.Functor.mem_inducedTopology_sieves_iff {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) :
      S (G.inducedTopology K) X CategoryTheory.Sieve.functorPushforward G S K (G.obj X)
      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]
      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]

      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
      Instances For
        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
        Instances For