Documentation

Mathlib.CategoryTheory.Sites.CoverPreserving

Cover-preserving functors between sites. #

In order to show that a functor is continuous, we define cover-preserving functors between sites as functors that push covering sieves to covering sieves. Then, a cover-preserving and compatible-preserving functor is continuous.

Main definitions #

Main results #

References #

structure CategoryTheory.CoverPreserving {C : Type u₁} [Category C] {D : Type u₂} [Category D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : Functor C D) :

A functor G : (C, J) ⥤ (D, K) between sites is cover-preserving if for all covering sieves R in C, R.functorPushforward G is a covering sieve in D.

Instances For

    The identity functor on a site is cover-preserving.

    theorem CategoryTheory.CoverPreserving.comp {C : Type u₁} [Category C] {D : Type u₂} [Category D] {A : Type u₃} [Category A] (J : GrothendieckTopology C) (K : GrothendieckTopology D) {L : GrothendieckTopology A} {F : Functor C D} (hF : CoverPreserving J K F) {G : Functor D A} (hG : CoverPreserving K L G) :

    The composition of two cover-preserving functors is cover-preserving.

    structure CategoryTheory.CompatiblePreserving {C : Type u₁} [Category C] {D : Type u₂} [Category D] (K : GrothendieckTopology D) (G : Functor C D) :

    A functor G : (C, J) ⥤ (D, K) between sites is called compatible preserving if for each compatible family of elements at C and valued in G.op ⋙ ℱ, and each commuting diagram f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂, x g₁ and x g₂ coincide when restricted via fᵢ. This is actually stronger than merely preserving compatible families because of the definition of functorPushforward used.

    Instances For

      CompatiblePreserving functors indeed preserve compatible families.

      theorem CategoryTheory.CompatiblePreserving.apply_map {C : Type u₁} [Category C] {D : Type u₂} [Category D] {K : GrothendieckTopology D} {G : Functor C D} (hG : CompatiblePreserving K G) ( : Sheaf K (Type w)) {Z : C} {T : Presieve Z} {x : Presieve.FamilyOfElements (G.op.comp .val) T} (h : x.Compatible) {Y : C} {f : Quiver.Hom Y Z} (hf : T f) :
      theorem CategoryTheory.compatiblePreservingOfDownwardsClosed {C : Type u₁} [Category C] {D : Type u₂} [Category D] (K : GrothendieckTopology D) (F : Functor C D) [F.Full] [F.Faithful] (hF : {c : C} → {d : D} → Quiver.Hom d (F.obj c)(c' : C) × Iso (F.obj c') d) :

      If F is cover-preserving and compatible-preserving, then F is a continuous functor.

      Stacks Tag 00WW (This is basically this Stacks entry.)