Theorems · Definition · category theory

CategoryTheory.Grp.mkIso

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : CategoryTheory.Grp C} →
        (e : G.X ≅ H.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
              CategoryTheory.Grp.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.Grp.mkIso._auto_3 →
              (G ≅ H)

Construct an isomorphism of group 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.Grp

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategory