Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.mk.noConfusion

{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.MonoidalCategoryStruct C} →
          {P : Sort u} →
            {actionObj : D → C → D} →
              {actionHomRight : (d : D) → {c c' : C} → (c ⟶ c') → (actionObj d c ⟶ actionObj d c')} →
                {actionHomLeft : {d d' : D} → (d ⟶ d') → (c : C) → actionObj d c ⟶ actionObj d' c} →
                  {actionHom : {c c' : C} → {d d' : D} → (d ⟶ d') → (c ⟶ c') → (actionObj d c ⟶ actionObj d' c')} →
                    {actionAssocIso :
                        (d : D) →
                          (c c' : C) →
                            actionObj d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') ≅
                              actionObj (actionObj d c) c'} →
                      {actionUnitIso : (d : D) → actionObj d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ d} →
                        {actionObj' : D → C → D} →
                          {actionHomRight' : (d : D) → {c c' : C} → (c ⟶ c') → (actionObj' d c ⟶ actionObj' d c')} →
                            {actionHomLeft' : {d d' : D} → (d ⟶ d') → (c : C) → actionObj' d c ⟶ actionObj' d' c} →
                              {actionHom' :
                                  {c c' : C} → {d d' : D} → (d ⟶ d') → (c ⟶ c') → (actionObj' d c ⟶ actionObj' d' c')} →
                                {actionAssocIso' :
                                    (d : D) →
                                      (c c' : C) →
                                        actionObj' d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') ≅
                                          actionObj' (actionObj' d c) c'} →
                                  {actionUnitIso' :
                                      (d : D) → actionObj' d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ d} →
                                    { actionObj := actionObj, actionHomRight := actionHomRight,
                                          actionHomLeft := actionHomLeft, actionHom := actionHom,
                                          actionAssocIso := actionAssocIso, actionUnitIso := actionUnitIso } =
                                        { actionObj := actionObj', actionHomRight := actionHomRight',
                                          actionHomLeft := actionHomLeft', actionHom := actionHom',
                                          actionAssocIso := actionAssocIso', actionUnitIso := actionUnitIso' } →
                                      (actionObj ≍ actionObj' →
                                          actionHomRight ≍ actionHomRight' →
                                            actionHomLeft ≍ actionHomLeft' →
                                              actionHom ≍ actionHom' →
                                                actionAssocIso ≍ actionAssocIso' → actionUnitIso ≍ actionUnitIso' → P) →
                                        P

Defined in

Mathlib.CategoryTheory.Monoidal.Action.Basic

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms