Theorems · Theorem · category theory

CategoryTheory.TwistShiftData.mk.inj

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : Type w} {inst_1 : AddMonoid A}
  {inst_2 : CategoryTheory.HasShift C A} {z : A → A → (CategoryTheory.CatCenter C)ˣ}
  {z_zero_zero : autoParam (z 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam}
  {assoc :
    autoParam (∀ (a b c : A), z (a + b) c * z a b = z a (b + c) * z b c) CategoryTheory.TwistShiftData.assoc._autoParam}
  {commShift :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam}
  {z_1 : A → A → (CategoryTheory.CatCenter C)ˣ}
  {z_zero_zero_1 : autoParam (z_1 0 0 = 1) CategoryTheory.TwistShiftData.z_zero_zero._autoParam}
  {assoc_1 :
    autoParam (∀ (a b c : A), z_1 (a + b) c * z_1 a b = z_1 a (b + c) * z_1 b c)
      CategoryTheory.TwistShiftData.assoc._autoParam}
  {commShift_1 :
    autoParam (∀ (a b : A), CategoryTheory.NatTrans.CommShift (↑(z_1 a b)) A)
      CategoryTheory.TwistShiftData.commShift._autoParam},
  { z := z, z_zero_zero := z_zero_zero, assoc := assoc, commShift := commShift } =
      { z := z_1, z_zero_zero := z_zero_zero_1, assoc := assoc_1, commShift := commShift_1 } →
    z = z_1

Defined in

Mathlib.CategoryTheory.Shift.Twist

Cited by

1 results in Mathlib

Foundations

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