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

• CategoryTheory.CoverPreserving: a functor between sites is cover-preserving if it pushes covering sieves to covering sieves
• CategoryTheory.CompatiblePreserving: a functor between sites is compatible-preserving if it pushes compatible families of elements to compatible families.

Main results

• CategoryTheory.isContinuous_of_coverPreserving: If G : C ⥤ D is cover-preserving and compatible-preserving, then G is a continuous functor, i.e. G.op ⋙ - as a functor (Dᵒᵖ ⥤ A) ⥤ (Cᵒᵖ ⥤ A) of presheaves maps sheaves to sheaves.

References

• [Joh02]: Sketches of an Elephant, P. T. Johnstone: C2.3.
• https://stacks.math.columbia.edu/tag/00WU

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

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.

• cover_preserve {U : C} {S : Sieve U} : S ∈ J U → Sieve.functorPushforward G S ∈ K (G.obj U)

theorem CategoryTheory.idCoverPreserving {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) : CoverPreserving J J (Functor.id C)

The identity functor on a site is cover-preserving.

theorem CategoryTheory.CoverPreserving.comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A : Type u₃} [Category.{v₃, u₃} 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) : CoverPreserving J L (F.comp G)

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

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

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.

• compatible (ℱ : Sheaf K (Type w)) {Z : C} {T : Presieve Z} {x : Presieve.FamilyOfElements (G.op.comp ℱ.val) T} : x.Compatible → ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂), CategoryStruct.comp f₁ (G.map g₁) = CategoryStruct.comp f₂ (G.map g₂) → ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.functorPushforward {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {K : GrothendieckTopology D} {G : Functor C D} (hG : CompatiblePreserving K G) (ℱ : Sheaf K (Type w)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op.comp ℱ.val) T} (h : x.Compatible) : (FamilyOfElements.functorPushforward G x).Compatible

CompatiblePreserving functors indeed preserve compatible families.

@[simp]

theorem CategoryTheory.CompatiblePreserving.apply_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} 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 : Y ⟶ Z} (hf : T f) : Presieve.FamilyOfElements.functorPushforward G x (G.map f) ⋯ = x f hf

theorem CategoryTheory.compatiblePreservingOfFlat {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₁} [Category.{v₁, u₁} D] (K : GrothendieckTopology D) (G : Functor C D) [RepresentablyFlat G] : CompatiblePreserving K G

theorem CategoryTheory.compatiblePreservingOfDownwardsClosed {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (F : Functor C D) [F.Full] [F.Faithful] (hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)) : CompatiblePreserving K F

theorem CategoryTheory.Functor.isContinuous_of_coverPreserving {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {J : GrothendieckTopology C} {K : GrothendieckTopology D} (hF₁ : CompatiblePreserving K F) (hF₂ : CoverPreserving J K F) : F.IsContinuous J K

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

This result is basically https://stacks.math.columbia.edu/tag/00WW.