Theorems · Theorem · category theory

CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y},
      CategoryTheory.IsUniversalColimit b →
        ∀ (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S)
          [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v] {P : ι × ι' → C}
          {q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i} {q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j},
          (∀ (i : ι) (j : ι'), CategoryTheory.IsPullback (q₁ i j) (q₂ i j) (f i) (g j)) →
            ∀ {Z : C} {p₁ : Z ⟶ a.pt} {p₂ : Z ⟶ b.pt},
              CategoryTheory.IsPullback p₁ p₂ u v →
                ∀ {d : CategoryTheory.Limits.Cofan P} (e : d.pt ≅ Z),
                  autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
                      CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_1 →
                    autoParam (∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i)
                        CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_3 →
                      autoParam
                          (∀ (i : ι) (j : ι'),
                            CategoryTheory.CategoryStruct.comp (d.inj (i, j))
                                (CategoryTheory.CategoryStruct.comp e.hom p₁) =
                              CategoryTheory.CategoryStruct.comp (q₁ i j) (a.inj i))
                          CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_5 →
                        autoParam
                            (∀ (i : ι) (j : ι'),
                              CategoryTheory.CategoryStruct.comp (d.inj (i, j))
                                  (CategoryTheory.CategoryStruct.comp e.hom p₂) =
                                CategoryTheory.CategoryStruct.comp (q₂ i j) (b.inj j))
                            CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_7 →
                          Nonempty (CategoryTheory.Limits.IsColimit d)

Pullbacks distribute over universal coproducts in both arguments: This is the isomorphism ∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ).

Defined in

Mathlib.CategoryTheory.Limits.VanKampen

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullback