Theorems · Definition · category theory

CategoryTheory.AddGrp.mkIso

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {G H : CategoryTheory.AddGrp C} →
        (e : G.X ≅ H.X) →
          autoParam
              (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero)
              CategoryTheory.AddGrp.mkIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                    CategoryTheory.AddMonObj.add)
                CategoryTheory.AddGrp.mkIso._auto_3 →
              (G ≅ H)

Construct an isomorphism of additive group objects by giving an isomorphism between the underlying objects and checking compatibility with zero and addition only in the forward direction.

Defined in

Mathlib.CategoryTheory.Monoidal.Grp

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategory