Theorems · Theorem · category theory

CategoryTheory.GrpObj.isPullback

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

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

Defined in

Mathlib.CategoryTheory.Monoidal.Grp

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CartesianMonoidalCategoryCategoryTheory.GrpObj