Theorems · Definition · category theory

CategoryTheory.Limits.pullbackDiagonalMapIdIso

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasPullbacks C] →
        {S T : C} →
          (f : X ⟶ T) →
            (g : Y ⟶ T) →
              (i : T ⟶ S) →
                [inst_2 : CategoryTheory.Limits.HasPullback i i] →
                  [inst_3 : CategoryTheory.Limits.HasPullback f g] →
                    [inst_4 :
                        CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i)
                          (CategoryTheory.CategoryStruct.comp g i)] →
                      [inst_5 :
                          CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
                            (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
                              (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯
                              ⋯)] →
                        CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal i)
                            (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
                              (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯
                              ⋯) ≅
                          CategoryTheory.Limits.pullback f g

This iso witnesses the fact that given f : X ⟶ T, g : Y ⟶ T, and i : T ⟶ S, the diagram `` X ×ₜ Y ⟶ X ×ₛ Y | | | | ↓ ↓ T ⟶ T ×ₛ T ` is a pullback square. Also see pullback_map_diagonal_isPullback`.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Cited by

16 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullback