Cover-lifting functors between sites. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define cover-lifting functors between sites as functors that pull covering sieves back to covering sieves. This concept is also known as cocontinuous functors or cover-reflecting functors, but we have chosen this name following [MM92] in order to avoid potential naming collision or confusion with the general definition of cocontinuous functors between categories as functors preserving small colimits.

The definition given here seems stronger than the definition found elsewhere, but they are actually equivalent via category_theory.grothendieck_topology.superset_covering. (The precise statement is not formalized, but follows from it quite trivially).

Main definitions #

• category_theory.sites.cover_lifting: a functor between sites is cover-lifting if it pulls back covering sieves to covering sieves
• category_theory.sites.copullback: A cover-lifting functor G : (C, J) ⥤ (D, K) induces a morphism of sites in the same direction as the functor.

Main results #

• category_theory.sites.Ran_is_sheaf_of_cover_lifting: If G : C ⥤ D is cover_lifting, then Ran G.op (ₚu) as a functor (Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A) of presheaves maps sheaves to sheaves.
• category_theory.pullback_copullback_adjunction: If G : (C, J) ⥤ (D, K) is cover-lifting, cover-preserving, and compatible-preserving, then pullback G and copullback G are adjoint.

References #

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

We will now prove that Ran G.op (ₚu) maps sheaves to sheaves if G is cover-lifting. This can be found in https://stacks.math.columbia.edu/tag/00XK. However, the proof given here 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 cover-lifting property of 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.