Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.ofTensorHom

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategoryStruct C] →
      autoParam
          (∀ (X₁ X₂ : C),
            CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₁)
                (CategoryTheory.CategoryStruct.id X₂) =
              CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
          CategoryTheory.MonoidalCategory.ofTensorHom._auto_1 →
        autoParam
            (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
              CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) f =
                CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
            CategoryTheory.MonoidalCategory.ofTensorHom._auto_3 →
          autoParam
              (∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
                CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id Y) =
                  CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
              CategoryTheory.MonoidalCategory.ofTensorHom._auto_5 →
            autoParam
                (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
                      (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
                    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
                      (CategoryTheory.CategoryStruct.comp f₂ g₂))
                CategoryTheory.MonoidalCategory.ofTensorHom._auto_7 →
              autoParam
                  (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
                    CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) f₃)
                        (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
                        (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom f₂ f₃)))
                  CategoryTheory.MonoidalCategory.ofTensorHom._auto_9 →
                autoParam
                    (∀ {X Y : C} (f : X ⟶ Y),
                      CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom
                            (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) f)
                          (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f)
                    CategoryTheory.MonoidalCategory.ofTensorHom._auto_11 →
                  autoParam
                      (∀ {X Y : C} (f : X ⟶ Y),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom f
                              (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
                            (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom =
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
                            f)
                      CategoryTheory.MonoidalCategory.ofTensorHom._auto_13 →
                    autoParam
                        (∀ (W X Y Z : C),
                          CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.tensorHom
                                (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
                                (CategoryTheory.CategoryStruct.id Z))
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.associator W
                                    (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
                                (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
                                  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.associator
                                  (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).hom
                              (CategoryTheory.MonoidalCategoryStruct.associator W X
                                  (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom)
                        CategoryTheory.MonoidalCategory.ofTensorHom._auto_15 →
                      autoParam
                          (∀ (X Y : C),
                            CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.associator X
                                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y).hom
                                (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X)
                                  (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) =
                              CategoryTheory.MonoidalCategoryStruct.tensorHom
                                (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
                                (CategoryTheory.CategoryStruct.id Y))
                          CategoryTheory.MonoidalCategory.ofTensorHom._auto_17 →
                        CategoryTheory.MonoidalCategory C

A constructor for monoidal categories that requires tensorHom instead of whiskerLeft and whiskerRight.

Defined in

Mathlib.CategoryTheory.Monoidal.Category

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryStruct