TriangleShift

📁 Source: Mathlib/CategoryTheory/Triangulated/TriangleShift.lean

Statistics

Metric	Count
Definitions instHasShiftInt, shiftFunctor, shiftFunctorAdd', shiftFunctorZero, invRotateInvRotateInvRotateIso, invRotateIsoRotateRotateShiftFunctorNegOne, rotateRotateRotateIso	7
Theorems shiftFunctorAdd'_eq, shiftFunctorAdd'_hom_app_hom₁, shiftFunctorAdd'_hom_app_hom₂, shiftFunctorAdd'_hom_app_hom₃, shiftFunctorAdd'_inv_app_hom₁, shiftFunctorAdd'_inv_app_hom₂, shiftFunctorAdd'_inv_app_hom₃, shiftFunctorAdd_eq, shiftFunctorZero_eq, shiftFunctorZero_hom_app_hom₁, shiftFunctorZero_hom_app_hom₂, shiftFunctorZero_hom_app_hom₃, shiftFunctorZero_inv_app_hom₁, shiftFunctorZero_inv_app_hom₂, shiftFunctorZero_inv_app_hom₃, shiftFunctor_eq, shiftFunctor_map_hom₁, shiftFunctor_map_hom₂, shiftFunctor_map_hom₃, shiftFunctor_obj	20
Total	27

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
invRotateInvRotateInvRotateIso 📖	CompOp	—
invRotateIsoRotateRotateShiftFunctorNegOne 📖	CompOp	—
rotateRotateRotateIso 📖	CompOp	—

CategoryTheory.Pretriangulated.Triangle

Definitions

Name	Category	Theorems
instHasShiftInt 📖	CompOp	6 math math: shift_distinguished, shiftFunctorAdd_eq, shiftFunctorZero_eq, shift_distinguished_iff, shiftFunctor_eq, shiftFunctorAdd'_eq
shiftFunctor 📖	CompOp	24 math math: shiftFunctorZero_inv_app_hom₁, shiftFunctor_map_hom₁, shiftFunctor_obj, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₁, shiftFunctorZero_inv_app_hom₃, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₃, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₃, shiftFunctorAdd'_inv_app_hom₂, shiftFunctorZero_hom_app_hom₃, shiftFunctorZero_hom_app_hom₁, shiftFunctorAdd'_inv_app_hom₁, shiftFunctorAdd'_hom_app_hom₃, shiftFunctor_eq, CategoryTheory.Functor.mapTriangleCommShiftIso_inv_app_hom₂, shiftFunctor_map_hom₃, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₁, shiftFunctorAdd'_hom_app_hom₁, shiftFunctorAdd'_inv_app_hom₃, shiftFunctor_map_hom₂, CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂, shiftFunctorZero_inv_app_hom₂, shiftFunctorAdd'_hom_app_hom₂, shiftFunctorZero_hom_app_hom₂, HomotopyCategory.Pretriangulated.shift_distinguished_triangle
shiftFunctorAdd' 📖	CompOp	8 math math: shiftFunctorAdd_eq, shiftFunctorAdd'_inv_app_hom₂, shiftFunctorAdd'_inv_app_hom₁, shiftFunctorAdd'_hom_app_hom₃, shiftFunctorAdd'_eq, shiftFunctorAdd'_hom_app_hom₁, shiftFunctorAdd'_inv_app_hom₃, shiftFunctorAdd'_hom_app_hom₂
shiftFunctorZero 📖	CompOp	7 math math: shiftFunctorZero_inv_app_hom₁, shiftFunctorZero_eq, shiftFunctorZero_inv_app_hom₃, shiftFunctorZero_hom_app_hom₃, shiftFunctorZero_hom_app_hom₁, shiftFunctorZero_inv_app_hom₂, shiftFunctorZero_hom_app_hom₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shiftFunctorAdd'_eq 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.shiftFunctorAdd' CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory instHasShiftInt shiftFunctorAdd'	—	CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd shiftFunctorAdd_eq
shiftFunctorAdd'_hom_app_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd' CategoryTheory.shiftFunctorAdd' obj₁	—	—
shiftFunctorAdd'_hom_app_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd' CategoryTheory.shiftFunctorAdd' obj₂	—	—
shiftFunctorAdd'_hom_app_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd' CategoryTheory.shiftFunctorAdd' obj₃	—	—
shiftFunctorAdd'_inv_app_hom₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.comp shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd' CategoryTheory.shiftFunctorAdd' obj₁	—	—
shiftFunctorAdd'_inv_app_hom₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.comp shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd' CategoryTheory.shiftFunctorAdd' obj₂	—	—
shiftFunctorAdd'_inv_app_hom₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.comp shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorAdd' CategoryTheory.shiftFunctorAdd' obj₃	—	—
shiftFunctorAdd_eq 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.shiftFunctorAdd CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory instHasShiftInt shiftFunctorAdd'	—	CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq
shiftFunctorZero_eq 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.shiftFunctorZero CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory instHasShiftInt shiftFunctorZero	—	CategoryTheory.ShiftMkCore.shiftFunctorZero_eq
shiftFunctorZero_hom_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorZero CategoryTheory.shiftFunctor Int.instAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj₁	—	—
shiftFunctorZero_hom_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorZero CategoryTheory.shiftFunctor Int.instAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj₂	—	—
shiftFunctorZero_hom_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorZero CategoryTheory.shiftFunctor Int.instAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj₃	—	—
shiftFunctorZero_inv_app_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.id shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorZero CategoryTheory.shiftFunctor Int.instAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj₁	—	—
shiftFunctorZero_inv_app_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.id shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorZero CategoryTheory.shiftFunctor Int.instAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj₂	—	—
shiftFunctorZero_inv_app_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.id shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorZero CategoryTheory.shiftFunctor Int.instAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.shiftFunctorZero obj₃	—	—
shiftFunctor_eq 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory instHasShiftInt shiftFunctor	—	—
shiftFunctor_map_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid obj₁ obj₂ obj₃ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow CategoryTheory.Functor.map mor₁ mor₂ CategoryTheory.Functor.comp AddCommMonoid.toAddMonoid Int.instAddCommMonoid CategoryTheory.CategoryStruct.comp mor₃ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorComm CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor	—	—
shiftFunctor_map_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid obj₁ obj₂ obj₃ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow CategoryTheory.Functor.map mor₁ mor₂ CategoryTheory.Functor.comp AddCommMonoid.toAddMonoid Int.instAddCommMonoid CategoryTheory.CategoryStruct.comp mor₃ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorComm CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor	—	—
shiftFunctor_map_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid obj₁ obj₂ obj₃ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow CategoryTheory.Functor.map mor₁ mor₂ CategoryTheory.Functor.comp AddCommMonoid.toAddMonoid Int.instAddCommMonoid CategoryTheory.CategoryStruct.comp mor₃ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorComm CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor	—	—
shiftFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory shiftFunctor CategoryTheory.shiftFunctor Int.instAddMonoid obj₁ obj₂ obj₃ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow CategoryTheory.Functor.map mor₁ mor₂ CategoryTheory.Functor.comp AddCommMonoid.toAddMonoid Int.instAddCommMonoid CategoryTheory.CategoryStruct.comp mor₃ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorComm	—	—

---

← Back to Index