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}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.RegularEpi f]
:
The data of an EffectiveEpi structure on a RegularEpi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpiOfRegularEpi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.RegularEpi f]
:
Equations
- ⋯ = ⋯
theorem
CategoryTheory.effectiveEpiOfKernelPair
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.Limits.HasPullback f f]
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.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}
[CategoryTheory.Category.{u_2, u_1} C]
{B : C}
{X : C}
(f : X ⟶ B)
[CategoryTheory.Limits.HasPullback f f]
[CategoryTheory.EffectiveEpi f]
:
An effective epi which has a kernel pair is a regular epi.
Equations
- One or more equations did not get rendered due to their size.