Theorems · Definition · category theory

CategoryTheory.isColimitOfEffectiveEpiStruct

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : Y ⟶ X) →
        CategoryTheory.EffectiveEpiStruct f →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Sieve.generateSingleton f).arrows.cocone

Implementation: This is a construction which will be used in the proof that the sieve generated by a single arrow is effective epimorphic if and only if the arrow is an effective epi.

Defined in

Mathlib.CategoryTheory.Sites.EffectiveEpimorphic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category