Theorems · Definition · category theory

CategoryTheory.unitOfTensorIsoUnit

{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) →
              (CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit M) →
                [F.Monoidal] → (F.obj m).comp (F.obj n) ≅ CategoryTheory.Functor.id C

If m ⊗ n ≅ 𝟙_M, then F.obj m is a left inverse of F.obj n.

Defined in

Mathlib.CategoryTheory.Monoidal.End

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.Functor.Monoidal