Theorems · Theorem · category theory

CategoryTheory.AddGrpObj.isPullback

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.AddGrpObj A],
  CategoryTheory.IsPullback (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.AddMonObj.add A)
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.AddMonObj.add))
    CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add

The associativity diagram of an additive group object is Cartesian. In fact, any additive monoid object whose associativity diagram is Cartesian can be made into an additive group object (we do not prove this in this file), so we should expect that many properties of additive group objects follow from this result.

Defined in

Mathlib.CategoryTheory.Monoidal.Grp

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.AddGrpObj