Effective epimorphisms in a slice category #
An effective epimorphism remains effective when regarded as a morphism over a fixed base. Descent on underlying objects respects the structure morphisms by epimorphism cancellation. No pullbacks are required. This lets descent on carriers be used for group schemes.
instance
CategoryTheory.Over.effectiveEpi_of_effectiveEpi_left
{C : Type u_1}
[Category.{v_1, u_1} C]
{S : C}
{X Y : Over S}
(f : X ⟶ Y)
[EffectiveEpi (Hom.left f)]
:
A morphism in a slice category is effective epi if its underlying morphism is.