Theorems · Theorem · category theory

CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ B)
      (q₂ : (i : ι) → P i ⟶ X i),
      (∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) v (f i)) →
        ∀ {d : CategoryTheory.Limits.Cofan P} (hd : CategoryTheory.Limits.IsColimit d),
          autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
              CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left._auto_1 →
            ∀ [CategoryTheory.Limits.HasPullback v u],
              CategoryTheory.IsPullback (CategoryTheory.Limits.Cofan.IsColimit.desc hd q₁)
                (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun x =>
                  CategoryTheory.CategoryStruct.comp (q₂ x) (a.inj x))
                v u

Pullbacks distribute over universal coproducts on the left: This is the isomorphism ∐ (B ×[S] Xᵢ) ≅ B ×[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