mathlib3 documentation


Locally surjective morphisms #

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

Main definitions #

Main results #

theorem category_theory.image_sieve_apply {C : Type u} [category_theory.category C] {A : Type u'} [category_theory.category A] [category_theory.concrete_category A] {F G : Cᵒᵖ A} (f : F G) {U : C} (s : (G.obj (opposite.op U))) (V : C) (i : V 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.


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.