Theorems · Definition · category theory

CategoryTheory.Limits.evaluationCoconePointwiseProductIso

{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)) →
                  (X : D) →
                    (c : (i : α) → CategoryTheory.Limits.Cocone (F i)) →
                      ((CategoryTheory.evaluation D C).obj X).mapCocone
                          (CategoryTheory.Limits.coconePointwiseProduct c) ≅
                        (CategoryTheory.Limits.Cocone.precompose
                              (CategoryTheory.Limits.pointwiseProductCompEvaluation F X).hom).obj
                          (CategoryTheory.Limits.coconePointwiseProduct fun i =>
                            ((CategoryTheory.evaluation D C).obj X).mapCocone (c i))

In a functor category, coconePointwiseProduct commutes with evaluation.

Defined in

Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimitsOfShape