Epimorphisms and monomorphisms in the category of presheaves of modules

In this file, we give characterizations of epimorphisms and monomorphisms in the category of presheaves of modules.

theorem PresheafOfModules.epi_of_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} {f : M₁ ⟶ M₂} (hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))) : CategoryTheory.Epi f

theorem PresheafOfModules.mono_of_injective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} {f : M₁ ⟶ M₂} (hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))) : CategoryTheory.Mono f

instance PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Epi f] (X : Cᵒᵖ) : CategoryTheory.Epi (f.app X)

instance PresheafOfModules.instMonoModuleCatCarrierObjOppositeRingCatApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Mono f] (X : Cᵒᵖ) : CategoryTheory.Mono (f.app X)

theorem PresheafOfModules.surjective_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Epi f] (X : Cᵒᵖ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))

theorem PresheafOfModules.injective_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) [CategoryTheory.Mono f] (X : Cᵒᵖ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))

theorem PresheafOfModules.epi_iff_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) : CategoryTheory.Epi f ↔ ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))

theorem PresheafOfModules.mono_iff_surjective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) : CategoryTheory.Mono f ↔ ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))