Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.mk.noConfusion

{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} →
                {P : Sort u} →
                  {π : (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)))} →
                          {π' :
                              (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)))} →
                                  { π := π, hπ := hπ, isLimitWedge := isLimitWedge, map_comp_π := map_comp_π } =
                                      { π := π', hπ := hπ', isLimitWedge := isLimitWedge', map_comp_π := map_comp_π' } →
                                    (π ≍ π' → isLimitWedge ≍ isLimitWedge' → P) → P

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Cited by

1 results in Mathlib

Foundations

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