Functor

📁 Source: Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean

Statistics

Metric	Count
Definitions instCatCommSqOppositeTriangleOpMapTriangleFunctorTriangleOpEquivalence, instCatCommSqTriangleOppositeMapTriangleOpInverseTriangleOpEquivalence, mapTriangleOpCompTriangleOpEquivalenceFunctor, mapTriangleOpCompTriangleOpEquivalenceFunctorApp, opMapTriangleCompTriangleOpEquivalenceInverse, commShiftFunctorOpInt	6
Theorems isTriangulated_of_op, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, map_opShiftFunctorEquivalence_counitIso_hom_app_unop, map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, map_opShiftFunctorEquivalence_counitIso_inv_app_unop, map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, map_opShiftFunctorEquivalence_unitIso_hom_app_unop, map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, map_opShiftFunctorEquivalence_unitIso_inv_app_unop, map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, map_shift_unop, map_shift_unop_assoc, op_commShiftIso_hom_app, op_commShiftIso_hom_app_assoc, op_commShiftIso_inv_app, op_commShiftIso_inv_app_assoc, op_isTriangulated_iff, shift_map_op, shift_map_op_assoc, commShift_adjunction_op_int, commShift_natTrans_op_int, functor_isTriangulated_op	27
Total	33

CategoryTheory.Functor

Definitions

Name	Category	Theorems
instCatCommSqOppositeTriangleOpMapTriangleFunctorTriangleOpEquivalence 📖	CompOp	—
instCatCommSqTriangleOppositeMapTriangleOpInverseTriangleOpEquivalence 📖	CompOp	—
mapTriangleOpCompTriangleOpEquivalenceFunctor 📖	CompOp	—
mapTriangleOpCompTriangleOpEquivalenceFunctorApp 📖	CompOp	6 math math: mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂
opMapTriangleCompTriangleOpEquivalenceInverse 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTriangulated_of_op 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated	—	CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt CategoryTheory.Pretriangulated.distinguished_iff_of_iso Opposite.unop_op id_obj comp_obj CategoryTheory.Pretriangulated.mem_distTriang_op_iff op_obj map_distinguished
mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.triangleOpEquivalence Opposite.op mapTriangle op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.Iso.hom mapTriangleOpCompTriangleOpEquivalenceFunctorApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.triangleOpEquivalence Opposite.op mapTriangle op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.Iso.hom mapTriangleOpCompTriangleOpEquivalenceFunctorApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.triangleOpEquivalence Opposite.op mapTriangle op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.Iso.hom mapTriangleOpCompTriangleOpEquivalenceFunctorApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.triangleOpEquivalence Opposite.op CategoryTheory.Iso.inv mapTriangleOpCompTriangleOpEquivalenceFunctorApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.triangleOpEquivalence Opposite.op CategoryTheory.Iso.inv mapTriangleOpCompTriangleOpEquivalenceFunctorApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt obj CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory mapTriangle op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.triangleOpEquivalence Opposite.op CategoryTheory.Iso.inv mapTriangleOpCompTriangleOpEquivalenceFunctorApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
map_opShiftFunctorEquivalence_counitIso_hom_app_unop 📖	mathematical	—	map Opposite.unop obj Opposite CategoryTheory.Category.opposite id comp CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category CategoryTheory.Equivalence.counitIso CategoryTheory.CategoryStruct.comp Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt op Quiver.Hom.op CategoryTheory.Iso.inv CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt	—	CategoryTheory.Category.assoc add_neg_cancel op_commShiftIso_hom_app_assoc map_comp map_shiftFunctorCompIsoId_inv_app_assoc CategoryTheory.op_comp CategoryTheory.op_comp_assoc CategoryTheory.NatTrans.naturality_assoc op_map CategoryTheory.Iso.inv_hom_id_app_assoc Quiver.Hom.unop_op
map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.app comp id CategoryTheory.Iso.hom CategoryTheory.Functor category CategoryTheory.Equivalence.counitIso Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.Iso.inv CommShift.commShiftIso op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_opShiftFunctorEquivalence_counitIso_hom_app_unop
map_opShiftFunctorEquivalence_counitIso_inv_app_unop 📖	mathematical	—	map Opposite.unop obj Opposite CategoryTheory.Category.opposite comp CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor id Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category CategoryTheory.Equivalence.counitIso CategoryTheory.CategoryStruct.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt op Opposite.op CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Quiver.Hom.op CategoryTheory.Iso.hom	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso map_isIso CategoryTheory.isIso_unop CategoryTheory.NatIso.hom_app_isIso map_comp CategoryTheory.unop_comp CategoryTheory.Iso.inv_hom_id_app map_opShiftFunctorEquivalence_counitIso_hom_app_unop map_id CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Category.id_comp
map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.app id comp CategoryTheory.Iso.inv CategoryTheory.Functor category CategoryTheory.Equivalence.counitIso CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt op Opposite.op CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Quiver.Hom.op CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_opShiftFunctorEquivalence_counitIso_inv_app_unop
map_opShiftFunctorEquivalence_unitIso_hom_app_unop 📖	mathematical	—	map Opposite.unop obj Opposite CategoryTheory.Category.opposite comp CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse id Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Opposite.op CommShift.commShiftIso op CategoryTheory.Iso.inv CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt	—	add_neg_cancel map_comp map_shiftFunctorCompIsoId_hom_app commShiftIso_hom_naturality_assoc op_commShiftIso_inv_app CategoryTheory.Category.assoc map_comp_assoc CategoryTheory.unop_comp CategoryTheory.Iso.inv_hom_id_app map_id CategoryTheory.Category.id_comp
map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.app id comp CategoryTheory.Iso.hom CategoryTheory.Functor category CategoryTheory.Equivalence.unitIso CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CommShift.commShiftIso op CategoryTheory.Iso.inv CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Opposite.op	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_opShiftFunctorEquivalence_unitIso_hom_app_unop
map_opShiftFunctorEquivalence_unitIso_inv_app_unop 📖	mathematical	—	map Opposite.unop obj Opposite CategoryTheory.Category.opposite id comp CategoryTheory.Equivalence.functor CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt op CategoryTheory.Iso.hom CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.instIsSplitMonoMap CategoryTheory.IsSplitMono.of_iso CategoryTheory.isIso_unop CategoryTheory.NatIso.hom_app_isIso map_comp CategoryTheory.unop_comp CategoryTheory.Iso.hom_inv_id_app map_opShiftFunctorEquivalence_unitIso_hom_app_unop CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc map_comp_assoc map_id CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.id_comp CategoryTheory.Iso.unop_inv_hom_id_app
map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.Equivalence.inverse CategoryTheory.Pretriangulated.opShiftFunctorEquivalence CategoryTheory.Equivalence.functor map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.app comp id CategoryTheory.Iso.inv CategoryTheory.Functor category CategoryTheory.Equivalence.unitIso Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid op CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Iso.hom CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_opShiftFunctorEquivalence_unitIso_inv_app_unop
map_shift_unop 📖	mathematical	—	map Opposite.unop obj Opposite CategoryTheory.Category.opposite CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp comp op CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Opposite.op Quiver.Hom.op CategoryTheory.Iso.hom	—	shift_map_op CategoryTheory.Category.assoc CategoryTheory.Iso.unop_inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Iso.unop_inv_hom_id_app_assoc
map_shift_unop_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver op CategoryTheory.NatTrans.app comp CategoryTheory.Iso.inv CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Opposite.op Quiver.Hom.op CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_shift_unop
op_commShiftIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt op CategoryTheory.Iso.hom CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op obj Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver map Quiver.Hom.unop CategoryTheory.Pretriangulated.shiftFunctorOpIso CategoryTheory.Iso.inv	—	—
op_commShiftIso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite obj op CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver map Quiver.Hom.unop CategoryTheory.Pretriangulated.shiftFunctorOpIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' op_commShiftIso_hom_app
op_commShiftIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite comp op CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Iso.inv CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct obj Opposite.op Opposite.unop CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver map Quiver.Hom.unop	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Iso.hom_inv_id_app op_commShiftIso_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Category.comp_id map_comp CategoryTheory.Iso.unop_inv_hom_id_app map_id
op_commShiftIso_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt op CategoryTheory.NatTrans.app comp CategoryTheory.Iso.inv CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Opposite.op Opposite.unop CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver map Quiver.Hom.unop	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' op_commShiftIso_inv_app
op_isTriangulated_iff 📖	mathematical	Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated Opposite CategoryTheory.Category.opposite CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt op CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt CategoryTheory.Limits.hasZeroObject_op CategoryTheory.instPreadditiveOpposite CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt CategoryTheory.Pretriangulated.Opposite.instOpposite	—	CategoryTheory.Limits.hasZeroObject_op CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt isTriangulated_of_op CategoryTheory.Pretriangulated.Opposite.functor_isTriangulated_op
shift_map_op 📖	mathematical	—	map Opposite CategoryTheory.Category.opposite CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Opposite.op obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite comp op CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Opposite.unop Quiver.Hom.unop CategoryTheory.Iso.hom	—	CategoryTheory.NatIso.naturality_1
shift_map_op_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt Opposite.op map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver op CategoryTheory.NatTrans.app comp CategoryTheory.Iso.inv CategoryTheory.Functor category CommShift.commShiftIso CategoryTheory.Pretriangulated.Opposite.commShiftFunctorOpInt Opposite.unop Quiver.Hom.unop CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shift_map_op

CategoryTheory.Pretriangulated.Opposite

Definitions

Name	Category	Theorems
commShiftFunctorOpInt 📖	CompOp	26 math math: CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, CategoryTheory.Functor.shift_map_op_assoc, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, CategoryTheory.Functor.map_shift_unop, CategoryTheory.Functor.op_commShiftIso_hom_app_assoc, commShift_natTrans_op_int, CategoryTheory.Functor.op_commShiftIso_inv_app_assoc, CategoryTheory.Functor.op_commShiftIso_inv_app, commShift_adjunction_op_int, functor_isTriangulated_op, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, CategoryTheory.Functor.shift_map_op, CategoryTheory.Functor.map_shift_unop_assoc, CategoryTheory.Functor.op_isTriangulated_iff, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, CategoryTheory.Functor.op_commShiftIso_hom_app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commShift_adjunction_op_int 📖	mathematical	—	CategoryTheory.Adjunction.CommShift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Adjunction.op Int.instAddMonoid instHasShiftOppositeInt commShiftFunctorOpInt	—	CategoryTheory.Adjunction.ext CategoryTheory.NatTrans.ext' CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Adjunction.commShiftPullback CategoryTheory.Adjunction.commShift_op
commShift_natTrans_op_int 📖	mathematical	—	CategoryTheory.NatTrans.CommShift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.NatTrans.op Int.instAddMonoid instHasShiftOppositeInt commShiftFunctorOpInt	—	CategoryTheory.NatTrans.commShiftPullback CategoryTheory.NatTrans.commShift_op
functor_isTriangulated_op 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated Opposite CategoryTheory.Category.opposite instHasShiftOppositeInt CategoryTheory.Functor.op commShiftFunctorOpInt CategoryTheory.Limits.hasZeroObject_op CategoryTheory.instPreadditiveOpposite instAdditiveOppositeShiftFunctorInt instOpposite	—	CategoryTheory.Limits.hasZeroObject_op instAdditiveOppositeShiftFunctorInt CategoryTheory.Pretriangulated.mem_distTriang_op_iff CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Functor.map_distinguished CategoryTheory.Pretriangulated.unop_distinguished

---

← Back to Index