Theorems · Definition · category theory

CategoryTheory.Limits.weakPullback.map

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z S T : C} →
      (f₁ : W ⟶ S) →
        (f₂ : X ⟶ S) →
          [inst_1 : CategoryTheory.Limits.HasWeakPullback f₁ f₂] →
            (g₁ : Y ⟶ T) →
              (g₂ : Z ⟶ T) →
                [inst_2 : CategoryTheory.Limits.HasWeakPullback 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.weakPullback f₁ f₂ ⟶ CategoryTheory.Limits.weakPullback g₁ g₂)

Given such a diagram, then there is a natural morphism from the weak pullback of W ⟶ S and X ⟶ S to the weak pullback of Y ⟶ T and Z ⟶ T. `` W ⟶ Y ↘ ↘ S ⟶ T ↗ ↗ X ⟶ Z ``

Defined in

Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasWeakPullbackCategoryTheory.Limits.HasWeakPullback