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 #

source
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.

Instances
    source
    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)
    source
    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
    source
    @[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)
    source
    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.
    Instances For
      source
      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
      • ⋯ = ⋯
      source
      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.

      source
      @[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
      • ⋯ = ⋯
      source
      @[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
      • ⋯ = ⋯
      source
      @[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
      Instances For
        source
        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
        • ⋯ = ⋯
        source
        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