# mathlibdocumentation

category_theory.sites.cover_lifting

# 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 #

• 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 #

@[nolint]
structure category_theory.cover_lifting {C : Type u_1} {D : Type u_3} (G : C D) :
Prop

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.

theorem category_theory.id_cover_lifting {C : Type u_1}  :
(𝟭 C)

The identity functor on a site is cover-lifting.

theorem category_theory.comp_cover_lifting {C : Type u_1} {D : Type u_3} {E : Type u_5} {F : C D} (hu : F) {G : D E} (hv : G) :
(F G)

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 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.

@[protected, instance]
noncomputable def category_theory.Ran_is_sheaf_of_cover_lifting.pulledback_family {C D : Type u} {A : Type w} {G : C D} (ℱ : A) {X : A} {U : D} (S : category_theory.sieve U) (Y : G.op) :

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

Equations
@[simp]
theorem category_theory.Ran_is_sheaf_of_cover_lifting.pulledback_family_apply {C D : Type u} {A : Type w} {G : C D} (ℱ : A) {X : A} {U : D} (S : category_theory.sieve U) (Y : G.op) {W : C} {f : W }  :
= x (G.map f Y.hom.unop) Hf ℱ.val).app (opposite.op W)
noncomputable def category_theory.Ran_is_sheaf_of_cover_lifting.get_section {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) (Y : G.op) :
X ℱ.val.obj Y.right

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

Equations
theorem category_theory.Ran_is_sheaf_of_cover_lifting.get_section_is_amalgamation {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) (Y : G.op) :
theorem category_theory.Ran_is_sheaf_of_cover_lifting.get_section_is_unique {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) (Y : G.op) {y : ((𝟭 (Cᵒᵖ A)).obj ℱ.val .obj }  :
@[simp]
theorem category_theory.Ran_is_sheaf_of_cover_lifting.get_section_commute {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) {Y Z : G.op} (f : Y Z) :
ℱ.val.map f.right =
noncomputable def category_theory.Ran_is_sheaf_of_cover_lifting.glued_limit_cone {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) :

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

Equations
@[simp]
theorem category_theory.Ran_is_sheaf_of_cover_lifting.glued_limit_cone_π_app {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) (W : G.op) :
noncomputable def category_theory.Ran_is_sheaf_of_cover_lifting.glued_section {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) :
X .obj ℱ.val).obj (opposite.op U)

The section obtained by passing glued_limit_cone into category_theory.limits.limit.lift.

Equations
theorem category_theory.Ran_is_sheaf_of_cover_lifting.helper {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) {V : D} (f : V U) (y : X .obj ℱ.val).obj (opposite.op V)) (W : G.op) (H : ∀ {V' : C} {fV : G.obj V' V} (hV : S.arrows (fV f)), y .obj ℱ.val).map fV.op = x (fV f) hV) :

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 category_theory.Ran_is_sheaf_of_cover_lifting.glued_section_is_amalgamation {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) :

Verify that the glued_section is an amalgamation of x.

theorem category_theory.Ran_is_sheaf_of_cover_lifting.glued_section_is_unique {C D : Type u} {A : Type w} {G : C D} (hu : G) (ℱ : A) {X : A} {U : D} {S : category_theory.sieve U} (hS : S K U) (hx : x.compatible) (y : .obj ℱ.val .obj (opposite.op U)) (hy : x.is_amalgamation y) :

Verify that the amalgamation is indeed unique.

theorem category_theory.Ran_is_sheaf_of_cover_lifting {C D : Type u} {A : Type w} {G : C D} (hG : G) (ℱ : A) :

If G is cover_lifting, 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.

noncomputable def category_theory.sites.copullback {C D : Type u} (A : Type w) {G : C D} (hG : G) :

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

Equations
@[simp]
theorem category_theory.sites.pullback_copullback_adjunction_unit_app_val {C D : Type u} (A : Type w) {G : C D} (Hp : G) (Hl : G) (X : A) :
Hc).unit.app X).val = X.val
@[simp]
theorem category_theory.sites.pullback_copullback_adjunction_counit_app_val {C D : Type u} (A : Type w) {G : C D} (Hp : G) (Hl : G) (X : A) :
Hc).counit.app X).val = X.val
noncomputable def category_theory.sites.pullback_copullback_adjunction {C D : Type u} (A : Type w) {G : C D} (Hp : G) (Hl : G)  :

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

Equations