# mathlibdocumentation

category_theory.sites.cover_preserving

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

• category_theory.cover_preserving: a functor between sites is cover-preserving if it pushes covering sieves to covering sieves
• category_theory.compatible_preserving: a functor between sites is compatible-preserving if it pushes compatible families of elements to compatible families.
• category_theory.pullback_sheaf: the pullback of a sheaf along a cover-preserving and compatible-preserving functor.
• category_theory.sites.pullback: the induced functor Sheaf K A ⥤ Sheaf J A for a cover-preserving and compatible-preserving functor G : (C, J) ⥤ (D, K).
• category_theory.sites.pushforward: the induced functor Sheaf J A ⥤ Sheaf K A for a cover-preserving and compatible-preserving functor G : (C, J) ⥤ (D, K).
• category_theory.sites.pushforward: the induced functor Sheaf J A ⥤ Sheaf K A for a cover-preserving and compatible-preserving functor G : (C, J) ⥤ (D, K).

## Main results #

• category_theory.sites.whiskering_left_is_sheaf_of_cover_preserving: If G : C ⥤ D is cover-preserving and compatible-preserving, then G ⋙ - (uᵖ) as a functor (Dᵒᵖ ⥤ A) ⥤ (Cᵒᵖ ⥤ A) of presheaves maps sheaves to sheaves.

## References #

@[nolint]
structure category_theory.cover_preserving {C : Type u₁} {D : Type u₂} (G : C D) :
Prop

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.

theorem category_theory.id_cover_preserving {C : Type u₁}  :

The identity functor on a site is cover-preserving.

theorem category_theory.cover_preserving.comp {C : Type u₁} {D : Type u₂} {A : Type u₃} {F : C D} (hF : F) {G : D A} (hG : G) :
(F G)

The composition of two cover-preserving functors is cover-preserving.

@[nolint]
structure category_theory.compatible_preserving {C : Type u₁} {D : Type u₂} (G : C D) :
Prop
• compatible : ∀ (ℱ : {Z : C} {T : {x : , x.compatible∀ {Y₁ Y₂ : C} {X : D} (f₁ : X G.obj Y₁) (f₂ : X G.obj Y₂) {g₁ : Y₁ Z} {g₂ : Y₂ Z} (hg₁ : T g₁) (hg₂ : T g₂), f₁ G.map g₁ = f₂ G.map g₂ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

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

theorem category_theory.presieve.family_of_elements.compatible.functor_pushforward {C : Type u₁} {D : Type u₂} {G : C D} {Z : C} {T : category_theory.presieve Z} {x : T} (h : x.compatible) :

compatible_preserving functors indeed preserve compatible families.

@[simp]
theorem category_theory.compatible_preserving.apply_map {C : Type u₁} {D : Type u₂} {G : C D} {Z : C} {T : category_theory.presieve Z} {x : T} (h : x.compatible) {Y : C} {f : Y Z} (hf : T f) :
= x f hf
theorem category_theory.compatible_preserving_of_flat {C : Type u₁} {D : Type u₁} (G : C D)  :
theorem category_theory.pullback_is_sheaf_of_cover_preserving {C : Type u₁} {D : Type u₂} {A : Type u₃} {G : C D} (hG₁ : G) (hG₂ : G) (ℱ : A) :
(G.op ℱ.val)

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

This result is basically https://stacks.math.columbia.edu/tag/00WW.

def category_theory.pullback_sheaf {C : Type u₁} {D : Type u₂} {A : Type u₃} {G : C D} (hG₁ : G) (hG₂ : G) (ℱ : A) :

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

Equations
@[simp]
theorem category_theory.sites.pullback_obj {C : Type u₁} {D : Type u₂} (A : Type u₃) {G : C D} (hG₁ : G) (hG₂ : G) (ℱ : A) :
hG₂).obj =
@[simp]
theorem category_theory.sites.pullback_map_val {C : Type u₁} {D : Type u₂} (A : Type u₃) {G : C D} (hG₁ : G) (hG₂ : G) (_x _x_1 : A) (f : _x _x_1) :
hG₂).map f).val = .obj G.op).map f.val
def category_theory.sites.pullback {C : Type u₁} {D : Type u₂} (A : Type u₃) {G : C D} (hG₁ : G) (hG₂ : G) :

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

Equations
Instances for category_theory.sites.pullback
@[protected, instance]
noncomputable def category_theory.Sheaf_to_presheaf.creates_limits {C : Type v₁} (A : Type u₂)  :
Equations
@[protected, instance]
@[simp]
theorem category_theory.sites.pushforward_map_val_app {C : Type v₁} {D : Type v₁} (A : Type u₂) (G : C D) (_x _x_1 : A) (f : _x _x_1) (X : Dᵒᵖ) :
noncomputable def category_theory.sites.pushforward {C : Type v₁} {D : Type v₁} (A : Type u₂) (G : C D) :

The pushforward functor Sheaf J A ⥤ Sheaf K A associated to a functor G : C ⥤ D in the same direction as G.

Equations
Instances for category_theory.sites.pushforward
@[simp]
theorem category_theory.sites.pushforward_obj_val_obj {C : Type v₁} {D : Type v₁} (A : Type u₂) (G : C D) (X : A) (X_1 : Dᵒᵖ) :
@[simp]
theorem category_theory.sites.pushforward_obj_val_map {C : Type v₁} {D : Type v₁} (A : Type u₂) (G : C D) (X : A) (X_1 Y : Dᵒᵖ) (f : X_1 Y) :
@[protected, instance]
Equations
noncomputable def category_theory.sites.pullback_pushforward_adjunction {C : Type v₁} {D : Type v₁} (A : Type u₂) {G : C D} (hG₁ : G) (hG₂ : G) :
hG₂

The pushforward functor is left adjoint to the pullback functor.

Equations