Documentation

Mathlib.CategoryTheory.EffectiveEpi.RegularEpi

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.

The data of an EffectiveEpi structure on a RegularEpi.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A morphism which is a coequalizer for its kernel pair is an effective epi.

    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.