The relationship between effective and regular epimorphisms. #
This file proves that the notions of regular epi and effective epi are equivalent for morphisms with kernel pairs, and that regular epi implies effective epi in general.
def
CategoryTheory.effectiveEpiStructOfRegularEpi
{C : Type u_1}
[Category.{u_2, u_1} C]
{B X : C}
(f : X ⟶ B)
[RegularEpi f]
:
The data of an EffectiveEpi structure on a RegularEpi.
Equations
Instances For
instance
CategoryTheory.instEffectiveEpiOfRegularEpi
{C : Type u_1}
[Category.{u_2, u_1} C]
{B X : C}
(f : X ⟶ B)
[RegularEpi f]
:
theorem
CategoryTheory.effectiveEpiOfKernelPair
{C : Type u_1}
[Category.{u_2, u_1} C]
{B X : C}
(f : X ⟶ B)
[Limits.HasPullback f f]
(hc : Limits.IsColimit (Limits.Cofork.ofπ f ⋯))
:
A morphism which is a coequalizer for its kernel pair is an effective epi.
noncomputable instance
CategoryTheory.regularEpiOfEffectiveEpi
{C : Type u_1}
[Category.{u_2, u_1} C]
{B X : C}
(f : X ⟶ B)
[Limits.HasPullback f f]
[EffectiveEpi f]
:
An effective epi which has a kernel pair is a regular epi.