Theorems · Definition · category theory

CategoryTheory.Limits.pullback.map

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z S T : C} →
      (f₁ : W ⟶ S) →
        (f₂ : X ⟶ S) →
          [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂] →
            (g₁ : Y ⟶ T) →
              (g₂ : Z ⟶ T) →
                [inst_2 : CategoryTheory.Limits.HasPullback g₁ g₂] →
                  (i₁ : W ⟶ Y) →
                    (i₂ : X ⟶ Z) →
                      (i₃ : S ⟶ T) →
                        CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁ →
                          CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂ →
                            (CategoryTheory.Limits.pullback f₁ f₂ ⟶ CategoryTheory.Limits.pullback g₁ g₂)

Given such a diagram, then there is a natural morphism W ×ₛ X ⟶ Y ×ₜ Z. `` W ⟶ Y ↘ ↘ S ⟶ T ↗ ↗ X ⟶ Z ``

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Cited by

156 results in Mathlib

Foundations

Depth 28 from the axioms, rests on 169 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullback