Locally surjective morphisms #

Main definitions #

Main results #

theorem CategoryTheory.imageSieve_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F : CategoryTheory.Functor Cᵒᵖ A} {G : CategoryTheory.Functor Cᵒᵖ A} (f : F G) {U : C} (s : (CategoryTheory.forget A).obj (G.obj (Opposite.op U))) (V : C) (i : V U) :
(CategoryTheory.imageSieve f s).arrows i = t, ↑( (Opposite.op V)) t = ↑( i.op) s

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

    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