Theorems · Theorem · category theory

CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1} {ι' : Type u_2} [inst_3 : Finite ι]
  [inst_4 : Finite ι'] {S : C} {X : ι → C} {Y : ι' → C} (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S),
  CategoryTheory.IsPullback
    (CategoryTheory.Limits.Sigma.desc fun p =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f p.1) (g p.2))
        (CategoryTheory.Limits.Sigma.ι X p.1))
    (CategoryTheory.Limits.Sigma.desc fun p =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (f p.1) (g p.2))
        (CategoryTheory.Limits.Sigma.ι Y p.2))
    (CategoryTheory.Limits.Sigma.desc f) (CategoryTheory.Limits.Sigma.desc g)

If C has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite coproducts, i.e., ∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ). For a variant, see FinitaryPreExtensive.isIso_sigmaDesc_map.

Defined in

Mathlib.CategoryTheory.Extensive

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.FinitaryPreExtensiveFiniteFinite