Theorems · Theorem · category theory

CategoryTheory.Limits.pointwiseProductCompEvaluation_hom_app

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4}
  [inst_2 : (i : α) → CategoryTheory.Category.{u_5, u_4} (I i)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (F : (i : α) → CategoryTheory.Functor (I i) (CategoryTheory.Functor D C)) (d : D) (X : (i : α) → I i),
  (CategoryTheory.Limits.pointwiseProductCompEvaluation F d).hom.app X =
    (CategoryTheory.Limits.piObjIso ((CategoryTheory.Functor.pi F).obj X) d).hom

Defined in

Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimitsOfShape