Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.MonoidalRightAction.casesOn

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          {motive : CategoryTheory.MonoidalCategory.MonoidalRightAction C D → Sort u} →
            (t : CategoryTheory.MonoidalCategory.MonoidalRightAction C D) →
              ([toMonoidalRightActionStruct : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
                  (actionHom_def :
                      ∀ {c c' : C} {d d' : D} (f : d ⟶ d') (g : c ⟶ c'),
                        CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)
                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d' g)) →
                    (actionHomRight_id :
                        ∀ (c : C) (d : D),
                          CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                              (CategoryTheory.CategoryStruct.id c) =
                            CategoryTheory.CategoryStruct.id
                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)) →
                      (id_actionHomLeft :
                          ∀ (c : C) (d : D),
                            CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                (CategoryTheory.CategoryStruct.id d) c =
                              CategoryTheory.CategoryStruct.id
                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)) →
                        (actionHom_comp :
                            ∀ {c c' c'' : C} {d d' d'' : D} (f₁ : d ⟶ d') (f₂ : d' ⟶ d'') (g₁ : c ⟶ c') (g₂ : c' ⟶ c''),
                              CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
                                  (CategoryTheory.CategoryStruct.comp f₁ f₂)
                                  (CategoryTheory.CategoryStruct.comp g₁ g₂) =
                                CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₁ g₁)
                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f₂ g₂)) →
                          (actionAssocIso_hom_naturality :
                              ∀ {d₁ d₂ : D} {c₁ c₂ c₃ c₄ : C} (f : d₁ ⟶ d₂) (g : c₁ ⟶ c₂) (h : c₃ ⟶ c₄),
                                CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f
                                      (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₂ c₂
                                        c₄).hom =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d₁ c₁
                                        c₃).hom
                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g) h)) →
                            (actionUnitIso_hom_naturality :
                                ∀ {d d' : D} (f : d ⟶ d'),
                                  CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom
                                      f =
                                    CategoryTheory.CategoryStruct.comp
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
                                        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                          d').hom) →
                              (actionHomRight_whiskerRight :
                                  ∀ {c' c'' : C} (f : c' ⟶ c'') (c : C) (d : D),
                                    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c) =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c'
                                            c).hom
                                        (CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                              f)
                                            c)
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                              c'' c).inv)) →
                                (whiskerRight_actionHomLeft :
                                    ∀ (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D),
                                      CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
                                              c').hom
                                          (CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)
                                              f)
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                                c c'').inv)) →
                                  (actionHom_associator :
                                      ∀ (c₁ c₂ c₃ : C) (d : D),
                                        CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                              (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom)
                                            (CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                                  d c₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃)).hom
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                                  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                                                    c₁)
                                                  c₂ c₃).hom) =
                                          CategoryTheory.CategoryStruct.comp
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
                                                (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃).hom
                                            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                                  d c₁ c₂).hom
                                              c₃)) →
                                    (actionHom_leftUnitor :
                                        ∀ (c : C) (d : D),
                                          CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                              (CategoryTheory.MonoidalCategoryStruct.leftUnitor c).hom =
                                            CategoryTheory.CategoryStruct.comp
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                                  d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) c).hom
                                              (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
                                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                                    d).hom
                                                c)) →
                                      (actionHom_rightUnitor :
                                          ∀ (c : C) (d : D),
                                            CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
                                                (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom =
                                              CategoryTheory.CategoryStruct.comp
                                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
                                                    d c (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
                                                (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
                                                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
                                                      d c)).hom) →
                                        motive
                                          { toMonoidalRightActionStruct := toMonoidalRightActionStruct,
                                            actionHom_def := actionHom_def, actionHomRight_id := actionHomRight_id,
                                            id_actionHomLeft := id_actionHomLeft, actionHom_comp := actionHom_comp,
                                            actionAssocIso_hom_naturality := actionAssocIso_hom_naturality,
                                            actionUnitIso_hom_naturality := actionUnitIso_hom_naturality,
                                            actionHomRight_whiskerRight := actionHomRight_whiskerRight,
                                            whiskerRight_actionHomLeft := whiskerRight_actionHomLeft,
                                            actionHom_associator := actionHom_associator,
                                            actionHom_leftUnitor := actionHom_leftUnitor,
                                            actionHom_rightUnitor := actionHom_rightUnitor }) →
                motive t

Defined in

Mathlib.CategoryTheory.Monoidal.Action.Basic

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory