Basic

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

Statistics

Metric	Count
Definitions instHasShiftOppositeInt, opShiftFunctorEquivalence, opShiftFunctorEquivalenceSymmHomEquiv, shiftFunctorOpIso	4
Theorems instAdditiveOppositeShiftFunctorInt, opShiftFunctorEquivalenceSymmHomEquiv_apply, opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, opShiftFunctorEquivalenceSymmHomEquiv_left_inv, opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, opShiftFunctorEquivalence_add_unitIso_hom_app_eq, opShiftFunctorEquivalence_add_unitIso_inv_app_eq, opShiftFunctorEquivalence_counitIso_hom_app, opShiftFunctorEquivalence_counitIso_hom_app_assoc, opShiftFunctorEquivalence_counitIso_hom_app_shift, opShiftFunctorEquivalence_counitIso_hom_naturality, opShiftFunctorEquivalence_counitIso_hom_naturality_assoc, opShiftFunctorEquivalence_counitIso_inv_app, opShiftFunctorEquivalence_counitIso_inv_app_assoc, opShiftFunctorEquivalence_counitIso_inv_app_shift, opShiftFunctorEquivalence_counitIso_inv_naturality, opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, opShiftFunctorEquivalence_functor, opShiftFunctorEquivalence_inverse, opShiftFunctorEquivalence_unitIso_hom_app, opShiftFunctorEquivalence_unitIso_hom_app_assoc, opShiftFunctorEquivalence_unitIso_hom_app_eq, opShiftFunctorEquivalence_unitIso_hom_naturality, opShiftFunctorEquivalence_unitIso_hom_naturality_assoc, opShiftFunctorEquivalence_unitIso_inv_app, opShiftFunctorEquivalence_unitIso_inv_app_assoc, opShiftFunctorEquivalence_unitIso_inv_app_eq, opShiftFunctorEquivalence_unitIso_inv_naturality, opShiftFunctorEquivalence_unitIso_inv_naturality_assoc, opShiftFunctorEquivalence_zero_unitIso_hom_app, opShiftFunctorEquivalence_zero_unitIso_inv_app, shiftFunctorAdd'_op_hom_app, shiftFunctorAdd'_op_inv_app, shiftFunctorCompIsoId_op_hom_app, shiftFunctorCompIsoId_op_hom_app_assoc, shiftFunctorCompIsoId_op_inv_app, shiftFunctorCompIsoId_op_inv_app_assoc, shiftFunctorZero_op_hom_app, shiftFunctorZero_op_inv_app, shiftFunctor_op_map, shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, shift_opShiftFunctorEquivalence_counitIso_inv_app, shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, shift_unop_opShiftFunctorEquivalence_counitIso_hom_app, shift_unop_opShiftFunctorEquivalence_counitIso_inv_app	46
Total	50

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
opShiftFunctorEquivalence 📖	CompOp	54 math math: opShiftFunctorEquivalence_unitIso_inv_app_eq, shift_opShiftFunctorEquivalence_counitIso_inv_app, opShiftFunctorEquivalence_add_unitIso_hom_app_eq, opShiftFunctorEquivalence_inverse, opShiftFunctorEquivalenceSymmHomEquiv_left_inv, TriangleOpEquivalence.functor_map_hom₂, opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, opShiftFunctorEquivalence_counitIso_hom_naturality, opShiftFunctorEquivalence_counitIso_inv_naturality, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop, TriangleOpEquivalence.functor_map_hom₃, TriangleOpEquivalence.unitIso_hom_app, opShiftFunctorEquivalence_counitIso_hom_naturality_assoc, opShiftFunctorEquivalence_counitIso_inv_app_shift, opShiftFunctorEquivalence_unitIso_hom_app, opShiftFunctorEquivalence_zero_unitIso_inv_app, shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, opShiftFunctorEquivalence_counitIso_hom_app, opShiftFunctorEquivalence_zero_unitIso_hom_app, opShiftFunctorEquivalenceSymmHomEquiv_apply, opShiftFunctorEquivalence_unitIso_inv_naturality_assoc, TriangleOpEquivalence.unitIso_inv_app, opShiftFunctorEquivalence_unitIso_hom_naturality_assoc, TriangleOpEquivalence.functor_obj, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, opShiftFunctorEquivalence_unitIso_hom_naturality, opShiftFunctorEquivalence_counitIso_hom_app_assoc, opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, opShiftFunctorEquivalence_add_unitIso_inv_app_eq, TriangleOpEquivalence.inverse_obj, opShiftFunctorEquivalence_unitIso_hom_app_assoc, opShiftFunctorEquivalence_counitIso_inv_app_assoc, shift_unop_opShiftFunctorEquivalence_counitIso_hom_app, CategoryTheory.ShiftedHom.opEquiv_symm_apply, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, TriangleOpEquivalence.functor_map_hom₁, opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, opShiftFunctorEquivalence_functor, TriangleOpEquivalence.inverse_map, opShiftFunctorEquivalence_unitIso_hom_app_eq, shift_unop_opShiftFunctorEquivalence_counitIso_inv_app, shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, opShiftFunctorEquivalence_unitIso_inv_app, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop, shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, opShiftFunctorEquivalence_unitIso_inv_naturality, opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, opShiftFunctorEquivalence_counitIso_hom_app_shift, opShiftFunctorEquivalence_unitIso_inv_app_assoc
opShiftFunctorEquivalenceSymmHomEquiv 📖	CompOp	6 math math: opShiftFunctorEquivalenceSymmHomEquiv_left_inv, opShiftFunctorEquivalenceSymmHomEquiv_apply, opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc
shiftFunctorOpIso 📖	CompOp	39 math math: shiftFunctorCompIsoId_op_hom_app, shift_opShiftFunctorEquivalence_counitIso_inv_app, Opposite.UnopUnopCommShift.iso_inv_app, shiftFunctorZero_op_inv_app, shiftFunctorCompIsoId_op_inv_app, shiftFunctorAdd'_op_hom_app, Opposite.OpOpCommShift.iso_inv_app, commShiftIso_opOp_inv_app, Opposite.UnopUnopCommShift.iso_inv_app_assoc, commShiftIso_opOp_hom_app_assoc, shiftFunctorAdd'_op_inv_app, opShiftFunctorEquivalence_unitIso_hom_app, CategoryTheory.Functor.op_commShiftIso_hom_app_assoc, shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, Opposite.UnopUnopCommShift.iso_hom_app_assoc, opShiftFunctorEquivalence_counitIso_hom_app, Opposite.OpOpCommShift.iso_hom_app_assoc, commShiftIso_unopUnop_inv_app, shiftFunctorZero_op_hom_app, CategoryTheory.Functor.op_commShiftIso_inv_app_assoc, CategoryTheory.Functor.op_commShiftIso_inv_app, Opposite.OpOpCommShift.iso_inv_app_assoc, opShiftFunctorEquivalence_counitIso_hom_app_assoc, opShiftFunctorEquivalence_counitIso_inv_app, shiftFunctor_op_map, commShiftIso_opOp_hom_app, commShiftIso_opOp_inv_app_assoc, commShiftIso_unopUnop_inv_app_assoc, Opposite.UnopUnopCommShift.iso_hom_app, opShiftFunctorEquivalence_unitIso_hom_app_assoc, opShiftFunctorEquivalence_counitIso_inv_app_assoc, shiftFunctorCompIsoId_op_hom_app_assoc, commShiftIso_unopUnop_hom_app, CategoryTheory.Functor.op_commShiftIso_hom_app, Opposite.OpOpCommShift.iso_hom_app, commShiftIso_unopUnop_hom_app_assoc, opShiftFunctorEquivalence_unitIso_inv_app, shiftFunctorCompIsoId_op_inv_app_assoc, opShiftFunctorEquivalence_unitIso_inv_app_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
opShiftFunctorEquivalenceSymmHomEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Opposite Quiver.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt EquivLike.toFunLike Equiv.instEquivLike opShiftFunctorEquivalenceSymmHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map	—	—
opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt DFunLike.coe Equiv Quiver.Hom Quiver.opposite CategoryTheory.CategoryStruct.toQuiver Opposite.op Opposite.unop EquivLike.toFunLike Equiv.instEquivLike opShiftFunctorEquivalenceSymmHomEquiv CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalenceSymmHomEquiv_apply
opShiftFunctorEquivalenceSymmHomEquiv_left_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.shiftFunctor Int.instAddMonoid Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.Functor.map Opposite.instHasShiftOppositeInt DFunLike.coe Equiv Quiver.Hom Quiver.opposite Opposite.op EquivLike.toFunLike Equiv.instEquivLike opShiftFunctorEquivalenceSymmHomEquiv	—	Equiv.left_inv
opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.map Opposite.instHasShiftOppositeInt DFunLike.coe Equiv Quiver.Hom Quiver.opposite Opposite.op EquivLike.toFunLike Equiv.instEquivLike opShiftFunctorEquivalenceSymmHomEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalenceSymmHomEquiv_left_inv
opShiftFunctorEquivalence_add_unitIso_hom_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.shiftFunctorAdd' CategoryTheory.Iso.inv	—	add_neg_cancel shiftFunctorAdd'_op_inv_app shiftFunctor_op_map CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id neg_add_cancel CategoryTheory.shiftFunctorCompIsoId_add'_hom_app
opShiftFunctorEquivalence_add_unitIso_inv_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.hom CategoryTheory.shiftFunctorAdd'	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.Functor.instIsSplitMonoApp CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.inv_hom_id_app opShiftFunctorEquivalence_add_unitIso_hom_app_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id_app
opShiftFunctorEquivalence_counitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Opposite.op Opposite.unop CategoryTheory.Functor.op shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv CategoryTheory.shiftFunctorCompIsoId	—	—
opShiftFunctorEquivalence_counitIso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.op CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.op Opposite.unop Opposite.instHasShiftOppositeInt shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv CategoryTheory.shiftFunctorCompIsoId	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_counitIso_hom_app
opShiftFunctorEquivalence_counitIso_hom_app_shift 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Equivalence.counit_app_functor
opShiftFunctorEquivalence_counitIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Opposite.op Opposite.unop CategoryTheory.Functor.id CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.CategoryStruct.opposite	—	CategoryTheory.NatTrans.naturality
opShiftFunctorEquivalence_counitIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Opposite.op Opposite.unop CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_counitIso_hom_naturality
opShiftFunctorEquivalence_counitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj Opposite.unop CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom CategoryTheory.shiftFunctorCompIsoId CategoryTheory.Functor.op shiftFunctorOpIso	—	—
opShiftFunctorEquivalence_counitIso_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom CategoryTheory.shiftFunctorCompIsoId CategoryTheory.Functor.op Opposite.instHasShiftOppositeInt shiftFunctorOpIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_counitIso_inv_app
opShiftFunctorEquivalence_counitIso_inv_app_shift 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Equivalence.counitInv_app_functor
opShiftFunctorEquivalence_counitIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Opposite.op Opposite.unop CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop	—	CategoryTheory.NatTrans.naturality
opShiftFunctorEquivalence_counitIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.Functor.map CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_counitIso_inv_naturality
opShiftFunctorEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Opposite CategoryTheory.Category.opposite opShiftFunctorEquivalence CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt	—	—
opShiftFunctorEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Opposite CategoryTheory.Category.opposite opShiftFunctorEquivalence CategoryTheory.Functor.op CategoryTheory.shiftFunctor Int.instAddMonoid	—	—
opShiftFunctorEquivalence_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj Opposite.unop CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.shiftFunctorCompIsoId CategoryTheory.Functor.op CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.inv shiftFunctorOpIso	—	—
opShiftFunctorEquivalence_unitIso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.shiftFunctorCompIsoId Opposite.instHasShiftOppositeInt CategoryTheory.Functor.op CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.inv shiftFunctorOpIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_unitIso_hom_app
opShiftFunctorEquivalence_unitIso_hom_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.shiftFunctorAdd' CategoryTheory.Iso.inv	—	opShiftFunctorEquivalence_add_unitIso_hom_app_eq
opShiftFunctorEquivalence_unitIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop	—	CategoryTheory.NatTrans.naturality
opShiftFunctorEquivalence_unitIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt CategoryTheory.Functor.map Quiver.Hom.unop	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_unitIso_hom_naturality
opShiftFunctorEquivalence_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.hom shiftFunctorOpIso CategoryTheory.shiftFunctorCompIsoId	—	—
opShiftFunctorEquivalence_unitIso_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso Opposite.op CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Opposite.instHasShiftOppositeInt CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.hom shiftFunctorOpIso CategoryTheory.shiftFunctorCompIsoId	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_unitIso_inv_app
opShiftFunctorEquivalence_unitIso_inv_app_eq 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.hom CategoryTheory.shiftFunctorAdd'	—	opShiftFunctorEquivalence_add_unitIso_inv_app_eq
opShiftFunctorEquivalence_unitIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt CategoryTheory.Functor.id Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso	—	CategoryTheory.NatTrans.naturality
opShiftFunctorEquivalence_unitIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opShiftFunctorEquivalence_unitIso_inv_naturality
opShiftFunctorEquivalence_zero_unitIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj Opposite.unop CategoryTheory.shiftFunctor Int.instAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Opposite.instHasShiftOppositeInt Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.shiftFunctorZero CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.inv	—	zero_add shiftFunctorZero_op_inv_app CategoryTheory.unop_comp Quiver.Hom.unop_op CategoryTheory.Functor.map_comp add_zero CategoryTheory.shiftFunctorCompIsoId_zero_zero_hom_app CategoryTheory.Category.assoc
opShiftFunctorEquivalence_zero_unitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite.instHasShiftOppositeInt AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.Iso.hom CategoryTheory.shiftFunctorZero	—	zero_add shiftFunctorZero_op_hom_app CategoryTheory.unop_comp Quiver.Hom.unop_op CategoryTheory.Functor.map_comp add_zero CategoryTheory.shiftFunctorCompIsoId_zero_zero_inv_app CategoryTheory.Category.assoc
shiftFunctorAdd'_op_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorAdd' CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.op shiftFunctorOpIso Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv CategoryTheory.Functor.map	—	CategoryTheory.pullbackShiftFunctorAdd'_hom_app CategoryTheory.oppositeShiftFunctorAdd'_hom_app
shiftFunctorAdd'_op_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorAdd' CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.op CategoryTheory.Functor.map CategoryTheory.Iso.hom shiftFunctorOpIso Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Iso.hom_inv_id_app shiftFunctorAdd'_op_hom_app CategoryTheory.Category.assoc CategoryTheory.Functor.map_comp_assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id_app_assoc CategoryTheory.op_comp_assoc CategoryTheory.op_id
shiftFunctorCompIsoId_op_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorCompIsoId CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.op Opposite.op Opposite.unop CategoryTheory.Functor.map shiftFunctorOpIso CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv	—	add_zero zero_add shiftFunctorAdd'_op_inv_app CategoryTheory.NatTrans.naturality_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc
shiftFunctorCompIsoId_op_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorCompIsoId CategoryTheory.Functor.op CategoryTheory.Functor.map shiftFunctorOpIso Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorCompIsoId_op_hom_app
shiftFunctorCompIsoId_op_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorCompIsoId CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom CategoryTheory.Functor.op shiftFunctorOpIso CategoryTheory.Functor.map	—	add_zero zero_add shiftFunctorZero_op_inv_app shiftFunctorAdd'_op_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app_assoc
shiftFunctorCompIsoId_op_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorCompIsoId Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom CategoryTheory.Functor.op shiftFunctorOpIso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftFunctorCompIsoId_op_inv_app
shiftFunctorZero_op_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorZero CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.op Opposite.op Opposite.unop shiftFunctorOpIso zero_add Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.inv	—	—
shiftFunctorZero_op_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorZero CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom CategoryTheory.Functor.op shiftFunctorOpIso zero_add	—	zero_add CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.hom_app_isIso CategoryTheory.Iso.hom_inv_id_app shiftFunctorZero_op_hom_app CategoryTheory.Category.assoc CategoryTheory.op_comp_assoc CategoryTheory.op_id CategoryTheory.Category.id_comp
shiftFunctor_op_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.op CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctorOpIso Opposite.op Opposite.unop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop CategoryTheory.Iso.inv	—	CategoryTheory.NatIso.naturality_2
shift_opShiftFunctorEquivalenceSymmHomEquiv_unop 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom Quiver.opposite Opposite.op EquivLike.toFunLike Equiv.instEquivLike opShiftFunctorEquivalenceSymmHomEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.comp CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso	—	opShiftFunctorEquivalenceSymmHomEquiv_left_inv CategoryTheory.Iso.unop_hom_inv_id_app_assoc
shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop Opposite CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt CategoryTheory.Functor.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver DFunLike.coe Equiv Quiver.Hom Quiver.opposite Opposite.op EquivLike.toFunLike Equiv.instEquivLike opShiftFunctorEquivalenceSymmHomEquiv CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shift_opShiftFunctorEquivalenceSymmHomEquiv_unop
shift_opShiftFunctorEquivalence_counitIso_inv_app 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Functor.obj CategoryTheory.Functor.id Opposite.op CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct AddCommMonoid.toAddMonoid Int.instAddCommMonoid Opposite.unop CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop CategoryTheory.Iso.hom shiftFunctorOpIso CategoryTheory.shiftFunctorComm	—	shiftFunctor_op_map CategoryTheory.Functor.map_comp CategoryTheory.shift_shiftFunctorCompIsoId_hom_app CategoryTheory.Category.assoc CategoryTheory.shiftFunctorComm_inv_app_of_add_eq_zero shiftFunctorCompIsoId_op_hom_app CategoryTheory.Iso.inv_hom_id_app_assoc shiftFunctorCompIsoId_op_inv_app CategoryTheory.Iso.unop_hom_inv_id_app_assoc CategoryTheory.NatIso.naturality_1
shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt Opposite.op CategoryTheory.Equivalence.functor opShiftFunctorEquivalence CategoryTheory.Equivalence.inverse CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso Opposite.unop CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop CategoryTheory.Iso.hom shiftFunctorOpIso AddCommMonoid.toAddMonoid Int.instAddCommMonoid CategoryTheory.shiftFunctorComm	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shift_opShiftFunctorEquivalence_counitIso_inv_app
shift_unop_opShiftFunctorEquivalence_counitIso_hom_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso Opposite.op CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Equivalence.unitInv_app_inverse
shift_unop_opShiftFunctorEquivalence_counitIso_inv_app 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Equivalence.inverse opShiftFunctorEquivalence CategoryTheory.Equivalence.functor CategoryTheory.Functor.id Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Equivalence.counitIso Opposite.op CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso	—	CategoryTheory.Equivalence.unit_app_inverse

CategoryTheory.Pretriangulated.Opposite

Definitions

Name	Category	Theorems
instHasShiftOppositeInt 📖	CompOp	139 math math: CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_eq, CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq, mem_distinguishedTriangles_iff, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁, UnopUnopCommShift.iso_inv_app, CategoryTheory.Pretriangulated.shiftFunctorZero_op_inv_app, mem_distinguishedTriangles_iff', CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOpEquivalence, CategoryTheory.ShiftedHom.opEquiv_symm_add, CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv, CategoryTheory.Pretriangulated.triangleOpEquivalence_unitIso, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app, OpOpCommShift.iso_inv_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂, CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₃, contractibleTriangleIso_hom_hom₂, UnopUnopCommShift.iso_inv_app_assoc, CategoryTheory.Functor.shift_map_op_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality, CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality, CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app, CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOp, contractibleTriangleIso_hom_hom₁, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₁, CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₃, contractibleTriangleIso_inv_hom₃, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₁, contractibleTriangleIso_hom_hom₃, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app, CategoryTheory.Functor.map_shift_unop, CategoryTheory.Functor.op_commShiftIso_hom_app_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app_assoc, UnopUnopCommShift.iso_hom_app_assoc, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app, contractibleTriangleIso_inv_hom₁, OpOpCommShift.iso_hom_app_assoc, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app, contractible_distinguished, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app, CategoryTheory.Pretriangulated.op_distinguished, commShift_natTrans_op_int, CategoryTheory.Pretriangulated.mem_distTriang_op_iff, CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply, CategoryTheory.Functor.op_commShiftIso_inv_app_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₂, CategoryTheory.Pretriangulated.triangleOpEquivalence_counitIso, CategoryTheory.Pretriangulated.triangleOpEquivalence_functor, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc, CategoryTheory.Pretriangulated.mem_distTriang_op_iff', CategoryTheory.Functor.op_commShiftIso_inv_app, CategoryTheory.ShiftedHom.opEquiv'_symm_apply, CategoryTheory.Pretriangulated.instCommShiftOppositeOpOpEquivalenceInt, commShift_adjunction_op_int, CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc, functor_isTriangulated_op, OpOpCommShift.iso_inv_app_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₃, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₂, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_assoc, CategoryTheory.ShiftedHom.opEquiv_symm_apply_comp, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app, CategoryTheory.ShiftedHom.opEquiv'_symm_add, CategoryTheory.ShiftedHom.opEquiv'_zero_add_symm, CategoryTheory.ShiftedHom.opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift, distinguished_cocone_triangle, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop_assoc, CategoryTheory.Functor.shift_map_op, CategoryTheory.Pretriangulated.shiftFunctor_op_map, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj, CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₂, CategoryTheory.ShiftedHom.opEquiv'_symm_comp, CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app_assoc, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app_assoc, CategoryTheory.Functor.map_shift_unop_assoc, UnopUnopCommShift.iso_hom_app, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_assoc, CategoryTheory.Functor.op_isTriangulated_iff, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_assoc, contractibleTriangleIso_inv_hom₂, CategoryTheory.ShiftedHom.opEquiv_symm_apply, CategoryTheory.ShiftedHom.opEquiv'_apply, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop, instAdditiveOppositeShiftFunctorInt, CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_hom_app_assoc, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc, CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app, CategoryTheory.Functor.op_commShiftIso_hom_app, OpOpCommShift.iso_hom_app, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₃, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app_assoc, instIsTriangulatedOpposite, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc, CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_functor, rotate_distinguished_triangle, CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map, CategoryTheory.Functor.map_distinguished_op_exact, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_eq, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app, CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop, CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_hom_app_unop, CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₁, CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂, CategoryTheory.Pretriangulated.triangleOpEquivalence_inverse, CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalenceSymmHomEquiv_unop_assoc, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality, CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply_assoc, CategoryTheory.Pretriangulated.shiftFunctorCompIsoId_op_inv_app_assoc, CategoryTheory.ShiftedHom.opEquiv'_add_symm, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_assoc, CategoryTheory.ShiftedHom.opEquiv_symm_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveOppositeShiftFunctorInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	Opposite CategoryTheory.Category.opposite CategoryTheory.instPreadditiveOpposite instHasShiftOppositeInt	—	CategoryTheory.instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom CategoryTheory.instAdditiveOppositeShiftShiftFunctor

---

← Back to Index