mathlib3

9dd3807b - feat(category_theory/sites/{sheaf, sheafification}): monomorphisms of sheaves are precisely monomorphisms of presheaves (#15932)

feat(category_theory/sites/{sheaf, sheafification}): monomorphisms of sheaves are precisely monomorphisms of presheaves (#15932) * monomorphisms of sheaves are precisely monomorphisms of underlying presheaves (when presheaves can be sheafified) * a morphism between sheaves is epic if the morphism between underlying presheaves is epic. (The converse is not always true)