Theorems · Theorem · category theory

CategoryTheory.Limits.Cotrident.coequalizer_ext

∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J]
  (s : CategoryTheory.Limits.Cotrident f) {W : C} {k l : s.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l →
    ∀ (j : CategoryTheory.Limits.WalkingParallelFamily J),
      CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l

To check whether two maps are coequalized by both maps of a cotrident, it suffices to check it for the second map

Defined in

Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryNonempty