Theorems · Definition · category theory

CategoryTheory.equivOfTensorIsoUnit

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} M] →
        [inst_2 : CategoryTheory.MonoidalCategory M] →
          (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) →
            (m n : M) →
              (h₁ :
                  CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit M) →
                (h₂ :
                    CategoryTheory.MonoidalCategoryStruct.tensorObj n m ≅
                      CategoryTheory.MonoidalCategoryStruct.tensorUnit M) →
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₁.hom m)
                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor m).hom =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator m n m).hom
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m h₂.hom)
                          (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).hom) →
                    [F.Monoidal] → C ≌ C

If m ⊗ n ≅ 𝟙_M and n ⊗ m ≅ 𝟙_M (subject to some commuting constraints), then F.obj m and F.obj n forms a self-equivalence of C.

Defined in

Mathlib.CategoryTheory.Monoidal.End

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Functor.Monoidal