Loogle!

Result

Found 52 declarations mentioning CategoryTheory.shiftFunctorCompIsoId.

CategoryTheory.shiftFunctorCompIsoId 📋 Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddMonoid A] [CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0) : (CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C j) ≅ CategoryTheory.Functor.id C
CategoryTheory.shiftEquiv'_counitIso 📋 Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0) : (CategoryTheory.shiftEquiv' C i j h).counitIso = CategoryTheory.shiftFunctorCompIsoId C j i ⋯
CategoryTheory.shiftEquiv'_unitIso 📋 Mathlib.CategoryTheory.Shift.Basic
(C : Type u) {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0) : (CategoryTheory.shiftEquiv' C i j h).unitIso = (CategoryTheory.shiftFunctorCompIsoId C i j h).symm
CategoryTheory.shift_shiftFunctorCompIsoId_hom_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n m : A) (h : n + m = 0) (X : C) : (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.shift_shiftFunctorCompIsoId_inv_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n m : A) (h : n + m = 0) (X : C) : (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_cancel_hom_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.shift_shiftFunctorCompIsoId_add_neg_cancel_inv_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)
CategoryTheory.shiftFunctorCompIsoId_naturality_1 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A) (hij : i + j = 0) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i j hij).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f)) ((CategoryTheory.shiftFunctorCompIsoId C i j hij).hom.app Y)) = f
CategoryTheory.shiftFunctorComm_hom_app_of_add_eq_zero 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C) : (CategoryTheory.shiftFunctorComm C m n).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).hom.app X) ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).inv.app X)
CategoryTheory.shiftFunctorComm_inv_app_of_add_eq_zero 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C) : (CategoryTheory.shiftFunctorComm C m n).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).hom.app X) ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).inv.app X)
CategoryTheory.shiftFunctorCompIsoId_naturality_1_assoc 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A) (hij : i + j = 0) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i j hij).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i j hij).hom.app Y) h)) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C (-n)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((CategoryTheory.shiftFunctor C (-n)).obj X)
CategoryTheory.shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (n : A) (X : C) : (CategoryTheory.shiftFunctor C (-n)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((CategoryTheory.shiftFunctor C (-n)).obj X)
CategoryTheory.shiftFunctorComm_hom_app_of_add_eq_zero_assoc 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C m).obj ((CategoryTheory.shiftFunctor C n).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m n).hom.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).inv.app X) h)
CategoryTheory.shiftFunctorComm_inv_app_of_add_eq_zero_assoc 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddCommMonoid A] [CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.shiftFunctor C m).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m n).inv.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).inv.app X) h)
CategoryTheory.shift_shift_neg' 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i : A) : (CategoryTheory.shiftFunctor C (-i)).map ((CategoryTheory.shiftFunctor C i).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).inv.app Y))
CategoryTheory.shiftFunctorCompIsoId_zero_zero_inv_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (X : C) : (CategoryTheory.shiftFunctorCompIsoId C 0 0 ⋯).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).inv.app X) ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
CategoryTheory.shift_neg_shift' 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i : A) : (CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C (-i)).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).inv.app Y))
CategoryTheory.shiftFunctorCompIsoId_zero_zero_hom_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} (A : Type u_1) [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] (X : C) : (CategoryTheory.shiftFunctorCompIsoId C 0 0 ⋯).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero C A).hom.app X)) ((CategoryTheory.shiftFunctorZero C A).hom.app X)
CategoryTheory.shiftFunctorCompIsoId_add'_hom_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X : C} (m n p m' n' p' : A) (hm : m' + m = 0) (hn : n' + n = 0) (hp : p' + p = 0) (h : m + n = p) : (CategoryTheory.shiftFunctorCompIsoId C p' p hp).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' C n' m' p' ⋯).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C m n p h).hom.app ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C n').obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C m' m hm).hom.app ((CategoryTheory.shiftFunctor C n').obj X))) ((CategoryTheory.shiftFunctorCompIsoId C n' n hn).hom.app X)))
CategoryTheory.shiftFunctorCompIsoId_add'_inv_app 📋 Mathlib.CategoryTheory.Shift.Basic
{C : Type u} {A : Type u_1} [CategoryTheory.Category.{v, u} C] [AddGroup A] [CategoryTheory.HasShift C A] {X : C} (m n p m' n' p' : A) (hm : m' + m = 0) (hn : n' + n = 0) (hp : p' + p = 0) (h : m + n = p) : (CategoryTheory.shiftFunctorCompIsoId C p' p hp).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n' n hn).inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C m' m hm).inv.app ((CategoryTheory.shiftFunctor C n').obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C m n p h).inv.app ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C n').obj X))) ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' C n' m' p' ⋯).inv.app X))))
CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app 📋 Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) : F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app X)) ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)))
CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app 📋 Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) : F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).inv.app X)) ((CategoryTheory.Functor.commShiftIso F b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)))
CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app_assoc 📋 Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) {Z : D} (h✝ : F.obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X)) h✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) h✝))
CategoryTheory.Functor.map_shiftFunctorCompIsoId_inv_app_assoc 📋 Mathlib.CategoryTheory.Shift.CommShift
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {A : Type u_4} [AddMonoid A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) {Z : D} (h✝ : F.obj ((CategoryTheory.shiftFunctor C b).obj ((CategoryTheory.shiftFunctor C a).obj X)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app X)) h✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).inv.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F b).inv.app ((CategoryTheory.shiftFunctor C a).obj X)) h✝))
CategoryTheory.Pretriangulated.Triangle.invRotate_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : T.invRotate.mor₃ = CategoryTheory.CategoryStruct.comp T.mor₂ ((CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3)
CategoryTheory.Pretriangulated.rotCompInvRot_hom_app_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) : (CategoryTheory.Pretriangulated.rotCompInvRot.hom.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X.obj₁
CategoryTheory.Pretriangulated.rotCompInvRot_inv_app_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) : (CategoryTheory.Pretriangulated.rotCompInvRot.inv.app X).hom₁ = (CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X.obj₁
CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) : (CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app X.obj₃
CategoryTheory.Pretriangulated.invRotCompRot_inv_app_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : CategoryTheory.Pretriangulated.Triangle C) : (CategoryTheory.Pretriangulated.invRotCompRot.inv.app X).hom₃ = (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app X.obj₃
CategoryTheory.Pretriangulated.Triangle.invRotate_mor₁ 📋 Mathlib.CategoryTheory.Triangulated.Rotate
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : T.invRotate.mor₁ = -CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C (-1)).map T.mor₃) ((CategoryTheory.shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁)
CategoryTheory.Functor.shiftIso_hom_app_comp_shiftMap_of_add_eq_zero 📋 Mathlib.CategoryTheory.Shift.ShiftSequence
{C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {G : Type u_5} [AddGroup G] [CategoryTheory.HasShift C G] [F.ShiftSequence G] {X Y : C} {m : G} (f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y) (n : G) (hnm : n + m = 0) (a a' : G) (ha' : m + a = a') : CategoryTheory.CategoryStruct.comp ((F.shiftIso n a' a ⋯).hom.app X) (F.shiftMap f a a' ha') = (F.shift a').map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map f) ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app Y))
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app_assoc 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (X : C) {Z : D} (h✝ : (CategoryTheory.shiftFunctor D a).obj (F.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).hom.app X) h✝ = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X))) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X))))) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.Functor.commShiftIso G b).hom.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X))))) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C b a ⋯).hom.app (G.obj ((CategoryTheory.shiftFunctor D a).obj (F.obj X))))) (CategoryTheory.CategoryStruct.comp (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X))) h✝))))
CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app_assoc 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (Y : D) {Z : C} (h✝ : G.obj ((CategoryTheory.shiftFunctor D a).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).inv.app Y) h✝ = CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj (G.obj Y))) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctorCompIsoId D b a h).inv.app (F.obj ((CategoryTheory.shiftFunctor C a).obj (G.obj Y))))) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app (G.obj Y))))) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y))))) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y))) h✝))))
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (X : C) : (CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).hom.app X = CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X))) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X))))) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.Functor.commShiftIso G b).hom.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X))))) (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C b a ⋯).hom.app (G.obj ((CategoryTheory.shiftFunctor D a).obj (F.obj X))))) (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X))))))
CategoryTheory.Adjunction.RightAdjointCommShift.iso_inv_app 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (Y : D) : (CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).inv.app Y = CategoryTheory.CategoryStruct.comp (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj (G.obj Y))) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctorCompIsoId D b a h).inv.app (F.obj ((CategoryTheory.shiftFunctor C a).obj (G.obj Y))))) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app (G.obj Y))))) (CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app (F.obj (G.obj Y))))) (G.map ((CategoryTheory.shiftFunctor D a).map (adj.counit.app Y))))))
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app_assoc 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (Y : C) {Z : D} (h✝ : F.obj ((CategoryTheory.shiftFunctor C a).obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).inv.app Y) h✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app Y))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.shiftFunctor C b).map (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj Y))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.Functor.commShiftIso G b).inv.app (F.obj ((CategoryTheory.shiftFunctor C a).obj Y))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (adj.counit.app ((CategoryTheory.shiftFunctor D b).obj (F.obj ((CategoryTheory.shiftFunctor C a).obj Y))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((CategoryTheory.shiftFunctor C a).obj Y))) h✝))))
CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app_assoc 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (X : D) {Z : C} (h✝ : (CategoryTheory.shiftFunctor C a).obj (G.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).hom.app X) h✝ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C b a h).inv.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (adj.unit.app ((CategoryTheory.shiftFunctor C b).obj (G.obj ((CategoryTheory.shiftFunctor D a).obj X))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.Functor.commShiftIso F b).hom.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.shiftFunctor D b).map (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj X))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app X))) h✝))))
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [G.CommShift A] (Y : C) : (CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).inv.app Y = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app Y))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.shiftFunctor C b).map (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj Y))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.Functor.commShiftIso G b).inv.app (F.obj ((CategoryTheory.shiftFunctor C a).obj Y))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (adj.counit.app ((CategoryTheory.shiftFunctor D b).obj (F.obj ((CategoryTheory.shiftFunctor C a).obj Y))))) ((CategoryTheory.shiftFunctorCompIsoId D b a ⋯).hom.app (F.obj ((CategoryTheory.shiftFunctor C a).obj Y))))))
CategoryTheory.Adjunction.RightAdjointCommShift.iso_hom_app 📋 Mathlib.CategoryTheory.Shift.Adjunction
{C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {A : Type u_3} [AddGroup A] [CategoryTheory.HasShift C A] [CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [F.CommShift A] (X : D) : (CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C b a h).inv.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (adj.unit.app ((CategoryTheory.shiftFunctor C b).obj (G.obj ((CategoryTheory.shiftFunctor D a).obj X))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.Functor.commShiftIso F b).hom.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X))))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.shiftFunctor D b).map (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj X))))) ((CategoryTheory.shiftFunctor C a).map (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app X))))))
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).hom.app (Opposite.unop X)).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X))))
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))) ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).inv.app (Opposite.unop X)).op
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖ} (h : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).hom.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))) h)
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖ} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m hnm).inv.app (Opposite.unop X)).op h)
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X).unop).op
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X).unop).op ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) : (CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X)))) ((CategoryTheory.shiftFunctor Cᵒᵖ m).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X)))
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖ} (h : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X).unop).op h)
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) : (CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ m).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X)))) ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op)
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖ} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X).unop).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op h)
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖ} (h : (CategoryTheory.shiftFunctor Cᵒᵖ m).obj ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).inv.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X)))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ m).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app X)) h))
CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.Opposite.Basic
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖ} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId Cᵒᵖ n m hnm).hom.app X) h = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ m).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op ((CategoryTheory.shiftFunctor C m).obj (Opposite.unop X)))) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app (Opposite.unop X)).op h))

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59