mathlib3 documentation


Cover-preserving functors between sites. #

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

We define cover-preserving functors between sites as functors that push covering sieves to covering sieves. A cover-preserving and compatible-preserving functor G : C ⥤ D then pulls sheaves on D back to sheaves on C via G.op ⋙ -.

Main definitions #

Main results #

References #


A functor G : (C, J) ⥤ (D, K) between sites is cover-preserving if for all covering sieves R in C, R.pushforward_functor G is a covering sieve in D.

The identity functor on a site is cover-preserving.


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₁ = f₂ ≫ 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 functor_pushforward used.

If G is cover-preserving and compatible-preserving, then G.op ⋙ _ pulls sheaves back to sheaves.

This result is basically

The pullback of a sheaf along a cover-preserving and compatible-preserving functor.


The induced functor from Sheaf K A ⥤ Sheaf J A given by G.op ⋙ _ if G is cover-preserving and compatible-preserving.

Instances for category_theory.sites.pullback