Theorems · Definition · category theory

CategoryTheory.Functor.LaxRightLinear.casesOn

{D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] →
                    {motive : F.LaxRightLinear C → Sort u} →
                      (t : F.LaxRightLinear C) →
                        ((μᵣ :
                              (d : D) →
                                (c : C) →
                                  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c ⟶
                                    F.obj (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)) →
                            (μᵣ_naturality_right :
                                ∀ (d : D) {c c' : C} (f : c ⟶ c'),
                                  CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight
                                        (F.obj d) f)
                                      (μᵣ d c') =
                                    CategoryTheory.CategoryStruct.comp (μᵣ d c)
                                      (F.map
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                          f))) →
                              (μᵣ_naturality_left :
                                  ∀ {d d' : D} (f : d ⟶ d') (c : C),
                                    CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                          (F.map f) c)
                                        (μᵣ d' c) =
                                      CategoryTheory.CategoryStruct.comp (μᵣ d c)
                                        (F.map
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
                                            c))) →
                                (μᵣ_associativity :
                                    ∀ (d : D) (c c' : C),
                                      CategoryTheory.CategoryStruct.comp
                                          (μᵣ d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
                                          (F.map
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                                c c').hom) =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                              (F.obj d) c c').hom
                                          (CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                              (μᵣ d c) c')
                                            (μᵣ
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
                                              c'))) →
                                  (μᵣ_unitality :
                                      ∀ (d : D),
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                              (F.obj d)).hom =
                                          CategoryTheory.CategoryStruct.comp
                                            (μᵣ d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                            (F.map
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                                  d).hom)) →
                                    motive
                                      { μᵣ := μᵣ, μᵣ_naturality_right := μᵣ_naturality_right,
                                        μᵣ_naturality_left := μᵣ_naturality_left, μᵣ_associativity := μᵣ_associativity,
                                        μᵣ_unitality := μᵣ_unitality }) →
                          motive t

Defined in

Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategory.MonoidalRightActionCategoryTheory.MonoidalCategory.MonoidalRightAction