Documentation

Mathlib.CategoryTheory.Sites.EpiMono

Morphisms of sheaves factor as a locally surjective followed by a locally injective morphism #

When morphisms in a concrete category A factor in a functorial manner as a surjective map followed by an injective map, we obtain that any morphism of sheaves in Sheaf J A factors in a functorial manner as a locally surjective morphism (which is epi) followed by a locally injective morphism (which is mono).

Moreover, if we assume that the category of sheaves Sheaf J A is balanced (see Sites.LeftExact), then epimorphisms are exactly locally surjective morphisms.

The class of locally injective morphisms of sheaves, see Sheaf.IsLocallyInjective.

Equations
Instances For

    The class of locally surjective morphisms of sheaves, see Sheaf.IsLocallySurjective.

    Equations
    Instances For

      Given a functorial surjective/injective factorizations of morphisms in a concrete category A, this is the induced functorial locally surjective/locally injective factorization of morphisms in the category Sheaf J A.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For