Theorems · Theorem · category theory

CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone

∀ {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]
          (s : (i : ι) → (j : ι') → CategoryTheory.Limits.PullbackCone (f i) (g j))
          (hs : (i : ι) → (j : ι') → CategoryTheory.Limits.IsLimit (s i j)) (t : CategoryTheory.Limits.PullbackCone u v)
          (ht : CategoryTheory.Limits.IsLimit t) {d : CategoryTheory.Limits.Cofan fun p => (s p.1 p.2).pt}
          (e : d.pt ≅ t.pt),
          autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
              CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._auto_1 →
            autoParam (∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i)
                CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._auto_3 →
              autoParam
                  (∀ (i : ι) (j : ι'),
                    CategoryTheory.CategoryStruct.comp (d.inj (i, j)) (CategoryTheory.CategoryStruct.comp e.hom t.fst) =
                      CategoryTheory.CategoryStruct.comp (s (i, j).1 (i, j).2).fst (a.inj (i, j).1))
                  CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._auto_5 →
                autoParam
                    (∀ (i : ι) (j : ι'),
                      CategoryTheory.CategoryStruct.comp (d.inj (i, j))
                          (CategoryTheory.CategoryStruct.comp e.hom t.snd) =
                        CategoryTheory.CategoryStruct.comp (s (i, j).1 (i, j).2).snd (b.inj (i, j).2))
                    CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone._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 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullback