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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] : CategoryTheory.MorphismProperty (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] : CategoryTheory.MorphismProperty (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.Sheaf.locallySurjective J A).FunctorialFactorizationData (CategoryTheory.Sheaf.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A) [CategoryTheory.HasWeakSheafify J A] (f : CategoryTheory.Arrow (CategoryTheory.Sheaf J A)) : CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization J data).i.app f)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance CategoryTheory.Sheaf.instHasFunctorialFactorizationLocallySurjectiveLocallyInjective {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] [J.WEqualsLocallyBijective A] [CategoryTheory.HasWeakSheafify J A] : (CategoryTheory.Sheaf.locallySurjective J A).HasFunctorialFactorization (CategoryTheory.Sheaf.locallyInjective J A)

Equations

• ⋯ = ⋯

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