Theorems · Definition · category theory

CategoryTheory.Limits.coequalizer.desc

{C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] →
          {W : C} →
            (k : Y ⟶ W) →
              CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k →
                (CategoryTheory.Limits.coequalizer f g ⟶ W)

Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k factors through the coequalizer of f and g via coequalizer.desc : coequalizer f g ⟶ W.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Cited by

37 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCoequalizer