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 sievescategory_theory.sites.copullback
: A cover-lifting functorG : (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
: IfG : C ⥤ D
is cover_lifting, thenRan G.op
(ₚu
) as a functor(Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A)
of presheaves maps sheaves to sheaves.category_theory.pullback_copullback_adjunction
: IfG : (C, J) ⥤ (D, K)
is cover-lifting, cover-preserving, and compatible-preserving, thenpullback G
andcopullback 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
- cover_lift : ∀ {U : C} {S : category_theory.sieve (G.obj U)}, S ∈ ⇑K (G.obj U) → category_theory.sieve.functor_pullback G S ∈ ⇑J U
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 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.
The family of morphisms X ⟶ 𝒢(G(Y')) ⟶ ℱ(Y')
defined on { Y' ⊆ Y : G(Y') ⊆ U ∈ S}
.
Equations
- category_theory.Ran_is_sheaf_of_cover_lifting.pulledback_family ℱ S x Y = category_theory.presieve.family_of_elements.comp_presheaf_map (show (category_theory.Ran G.op ⋙ (category_theory.whiskering_left Cᵒᵖ Dᵒᵖ A).obj G.op).obj ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op X) ⟶ (𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op X), from category_theory.whisker_right ((category_theory.Ran.adjunction A G.op).counit.app ℱ.val) (category_theory.coyoneda.obj (opposite.op X))) (category_theory.presieve.family_of_elements.functor_pullback G (category_theory.presieve.family_of_elements.pullback Y.hom.unop x))
Given a G(Y) ⊆ U
, we can find a unique section X ⟶ ℱ(Y)
that agrees with x
.
Equations
- category_theory.Ran_is_sheaf_of_cover_lifting.get_section hu ℱ hS hx Y = let hom_sh : (category_theory.Ran G.op ⋙ (category_theory.whiskering_left Cᵒᵖ Dᵒᵖ A).obj G.op).obj ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op X) ⟶ (𝟭 (Cᵒᵖ ⥤ A)).obj ℱ.val ⋙ category_theory.coyoneda.obj (opposite.op X) := category_theory.whisker_right ((category_theory.Ran.adjunction A G.op).counit.app ℱ.val) (category_theory.coyoneda.obj (opposite.op X)) in _.amalgamate (category_theory.presieve.family_of_elements.comp_presheaf_map hom_sh (category_theory.presieve.family_of_elements.functor_pullback G (category_theory.presieve.family_of_elements.pullback Y.hom.unop x))) _
The limit cone in order to glue the sections obtained via get_section
.
Equations
- category_theory.Ran_is_sheaf_of_cover_lifting.glued_limit_cone hu ℱ hS hx = {X := X, π := {app := λ (Y : category_theory.structured_arrow (opposite.op U) G.op), category_theory.Ran_is_sheaf_of_cover_lifting.get_section hu ℱ hS hx Y, naturality' := _}}
The section obtained by passing glued_limit_cone
into category_theory.limits.limit.lift
.
Equations
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.
Verify that the glued_section
is an amalgamation of x
.
Verify that the amalgamation is indeed unique.
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.
A cover-lifting functor induces a morphism of sites in the same direction as the functor.
Equations
- category_theory.sites.copullback A hG = {obj := λ (ℱ : category_theory.Sheaf J A), {val := (category_theory.Ran G.op).obj ℱ.val, cond := _}, map := λ (_x _x_1 : category_theory.Sheaf J A) (f : _x ⟶ _x_1), {val := (category_theory.Ran G.op).map f.val}, map_id' := _, map_comp' := _}
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
- category_theory.sites.pullback_copullback_adjunction A Hp Hl Hc = {hom_equiv := λ (X : category_theory.Sheaf K A) (Y : category_theory.Sheaf J A), {to_fun := λ (f : (category_theory.sites.pullback A Hc Hp).obj X ⟶ Y), {val := ⇑((category_theory.Ran.adjunction A G.op).hom_equiv X.val Y.val) f.val}, inv_fun := λ (f : X ⟶ (category_theory.sites.copullback A Hl).obj Y), {val := ⇑(((category_theory.Ran.adjunction A G.op).hom_equiv X.val Y.val).symm) f.val}, left_inv := _, right_inv := _}, unit := {app := λ (X : category_theory.Sheaf K A), {val := (category_theory.Ran.adjunction A G.op).unit.app X.val}, naturality' := _}, counit := {app := λ (X : category_theory.Sheaf J A), {val := (category_theory.Ran.adjunction A G.op).counit.app X.val}, naturality' := _}, hom_equiv_unit' := _, hom_equiv_counit' := _}