Documentation

Mathlib.CategoryTheory.Sites.CoverPreserving

Cover-preserving functors between sites. #

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.functorPushforward G is a covering sieve in D.

Instances For

    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.

    Instances For

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

      Instances For