The category of type-valued sheaves is a regular epi category

Main results

isRegularEpiCategory_sheaf: Let J be a Grothendieck topology on C, and suppose that D is a regular epi category which has pushouts and pullbacks, and that sheafification of D-valued J-sheaves exists. Suppose further that the category Sheaf J D is balanced, and that the underlying morphism of presheaves of every epimorphism in Sheaf J D can be factored as an epimorphism followed by a monomorphism. Then Sheaf J D is a regular epi category.

Note: This is not an instance because of the factorisation requirement, but it can in principle be turned into an instance whenever D has equalizers and Cᵒᵖ ⥤ D has images. This holds in particular when D is Type* or any abelian category. We add it as an instance for D := Type*, but the fact that Sheaf J D is a regular epi category when D is an abelian category already follows from the sheaf category being abelian.

References

We follow the proof of Proposition 3.4.13 in [Bor94c] Handbook of Categorical Algebra: Volume 3, Sheaf Theory, by Borceux, 1994. The first part of that proof, the result for presheaf categories, is proved in the file Mathlib.CategoryTheory.Functor.RegularEpi.

theorem CategoryTheory.isRegularEpiCategory_sheaf {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (J : GrothendieckTopology C) [Limits.HasPullbacks D] [Limits.HasPushouts D] [IsRegularEpiCategory D] (h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ (I : Functor Cᵒᵖ D) (p : F.val ⟶ I) (i : I ⟶ G.val), Epi p ∧ Mono i ∧ CategoryStruct.comp p i = f.val) [HasSheafify J D] [Balanced (Sheaf J D)] : IsRegularEpiCategory (Sheaf J D)

instance CategoryTheory.instIsRegularEpiCategorySheafTypeOfHasSheafify {C : Type u_1} [Category.{u_3, u_1} C] (J : GrothendieckTopology C) [HasSheafify J (Type u)] : IsRegularEpiCategory (Sheaf J (Type u))