Theorems · Theorem · category theory

CategoryTheory.ShiftMkCore.assoc_inv_app

∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((h.F m₃).map ((h.add m₁ m₂).inv.app X)) ((h.add (m₁ + m₂) m₃).inv.app X) =
    CategoryTheory.CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).obj X))
      (CategoryTheory.CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X) (CategoryTheory.eqToHom ⋯))

Defined in

Mathlib.CategoryTheory.Shift.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoid