Theorems · Definition · category theory

CategoryTheory.isColimitCoforkOfEffectiveEpi

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B X : C} →
      (f : X ⟶ B) →
        [CategoryTheory.EffectiveEpi f] →
          (c : CategoryTheory.Limits.PullbackCone f f) →
            CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯)

Given a kernel pair of an effective epimorphism f : X ⟶ B, the induced cofork is a coequalizer.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Cited by

2 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.EffectiveEpi