Cocontinuous functors between sites.

We define cocontinuous functors between sites as functors that pull covering sieves back to covering sieves. This concept is also known as cover-lifting or cover-reflecting functors. We use the original terminology and definition of SGA 4 III 2.1. However, the notion of cocontinuous functor should not be confused with the general definition of cocontinuous functors between categories as functors preserving small colimits.

Main definitions

• CategoryTheory.Functor.IsCocontinuous: a functor between sites is cocontinuous if it pulls back covering sieves to covering sieves
• CategoryTheory.Functor.sheafPushforwardCocontinuous: A cocontinuous functor G : (C, J) ⥤ (D, K) induces a functor Sheaf J A ⥤ Sheaf K A.

Main results

• CategoryTheory.ran_isSheaf_of_isCocontinuous: If G : C ⥤ D is cocontinuous, then Ran G.op (ₚu) as a functor (Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A) of presheaves maps sheaves to sheaves.
• CategoryTheory.Sites.pullbackCopullbackAdjunction: If G : (C, J) ⥤ (D, K) is cocontinuous and continuous, then G.sheafPushforwardContinuous A J K and G.sheafPushforwardCocontinuous A J K are adjoint.

References

• [Elephant]: Sketches of an Elephant, P. T. Johnstone: C2.3.
• [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]
• https://stacks.math.columbia.edu/tag/00XI

class CategoryTheory.Functor.IsCocontinuous {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) : Prop

A functor G : (C, J) ⥤ (D, K) between sites is called cocontinuous (SGA 4 III 2.1) if for all covering sieves R in D, R.pullback G is a covering sieve in C.

• cover_lift : ∀ {U : C} {S : CategoryTheory.Sieve (G.toPrefunctor.obj U)}, S ∈ K.sieves (G.toPrefunctor.obj U) → CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U

theorem CategoryTheory.Functor.cover_lift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] (G : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsCocontinuous G J K] {U : C} {S : CategoryTheory.Sieve (G.toPrefunctor.obj U)} (hS : S ∈ K.sieves (G.toPrefunctor.obj U)) : CategoryTheory.Sieve.functorPullback G S ∈ J.sieves U

instance CategoryTheory.isCocontinuous_id {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Functor.IsCocontinuous (CategoryTheory.Functor.id C) J J

The identity functor on a site is cocontinuous.

Equations

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

theorem CategoryTheory.isCocontinuous_comp {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_5, u_2} D] {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (G : CategoryTheory.Functor C D) (G' : CategoryTheory.Functor D E) (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) {L : CategoryTheory.GrothendieckTopology E} [CategoryTheory.Functor.IsCocontinuous G J K] [CategoryTheory.Functor.IsCocontinuous G' K L] : CategoryTheory.Functor.IsCocontinuous (CategoryTheory.Functor.comp G G') J L

The composition of two cocontinuous functors is cocontinuous.

We will now prove that Ran G.op (ₚu) maps sheaves to sheaves if G is cocontinuous (SGA 4 III 2.2). This can also be be found in . However, the proof given there uses the amalgamation definition of sheaves, and thus does not require that C or D has categorical pullbacks.

For the following proof sketch, ⊆ denotes the homs on C and D as in the topological analogy. By definition, the presheaf 𝒢 : Dᵒᵖ ⥤ A is a sheaf if for every sieve S of U : D, and every compatible family of morphisms X ⟶ 𝒢(V) for each V ⊆ U : S with a fixed source X, we can glue them into a morphism X ⟶ 𝒢(U).

Since the presheaf 𝒢 := (Ran G.op).obj ℱ.val is defined via 𝒢(U) = lim_{G(V) ⊆ U} ℱ(V), for gluing the family x into a X ⟶ 𝒢(U), it suffices to provide a X ⟶ ℱ(Y) for each G(Y) ⊆ U. This can be done since { Y' ⊆ Y : G(Y') ⊆ U ∈ S} is a covering sieve for Y on C (by the cocontinuity G). Thus the morphisms X ⟶ 𝒢(G(Y')) ⟶ ℱ(Y') can be glued into a morphism X ⟶ ℱ(Y). This is done in get_sections.

In glued_limit_cone, we verify these obtained sections are indeed compatible, and thus we obtain A X ⟶ 𝒢(U). The remaining work is to verify that this is indeed the amalgamation and is unique.

instance CategoryTheory.RanIsSheafOfIsCocontinuous.instHasLimitsOfShapeStructuredArrowOppositeOppositeOpInstCategoryStructuredArrow {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (X : Dᵒᵖ) : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A

Equations

• (_ : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A) = (_ : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A)

def CategoryTheory.RanIsSheafOfIsCocontinuous.pulledbackFamily {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} (S : CategoryTheory.Sieve U) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows) (Y : CategoryTheory.StructuredArrow (Opposite.op U) G.op) : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) (CategoryTheory.Presieve.functorPullback G (CategoryTheory.Sieve.pullback Y.hom.unop S).arrows)

The family of morphisms X ⟶ 𝒢(G(Y')) ⟶ ℱ(Y') defined on { Y' ⊆ Y : G(Y') ⊆ U ∈ S}.

Equations

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

@[simp]

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.pulledbackFamily_apply {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} (S : CategoryTheory.Sieve U) (x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows) (Y : CategoryTheory.StructuredArrow (Opposite.op U) G.op) {W : C} {f : W ⟶ Y.right.unop} (Hf : CategoryTheory.Presieve.functorPullback G (CategoryTheory.Sieve.pullback Y.hom.unop S).arrows f) : CategoryTheory.RanIsSheafOfIsCocontinuous.pulledbackFamily ℱ S x Y f Hf = CategoryTheory.CategoryStruct.comp (x (CategoryTheory.CategoryStruct.comp (G.toPrefunctor.map f) Y.hom.unop) Hf) (((CategoryTheory.Ran.adjunction A G.op).counit.app ℱ.val).app (Opposite.op W))

def CategoryTheory.RanIsSheafOfIsCocontinuous.getSection {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) (Y : CategoryTheory.StructuredArrow (Opposite.op U) G.op) : X ⟶ ℱ.val.toPrefunctor.obj Y.right

Given a G(Y) ⊆ U, we can find a unique section X ⟶ ℱ(Y) that agrees with x.

Equations

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

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.getSection_isAmalgamation {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) (Y : CategoryTheory.StructuredArrow (Opposite.op U) G.op) : CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation (CategoryTheory.RanIsSheafOfIsCocontinuous.pulledbackFamily ℱ S x Y) (CategoryTheory.RanIsSheafOfIsCocontinuous.getSection ℱ hS hx Y)

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.getSection_is_unique {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) (Y : CategoryTheory.StructuredArrow (Opposite.op U) G.op) {y : (CategoryTheory.Functor.comp ((CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))).toPrefunctor.obj (Opposite.op Y.right.unop)} (H : CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation (CategoryTheory.RanIsSheafOfIsCocontinuous.pulledbackFamily ℱ S x Y) y) : y = CategoryTheory.RanIsSheafOfIsCocontinuous.getSection ℱ hS hx Y

@[simp]

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.getSection_commute {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) {Y : CategoryTheory.StructuredArrow (Opposite.op U) G.op} {Z : CategoryTheory.StructuredArrow (Opposite.op U) G.op} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.RanIsSheafOfIsCocontinuous.getSection ℱ hS hx Y) (ℱ.val.toPrefunctor.map f.right) = CategoryTheory.RanIsSheafOfIsCocontinuous.getSection ℱ hS hx Z

def CategoryTheory.RanIsSheafOfIsCocontinuous.gluedLimitCone {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) : CategoryTheory.Limits.Cone (CategoryTheory.Ran.diagram G.op ℱ.val (Opposite.op U))

The limit cone in order to glue the sections obtained via get_section.

Equations

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

@[simp]

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.gluedLimitCone_π_app {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) (W : CategoryTheory.StructuredArrow (Opposite.op U) G.op) : (CategoryTheory.RanIsSheafOfIsCocontinuous.gluedLimitCone ℱ hS hx).π.app W = CategoryTheory.RanIsSheafOfIsCocontinuous.getSection ℱ hS hx W

def CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) : X ⟶ ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val).toPrefunctor.obj (Opposite.op U)

The section obtained by passing glued_limit_cone into CategoryTheory.Limits.limit.lift.

Equations

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

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.helper {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) {V : D} (f : V ⟶ U) (y : X ⟶ ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val).toPrefunctor.obj (Opposite.op V)) (W : CategoryTheory.StructuredArrow (Opposite.op V) G.op) (H : ∀ {V' : C} {fV : G.toPrefunctor.obj V' ⟶ V} (hV : S.arrows (CategoryTheory.CategoryStruct.comp fV f)), CategoryTheory.CategoryStruct.comp y (((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val).toPrefunctor.map fV.op) = x (CategoryTheory.CategoryStruct.comp fV f) hV) : CategoryTheory.CategoryStruct.comp y (CategoryTheory.Limits.limit.π (CategoryTheory.Ran.diagram G.op ℱ.val (Opposite.op V)) W) = (CategoryTheory.RanIsSheafOfIsCocontinuous.gluedLimitCone ℱ hS hx).π.app ((CategoryTheory.StructuredArrow.map f.op).toPrefunctor.obj W)

A helper lemma for the following two lemmas. Basically stating that if the section y : X ⟶ 𝒢(V) coincides with x on G(V') for all G(V') ⊆ V ∈ S, then X ⟶ 𝒢(V) ⟶ ℱ(W) is indeed the section obtained in get_sections. That said, this is littered with some more categorical jargon in order to be applied in the following lemmas easier.

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection_isAmalgamation {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) : CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation x (CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection ℱ hS hx)

Verify that the glued_section is an amalgamation of x.

theorem CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection_is_unique {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S ∈ K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))) S.arrows} (hx : CategoryTheory.Presieve.FamilyOfElements.Compatible x) (y : (CategoryTheory.Functor.comp ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val) (CategoryTheory.coyoneda.toPrefunctor.obj (Opposite.op X))).toPrefunctor.obj (Opposite.op U)) (hy : CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation x y) : y = CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection ℱ hS hx

Verify that the amalgamation is indeed unique.

theorem CategoryTheory.ran_isSheaf_of_isCocontinuous {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) {A : Type w} [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] {J : CategoryTheory.GrothendieckTopology C} (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsCocontinuous G J K] (ℱ : CategoryTheory.Sheaf J A) : CategoryTheory.Presheaf.IsSheaf K ((CategoryTheory.ran G.op).toPrefunctor.obj ℱ.val)

If G is cocontinuous, then Ran G.op pushes sheaves to sheaves.

This result is basically https://stacks.math.columbia.edu/tag/00XK, but without the condition that C or D has pullbacks.

def CategoryTheory.Functor.sheafPushforwardCocontinuous {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsCocontinuous G J K] : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf K A)

A cover-lifting functor induces a pushforward functor on categories of sheaves.

Equations

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

@[simp]

theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsCocontinuous G J K] [CategoryTheory.Functor.IsContinuous G J K] (X : CategoryTheory.Sheaf J A) : ((CategoryTheory.Functor.sheafAdjunctionCocontinuous G A J K).counit.app X).val = (CategoryTheory.Ran.adjunction A G.op).counit.app X.val

@[simp]

theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsCocontinuous G J K] [CategoryTheory.Functor.IsContinuous G J K] (X : CategoryTheory.Sheaf K A) : ((CategoryTheory.Functor.sheafAdjunctionCocontinuous G A J K).unit.app X).val = (CategoryTheory.Ran.adjunction A G.op).unit.app X.val

noncomputable def CategoryTheory.Functor.sheafAdjunctionCocontinuous {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.Functor.IsCocontinuous G J K] [CategoryTheory.Functor.IsContinuous G J K] : CategoryTheory.Functor.sheafPushforwardContinuous G A J K ⊣ CategoryTheory.Functor.sheafPushforwardCocontinuous G A J K

Given a functor between sites that is continuous and cocontinuous, the pushforward for the continuous functor G is left adjoint to the pushforward for the cocontinuous functor G.

Equations

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

def CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] [CategoryTheory.Functor.IsCocontinuous G J K] [CategoryTheory.Functor.IsContinuous G J K] : CategoryTheory.Functor.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ A).toPrefunctor.obj G.op) (CategoryTheory.presheafToSheaf J A) ≅ CategoryTheory.Functor.comp (CategoryTheory.presheafToSheaf K A) (CategoryTheory.Functor.sheafPushforwardContinuous G A J K)

The natural isomorphism exhibiting compatibility between pushforward and sheafification.

Equations

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

theorem CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] [CategoryTheory.Functor.IsCocontinuous G J K] [CategoryTheory.Functor.IsContinuous G J K] (F : CategoryTheory.Functor Dᵒᵖ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (CategoryTheory.Functor.comp G.op F)) ((CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility G A J K).hom.app F).val = CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)

@[simp]

theorem CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val {C : Type u} {D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{max u v, w} A] [CategoryTheory.Limits.HasLimits A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.HasWeakSheafify K A] [CategoryTheory.Functor.IsCocontinuous G J K] [CategoryTheory.Functor.IsContinuous G J K] (F : CategoryTheory.Functor Dᵒᵖ A) : ((CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility G A J K).hom.app F).val = CategoryTheory.sheafifyLift J (CategoryTheory.whiskerLeft G.op (CategoryTheory.toSheafify K F)) (_ : CategoryTheory.Presheaf.IsSheaf J ((CategoryTheory.Functor.comp (CategoryTheory.presheafToSheaf K A) (CategoryTheory.Functor.sheafPushforwardContinuous G A J K)).toPrefunctor.obj F).val)