mathlib documentation


Cover-lifting functors between sites. #

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 #

Main results #

References #


A functor G : (C, J) ⥤ (D, K) between sites is called to have the cover-lifting property if for all covering sieves R in D, R.pullback G is a covering sieve in C.

The identity functor on a site is cover-lifting.

The composition of two cover-lifting functors are cover-lifting

We will now prove that Ran G.op (ₚu) maps sheaves to sheaves if G is cover-lifting. This can be found in 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.

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


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


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.

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

This result is basically, but without the condition that C or D has pullbacks.

A cover-lifting functor induces a morphism of sites in the same direction as the functor.


Given a functor between sites that is cover-preserving, cover-lifting, and compatible-preserving, the pullback and copullback along G are adjoint to each other