Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.mk.injEq

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (π : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))
  (hπ :
    ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π c i)
          ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
            (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))))
  (isLimitWedge : (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π c) ⋯))
  (map_comp_π :
    ∀ {c c' : C} (f : c ⟶ c') (j : C),
      CategoryTheory.CategoryStruct.comp (H.map f) (π c' j) =
        CategoryTheory.CategoryStruct.comp (π c j)
          ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f))))
  (π_1 : (c j : C) → H.obj c ⟶ F.obj j ⟹ G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))
  (hπ_1 :
    ∀ (c : C) ⦃i j : C⦄ (f : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (π_1 c i)
          ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
        CategoryTheory.CategoryStruct.comp (π_1 c j)
          ((CategoryTheory.MonoidalClosed.pre (F.map f)).app
            (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c))))
  (isLimitWedge_1 : (c : C) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Wedge.mk (H.obj c) (π_1 c) ⋯))
  (map_comp_π_1 :
    ∀ {c c' : C} (f : c ⟶ c') (j : C),
      CategoryTheory.CategoryStruct.comp (H.map f) (π_1 c' j) =
        CategoryTheory.CategoryStruct.comp (π_1 c j)
          ((CategoryTheory.ihom (F.obj j)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft j f)))),
  ({ π := π, hπ := hπ, isLimitWedge := isLimitWedge, map_comp_π := map_comp_π } =
      { π := π_1, hπ := hπ_1, isLimitWedge := isLimitWedge_1, map_comp_π := map_comp_π_1 }) =
    (π = π_1 ∧ isLimitWedge ≍ isLimitWedge_1)

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosed