Local epimorphisms with respect to an object property

Let P be an object property on a category C. We say that f : X ⟶ Y is a local epimorphism wrt. P if f cancels on the left for morphisms with codomain in P.

If C is the category of presheafs on some category with Grothendieck topology J and P the property of being a sheaf for J, then being a local epimorphism wrt. P is being an epimorphism after sheafification.

Main declarations

• CategoryTheory.ObjectProperty.localEpi: The morphism property of local epimorphisms.
• CategoryTheory.ObjectProperty.localEpi_mem_range_iff_epi: If F ⊣ G and G is fully faithful, then f : X ⟶ Y is a local epimorphism if and only if F.map f is an epimorphism.

References

The terminology is from M. Kashiwara, P. Schapira, Categories and Sheaves, 16.1.

def CategoryTheory.ObjectProperty.localEpi {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) : MorphismProperty C

A morphism f is a local epimorphism wrt. the object property P if it satisfies left cancellation for morphisms with codomain in P.

Equations

• P.localEpi f = ∀ ⦃Z : C⦄, P Z → Function.Injective fun (g : x✝ ⟶ Z) => CategoryTheory.CategoryStruct.comp f g

instance CategoryTheory.ObjectProperty.instIsMultiplicativeLocalEpi {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} : P.localEpi.IsMultiplicative

theorem CategoryTheory.ObjectProperty.localEpi.of_epi {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} {X Y : C} (f : X ⟶ Y) [Epi f] : P.localEpi f

@[simp]

theorem CategoryTheory.ObjectProperty.localEpi_top_apply_iff {C : Type u_1} [Category.{v_1, u_1} C] {X Y : C} {f : X ⟶ Y} : ⊤.localEpi f ↔ Epi f

theorem CategoryTheory.ObjectProperty.localEpi_top_eq_epimorphisms {C : Type u_1} [Category.{v_1, u_1} C] : ⊤.localEpi = MorphismProperty.epimorphisms C

theorem CategoryTheory.ObjectProperty.localEpi_antitone {C : Type u_1} [Category.{v_1, u_1} C] : Antitone localEpi

theorem CategoryTheory.ObjectProperty.localEpi_isoClosure {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} : P.isoClosure.localEpi = P.localEpi

theorem CategoryTheory.ObjectProperty.isLocal_le_localEpi {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} : P.isLocal ≤ P.localEpi

instance CategoryTheory.ObjectProperty.instRespectsIsoLocalEpi {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} : P.localEpi.RespectsIso

instance CategoryTheory.ObjectProperty.instHasOfPrecompPropertyLocalEpi {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} (W : MorphismProperty C) : P.localEpi.HasOfPrecompProperty W

instance CategoryTheory.ObjectProperty.instHasOfPostcompPropertyLocalEpiIsLocal {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} : P.localEpi.HasOfPostcompProperty P.isLocal

instance CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeLocalEpi {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} : P.localEpi.IsStableUnderCobaseChange

instance CategoryTheory.ObjectProperty.instRespectsLocalEpiIsLocal {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} : P.localEpi.Respects P.isLocal

theorem CategoryTheory.ObjectProperty.localEpi_mem_range_iff_epi {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.Faithful] [G.Full] {X Y : C} (f : X ⟶ Y) : localEpi (fun (x : C) => x ∈ Set.range G.obj) f ↔ Epi (F.map f)

theorem CategoryTheory.ObjectProperty.localEpi_mem_range_eq_inverseImage_epimorphisms {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.Faithful] [G.Full] : (localEpi fun (x : C) => x ∈ Set.range G.obj) = (MorphismProperty.epimorphisms D).inverseImage F

theorem CategoryTheory.ObjectProperty.localEpi_essImage {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) [G.Faithful] [G.Full] : G.essImage.localEpi = (MorphismProperty.epimorphisms D).inverseImage F