Theorems · Theorem · category theory

CategoryTheory.pullbackShiftFunctorZero_inv_app

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (X : CategoryTheory.PullbackShift C φ),
  (CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C B).inv.app X)
      ((CategoryTheory.pullbackShiftIso C φ 0 0 ⋯).inv.app X)

Defined in

Mathlib.CategoryTheory.Shift.Pullback

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryAddMonoidAddMonoidCategoryTheory.HasShift