Theorems · Definition · category theory

CategoryTheory.Limits.equalizerPullbackMapIso

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasEqualizers C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y S T : C} →
          {f g : X ⟶ Y} →
            {s : X ⟶ S} →
              {t : Y ⟶ S} →
                (hf : CategoryTheory.CategoryStruct.comp f t = s) →
                  (hg : CategoryTheory.CategoryStruct.comp g t = s) →
                    (v : T ⟶ S) →
                      CategoryTheory.Limits.equalizer
                          (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
                          (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                            (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) ≅
                        CategoryTheory.Limits.pullback (CategoryTheory.Limits.equalizer.ι f g)
                          (CategoryTheory.Limits.pullback.fst s v)

The natural isomorphism eq(f ×[S] T, g ×[S] T) ≅ eq(f, g) ×[S] T.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasEqualizersCategoryTheory.Limits.HasPullbacks