# Documentation

Mathlib.CategoryTheory.Sites.Surjective

# Locally surjective morphisms #

## Main definitions #

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

• toSheafify_isLocallySurjective : toSheafify is locally surjective.
theorem CategoryTheory.imageSieve_apply {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) {U : C} (s : ().obj (G.obj ())) (V : C) (i : V U) :
().arrows i = t, ↑(f.app ()) t = ↑(G.map i.op) s
def CategoryTheory.imageSieve {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) {U : C} (s : ().obj (G.obj ())) :

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.

Instances For
theorem CategoryTheory.imageSieve_eq_sieveOfSection {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) {U : C} (s : ().obj (G.obj ())) :
theorem CategoryTheory.imageSieve_whisker_forget {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) {U : C} (s : ().obj (G.obj ())) :
theorem CategoryTheory.imageSieve_app {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) {U : C} (s : ().obj (F.obj ())) :
CategoryTheory.imageSieve f (↑(f.app ()) s) =
def CategoryTheory.IsLocallySurjective {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) :

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.

Instances For
theorem CategoryTheory.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) :
theorem CategoryTheory.isLocallySurjective_iff_isIso {C : Type u} {F : } {G : } (f : F G) :
theorem CategoryTheory.isLocallySurjective_iff_whisker_forget {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) :
theorem CategoryTheory.isLocallySurjective_of_surjective {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) (H : ∀ (U : Cᵒᵖ), Function.Surjective ↑(f.app U)) :
theorem CategoryTheory.isLocallySurjective_of_iso {C : Type u} {A : Type u'} [] {F : } {G : } (f : F G) :
theorem CategoryTheory.IsLocallySurjective.comp {C : Type u} {A : Type u'} [] {F₁ : } {F₂ : } {F₃ : } {f₁ : F₁ F₂} {f₂ : F₂ F₃} (h₁ : ) (h₂ : ) :

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

Instances For
theorem CategoryTheory.toSheafify_isLocallySurjective {C : Type u} {B : Type w} [] [] [] [(X : C) → (W : ) → ] [] [∀ (α β : Type (max u v)) (fst snd : βα), ] (F : ) :