Theorems · Definition · category theory

CategoryTheory.Mon.mkIso

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Mon C} →
        (e : M.X ≅ N.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
              CategoryTheory.Mon.mkIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                    CategoryTheory.MonObj.mul)
                CategoryTheory.Mon.mkIso._auto_3 →
              (M ≅ N)

Construct an isomorphism of monoid objects by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

Defined in

Mathlib.CategoryTheory.Monoidal.Mon

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory