Cover-preserving and continuous functors between sites.

We define the notion of continuous functor between sites: these are functors G such that the precomposition with G.op preserves sheaves of types (and actually sheaves in any category).

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.Functor.IsContinuous: a functor between sites is continuous if the precomposition with this functor preserves sheaves.
• 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.
• CategoryTheory.Functor.sheafPushforwardContinuous: the induced functor Sheaf K A ⥤ Sheaf J A for a continuous functor G : (C, J) ⥤ (D, K). In case this is part of a morphism of sites, this would be understood as the pushforward functor even though it goes in the opposite direction as the functor G.

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

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

structure CategoryTheory.CoverPreserving {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.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 : CategoryTheory.Sieve U}, S ∈ J.sieves U → CategoryTheory.Sieve.functorPushforward G S ∈ K.sieves (G.toPrefunctor.obj U)

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

The identity functor on a site is cover-preserving.

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

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

structure CategoryTheory.CompatiblePreserving {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.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 : ∀ (ℱ : CategoryTheory.SheafOfTypes K) {Z : C} {T : CategoryTheory.Presieve Z} {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp G.op ℱ.val) T}, CategoryTheory.Presieve.FamilyOfElements.Compatible x → ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.toPrefunctor.obj Y₁) (f₂ : X ⟶ G.toPrefunctor.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂), CategoryTheory.CategoryStruct.comp f₁ (G.toPrefunctor.map g₁) = CategoryTheory.CategoryStruct.comp f₂ (G.toPrefunctor.map g₂) → ℱ.val.toPrefunctor.map f₁.op (x g₁ hg₁) = ℱ.val.toPrefunctor.map f₂.op (x g₂ hg₂)

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

CompatiblePreserving functors indeed preserve compatible families.

@[simp]

theorem CategoryTheory.CompatiblePreserving.apply_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {G : CategoryTheory.Functor C D} (hG : CategoryTheory.CompatiblePreserving K G) (ℱ : CategoryTheory.SheafOfTypes K) {Z : C} {T : CategoryTheory.Presieve Z} {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp G.op ℱ.val) T} (h : CategoryTheory.Presieve.FamilyOfElements.Compatible x) {Y : C} {f : Y ⟶ Z} (hf : T f) : CategoryTheory.Presieve.FamilyOfElements.functorPushforward G x (G.toPrefunctor.map f) (_ : CategoryTheory.Presieve.functorPushforward G T (G.toPrefunctor.map f)) = x f hf

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

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

class CategoryTheory.Functor.IsContinuous {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) : Prop

A functor F is continuous if the precomposition with F.op sends sheaves of Type w to sheaves.

• op_comp_isSheafOfTypes : ∀ (G : CategoryTheory.SheafOfTypes K), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.Functor.comp F.op G.val)

theorem CategoryTheory.Functor.op_comp_isSheafOfTypes {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsContinuous F J K] (G : CategoryTheory.SheafOfTypes K) : CategoryTheory.Presieve.IsSheaf J (CategoryTheory.Functor.comp F.op G.val)

theorem CategoryTheory.Functor.isContinuous_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} (e : F₁ ≅ F₂) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsContinuous F₁ J K] : CategoryTheory.Functor.IsContinuous F₂ J K

instance CategoryTheory.Functor.isContinuous_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Functor.IsContinuous (CategoryTheory.Functor.id C) J J

Equations

• (_ : CategoryTheory.Functor.IsContinuous (CategoryTheory.Functor.id C) J J) = (_ : CategoryTheory.Functor.IsContinuous (CategoryTheory.Functor.id C) J J)

theorem CategoryTheory.Functor.isContinuous_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (F₁ : CategoryTheory.Functor C D) (F₂ : CategoryTheory.Functor D A) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (L : CategoryTheory.GrothendieckTopology A) [CategoryTheory.Functor.IsContinuous F₁ J K] [CategoryTheory.Functor.IsContinuous F₂ K L] : CategoryTheory.Functor.IsContinuous (CategoryTheory.Functor.comp F₁ F₂) J L

theorem CategoryTheory.Functor.isContinuous_comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor D A} {F₁₂ : CategoryTheory.Functor C A} (e : CategoryTheory.Functor.comp F₁ F₂ ≅ F₁₂) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) (L : CategoryTheory.GrothendieckTopology A) [CategoryTheory.Functor.IsContinuous F₁ J K] [CategoryTheory.Functor.IsContinuous F₂ K L] : CategoryTheory.Functor.IsContinuous F₁₂ J L

theorem CategoryTheory.Functor.op_comp_isSheaf {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {A : Type u₃} [CategoryTheory.Category.{v₃, u₃} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsContinuous F J K] (G : CategoryTheory.Sheaf K A) : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.Functor.comp F.op G.val)

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

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

This result is basically .

def CategoryTheory.Functor.sheafPushforwardContinuous {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (A : Type u₃) [CategoryTheory.Category.{v₃, u₃} A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsContinuous F J K] : CategoryTheory.Functor (CategoryTheory.Sheaf K A) (CategoryTheory.Sheaf J A)

The induced functor Sheaf K A ⥤ Sheaf J A given by G.op ⋙ _ if G is a continuous functor.

Equations

• One or more equations did not get rendered due to their size.