Theorems · Theorem · category theory

CategoryTheory.Limits.Pi.map_eq_prod_map

∀ {C : Type u_1} {I : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : I → C} (f : (i : I) → X i ⟶ Y i)
  (P : I → Prop) [inst_1 : CategoryTheory.Limits.HasProduct X] [inst_2 : CategoryTheory.Limits.HasProduct Y]
  [inst_3 : CategoryTheory.Limits.HasProduct fun i => X ↑i] [inst_4 : CategoryTheory.Limits.HasProduct fun i => X ↑i]
  [inst_5 : CategoryTheory.Limits.HasProduct fun i => Y ↑i] [inst_6 : CategoryTheory.Limits.HasProduct fun i => Y ↑i]
  [inst_7 : (i : I) → Decidable (P i)],
  CategoryTheory.Limits.Pi.map f =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso
          (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map (CategoryTheory.Limits.Pi.map fun i => f ↑i)
          (CategoryTheory.Limits.Pi.map fun i => f ↑i))
        ((CategoryTheory.Limits.Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso
            (CategoryTheory.Limits.prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).inv)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.PiProd

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasProductCategoryTheory.Limits.HasProductCategoryTheory.Limits.HasProductCategoryTheory.Limits.HasProductCategoryTheory.Limits.HasProductCategoryTheory.Limits.HasProductDecidable