Theorems · Theorem · category theory

CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp C} (e : G.X ≅ H.X)
  (one_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
      _auto_105✝)
  (mul_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
          CategoryTheory.MonObj.mul)
      _auto_107✝),
  (CategoryTheory.CommGrp.mkIso e one_f mul_f).inv.hom.hom.hom = e.inv

Defined in

Mathlib.CategoryTheory.Monoidal.CommGrp_

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.BraidedCategory