Theorems · Definition · category theory

CategoryTheory.Limits.isEqualizerCompMono

{C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {c : CategoryTheory.Limits.Fork f g} →
          CategoryTheory.Limits.IsLimit c →
            {Z : C} →
              (h : Y ⟶ Z) →
                [hm : CategoryTheory.Mono h] →
                  have this := ⋯;
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι c.ι ⋯)

The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Mono