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₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
{f : M₁ ⟶ M₂}
(hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(f.app X))
:
theorem
PresheafOfModules.mono_of_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
{f : M₁ ⟶ M₂}
(hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(f.app X))
:
instance
PresheafOfModules.instEpiModuleCatαRingObjOppositeRingCatApp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
[CategoryTheory.Epi f]
(X : Cᵒᵖ)
:
CategoryTheory.Epi (f.app X)
Equations
- ⋯ = ⋯
instance
PresheafOfModules.instMonoModuleCatαRingObjOppositeRingCatApp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
[CategoryTheory.Mono f]
(X : Cᵒᵖ)
:
CategoryTheory.Mono (f.app X)
Equations
- ⋯ = ⋯
theorem
PresheafOfModules.surjective_of_epi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
[CategoryTheory.Epi f]
(X : Cᵒᵖ)
:
Function.Surjective ⇑(f.app X)
theorem
PresheafOfModules.injective_of_mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
[CategoryTheory.Mono f]
(X : Cᵒᵖ)
:
Function.Injective ⇑(f.app X)
theorem
PresheafOfModules.epi_iff_surjective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
:
CategoryTheory.Epi f ↔ ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(f.app X)
theorem
PresheafOfModules.mono_iff_surjective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{M₁ : PresheafOfModules R}
{M₂ : PresheafOfModules R}
(f : M₁ ⟶ M₂)
:
CategoryTheory.Mono f ↔ ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(f.app X)