Theorems · Theorem · category theory

CategoryTheory.Limits.equalizer.hom_ext

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

Two maps into an equalizer are equal if they are equal when composed with the equalizer map.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Cited by

27 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasEqualizer