Theorems · Theorem · category theory

CategoryTheory.AddGrpObj.eq_lift_neg_right

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f g h : A ⟶ B),
  f =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift g
          (CategoryTheory.CategoryStruct.comp h CategoryTheory.AddGrpObj.neg))
        CategoryTheory.AddMonObj.add ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h)
        CategoryTheory.AddMonObj.add =
      g

Defined in

Mathlib.CategoryTheory.Monoidal.Grp

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.AddGrpObj