Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.mk.inj

∀ {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

1 results in Mathlib

Foundations

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