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.

def CategoryTheory.Sheaf.locallyInjective {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] : MorphismProperty (Sheaf J A)

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

Equations

• CategoryTheory.Sheaf.locallyInjective J A f = CategoryTheory.Sheaf.IsLocallyInjective f

def CategoryTheory.Sheaf.locallySurjective {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] : MorphismProperty (Sheaf J A)

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

Equations

• CategoryTheory.Sheaf.locallySurjective J A f = CategoryTheory.Sheaf.IsLocallySurjective f

noncomputable def CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [J.WEqualsLocallyBijective A] (data : ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [HasWeakSheafify J A] : (locallySurjective J A).FunctorialFactorizationData (locallyInjective J A)

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.

instance CategoryTheory.Sheaf.instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [J.WEqualsLocallyBijective A] (data : ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [HasWeakSheafify J A] (f : Arrow (Sheaf J A)) : IsLocallySurjective ((functorialLocallySurjectiveInjectiveFactorization J data).i.app f)

instance CategoryTheory.Sheaf.instIsLocallyInjectiveAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [J.WEqualsLocallyBijective A] (data : ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [HasWeakSheafify J A] (f : Arrow (Sheaf J A)) : IsLocallyInjective ((functorialLocallySurjectiveInjectiveFactorization J data).p.app f)

instance CategoryTheory.Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [J.WEqualsLocallyBijective A] (data : ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [HasWeakSheafify J A] (f : Arrow (Sheaf J A)) [J.HasSheafCompose (forget A)] : Epi ((functorialLocallySurjectiveInjectiveFactorization J data).i.app f)

instance CategoryTheory.Sheaf.instMonoAppArrowPLocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [J.WEqualsLocallyBijective A] (data : ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [HasWeakSheafify J A] (f : Arrow (Sheaf J A)) [J.HasSheafCompose (forget A)] : Mono ((functorialLocallySurjectiveInjectiveFactorization J data).p.app f)

instance CategoryTheory.Sheaf.instHasFunctorialFactorizationLocallySurjectiveLocallyInjective {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] [J.WEqualsLocallyBijective A] [HasWeakSheafify J A] : (locallySurjective J A).HasFunctorialFactorization (locallyInjective J A)

theorem CategoryTheory.Sheaf.isLocallySurjective_iff_epi' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (A : Type u') [Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] [J.WEqualsLocallyBijective A] [HasSheafify J A] [J.HasSheafCompose (forget A)] [Balanced (Sheaf J A)] {F G : Sheaf J A} (φ : F ⟶ G) : IsLocallySurjective φ ↔ Epi φ