Epimorphisms of sheaves with values in a concrete category

For a concrete category A, the functor sheafCompose J (forget A) : Sheaf J A ⥤ Sheaf J (Type w) preserves epimorphisms (CategoryTheory.Sheaf.preservesEpimorphisms_sheafCompose_forget) and reflects them, so a morphism of A-valued sheaves is an epimorphism if and only if its underlying morphism of sheaves of types is (CategoryTheory.Functor.epi_map_iff_epi): in both categories the epimorphisms are the locally surjective morphisms, and local surjectivity of an A-valued presheaf map is a condition on its underlying map of presheaves of types (CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget).

This generalizes Mathlib's PreservesEpimorphisms instance for LightCondensed.forget in Mathlib.Condensed.Light.Epi (Dagur Asgeirsson), with the same proof, from light condensed modules to arbitrary sites. Reflection of epimorphisms needs no separate instance: sheafCompose J (forget A) is faithful, so Mathlib's Functor.reflectsEpimorphisms_of_faithful applies.

It also records that a monomorphism of sheaves with values in a concrete category whose forgetful functor preserves pullbacks is injective on the sections over every object (CategoryTheory.Sheaf.injective_app_of_mono).

instance CategoryTheory.Sheaf.preservesEpimorphisms_sheafCompose_forget {C : Type u_1} [Category.{v_1, u_1} C] (J : GrothendieckTopology C) {A : Type u_2} [Category.{v_2, u_2} A] {FA : A → A → Type u_3} {CA : A → Type w} [(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [HasSheafify J A] [J.HasSheafCompose (forget A)] [J.WEqualsLocallyBijective A] [ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A] [Balanced (Sheaf J A)] : (sheafCompose J (forget A)).PreservesEpimorphisms

An epimorphism of sheaves with values in a concrete category is an epimorphism of the underlying sheaves of sets: both are the locally surjective morphisms.

theorem CategoryTheory.Sheaf.injective_app_of_mono {D : Type u_1} [Category.{u_6, u_1} D] {J : GrothendieckTopology D} {C : Type u_2} [Category.{u_5, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] [Limits.HasPullbacks C] [Limits.PreservesLimitsOfShape Limits.WalkingCospan (forget C)] {F G : Sheaf J C} (f : F ⟶ G) [Mono f] (W : Dᵒᵖ) : Function.Injective ⇑(ConcreteCategory.hom (f.hom.app W))

A monomorphism of sheaves of a concrete category, whose forgetful functor preserves pullbacks, is injective on sections over every object.