# mathlib3documentation

category_theory.sites.surjective

# Locally surjective morphisms #

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

## Main definitions #

• is_locally_surjective : A morphism of presheaves valued in a concrete category is locally surjective with respect to a grothendieck topology if every section in the target is locally in the set-theoretic image, i.e. the image sheaf coincides with the target.

## Main results #

• to_sheafify_is_locally_surjective : to_sheafify is locally surjective.
theorem category_theory.image_sieve_apply {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) {U : C} (s : (G.obj (opposite.op U))) (V : C) (i : V U) :
i = (t : (F.obj (opposite.op V))), (f.app (opposite.op V)) t = (G.map i.op) s
def category_theory.image_sieve {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) {U : C} (s : (G.obj (opposite.op U))) :

Given f : F ⟶ G, a morphism between presieves, and s : G.obj (op U), this is the sieve of U consisting of the i : V ⟶ U such that s restricted along i is in the image of f.

Equations
theorem category_theory.image_sieve_eq_sieve_of_section {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) {U : C} (s : (G.obj (opposite.op U))) :
theorem category_theory.image_sieve_whisker_forget {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) {U : C} (s : (G.obj (opposite.op U))) :
theorem category_theory.image_sieve_app {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) {U : C} (s : (F.obj (opposite.op U))) :
((f.app (opposite.op U)) s) =
def category_theory.is_locally_surjective {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) :
Prop

A morphism of presheaves f : F ⟶ G is locally surjective with respect to a grothendieck topology if every section of G is locally in the image of f.

Equations
theorem category_theory.is_locally_surjective_iff_is_iso {C : Type u} {F G : (Type w)} (f : F G) :
theorem category_theory.is_locally_surjective_iff_whisker_forget {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) :
theorem category_theory.is_locally_surjective_of_surjective {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G) (H : (U : Cᵒᵖ), function.surjective (f.app U)) :
theorem category_theory.is_locally_surjective_of_iso {C : Type u} {A : Type u'} {F G : Cᵒᵖ A} (f : F G)  :
theorem category_theory.is_locally_surjective.comp {C : Type u} {A : Type u'} {F₁ F₂ F₃ : Cᵒᵖ A} {f₁ : F₁ F₂} {f₂ : F₂ F₃} (h₁ : f₁) (h₂ : f₂) :
(f₁ f₂)
noncomputable def category_theory.sheafification_iso_image_presheaf {C : Type u} (F : Cᵒᵖ Type (max u v)) :

The image of F in J.sheafify F is isomorphic to the sheafification.

Equations
theorem category_theory.to_sheafify_is_locally_surjective {C : Type u} {B : Type w} [ (X : C), ] [ (P : Cᵒᵖ B) (X : C) (S : J.cover X), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ B), ] [Π (X : C), ] [ (α β : Type (max u v)) (fst snd : β α), ] (F : Cᵒᵖ B) :