OpOp

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

Statistics

Metric	Count
Definitions iso, iso, instCommShiftOppositeOpOpInt, instCommShiftOppositeUnopUnopInt, instCommShiftOppositeFunctorOpOpEquivalenceInt, instCommShiftOppositeInverseOpOpEquivalenceInt	6
Theorems iso_hom_app, iso_hom_app_assoc, iso_inv_app, iso_inv_app_assoc, iso_hom_app, iso_hom_app_assoc, iso_inv_app, iso_inv_app_assoc, commShiftIso_opOp_hom_app, commShiftIso_opOp_hom_app_assoc, commShiftIso_opOp_inv_app, commShiftIso_opOp_inv_app_assoc, commShiftIso_unopUnop_hom_app, commShiftIso_unopUnop_hom_app_assoc, commShiftIso_unopUnop_inv_app, commShiftIso_unopUnop_inv_app_assoc, instCommShiftOppositeOpOpEquivalenceInt, instIsTriangulatedOppositeOpOp, instIsTriangulatedOppositeOpOpEquivalence, instIsTriangulatedOppositeUnopUnop	20
Total	26

CategoryTheory.Pretriangulated

Definitions

Name	Category	Theorems
instCommShiftOppositeFunctorOpOpEquivalenceInt 📖	CompOp	2 math math: instIsTriangulatedOppositeOpOpEquivalence, instCommShiftOppositeOpOpEquivalenceInt
instCommShiftOppositeInverseOpOpEquivalenceInt 📖	CompOp	2 math math: instIsTriangulatedOppositeOpOpEquivalence, instCommShiftOppositeOpOpEquivalenceInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commShiftIso_opOp_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.opOp Opposite.instHasShiftOppositeInt CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeOpOpInt CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver shiftFunctorOpIso CategoryTheory.Iso.inv	—	Opposite.OpOpCommShift.iso_hom_app
commShiftIso_opOp_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.opOp CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeOpOpInt Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.op shiftFunctorOpIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commShiftIso_opOp_hom_app
commShiftIso_opOp_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.opOp CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeOpOpInt CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite.op CategoryTheory.Functor.op CategoryTheory.Iso.hom shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	Opposite.OpOpCommShift.iso_inv_app
commShiftIso_opOp_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.opOp CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeOpOpInt CategoryTheory.Functor.op Opposite.op CategoryTheory.Iso.hom shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commShiftIso_opOp_inv_app
commShiftIso_unopUnop_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.unopUnop CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeUnopUnopInt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver shiftFunctorOpIso CategoryTheory.Iso.inv	—	Opposite.UnopUnopCommShift.iso_hom_app
commShiftIso_unopUnop_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.unopUnop CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeUnopUnopInt Opposite.unop CategoryTheory.Functor.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver shiftFunctorOpIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commShiftIso_unopUnop_hom_app
commShiftIso_unopUnop_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.unopUnop CategoryTheory.shiftFunctor Int.instAddMonoid Opposite.instHasShiftOppositeInt CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeUnopUnopInt CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom shiftFunctorOpIso	—	Opposite.UnopUnopCommShift.iso_inv_app
commShiftIso_unopUnop_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite CategoryTheory.Category.opposite CategoryTheory.unopUnop Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso Opposite.instCommShiftOppositeUnopUnopInt Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.op CategoryTheory.Iso.hom shiftFunctorOpIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commShiftIso_unopUnop_inv_app
instCommShiftOppositeOpOpEquivalenceInt 📖	mathematical	—	CategoryTheory.Equivalence.CommShift Opposite CategoryTheory.Category.opposite CategoryTheory.opOpEquivalence Int.instAddMonoid Opposite.instHasShiftOppositeInt instCommShiftOppositeFunctorOpOpEquivalenceInt instCommShiftOppositeInverseOpOpEquivalenceInt	—	CategoryTheory.Equivalence.CommShift.mk'' CategoryTheory.NatTrans.ext' CategoryTheory.Functor.whiskerRight_id' CategoryTheory.Category.comp_id CategoryTheory.Functor.commShiftIso_comp_hom_app commShiftIso_opOp_hom_app commShiftIso_unopUnop_hom_app CategoryTheory.Category.assoc CategoryTheory.Iso.unop_hom_inv_id_app CategoryTheory.Category.id_comp CategoryTheory.Functor.commShiftIso_id_hom_app
instIsTriangulatedOppositeOpOp 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated Opposite CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt CategoryTheory.opOp Opposite.instCommShiftOppositeOpOpInt CategoryTheory.Limits.hasZeroObject_op CategoryTheory.instPreadditiveOpposite Opposite.instAdditiveOppositeShiftFunctorInt Opposite.instOpposite	—	CategoryTheory.Limits.hasZeroObject_op Opposite.instAdditiveOppositeShiftFunctorInt isomorphic_distinguished op_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp neg_add_cancel CategoryTheory.NatTrans.naturality add_neg_cancel shiftFunctor_op_map CategoryTheory.Category.assoc commShiftIso_opOp_hom_app CategoryTheory.Iso.unop_hom_inv_id_app_assoc CategoryTheory.Iso.inv_hom_id_app_assoc opShiftFunctorEquivalence_counitIso_inv_app shiftFunctorCompIsoId_op_hom_app CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp CategoryTheory.shift_shiftFunctorCompIsoId_hom_app Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Iso.inv_hom_id_app
instIsTriangulatedOppositeOpOpEquivalence 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Equivalence.IsTriangulated Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroObject_op CategoryTheory.instPreadditiveOpposite Opposite.instHasShiftOppositeInt Opposite.instAdditiveOppositeShiftFunctorInt Opposite.instOpposite CategoryTheory.opOpEquivalence instCommShiftOppositeFunctorOpOpEquivalenceInt instCommShiftOppositeInverseOpOpEquivalenceInt	—	CategoryTheory.Equivalence.IsTriangulated.mk'' CategoryTheory.Limits.hasZeroObject_op Opposite.instAdditiveOppositeShiftFunctorInt instCommShiftOppositeOpOpEquivalenceInt instIsTriangulatedOppositeOpOp
instIsTriangulatedOppositeUnopUnop 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated Opposite CategoryTheory.Category.opposite Opposite.instHasShiftOppositeInt CategoryTheory.unopUnop Opposite.instCommShiftOppositeUnopUnopInt CategoryTheory.Limits.hasZeroObject_op CategoryTheory.instPreadditiveOpposite Opposite.instAdditiveOppositeShiftFunctorInt Opposite.instOpposite	—	CategoryTheory.Limits.hasZeroObject_op Opposite.instAdditiveOppositeShiftFunctorInt CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctor instIsTriangulatedOppositeOpOpEquivalence

CategoryTheory.Pretriangulated.Opposite

Definitions

Name	Category	Theorems
instCommShiftOppositeOpOpInt 📖	CompOp	5 math math: CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app, CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app_assoc, CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOp, CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app, CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app_assoc
instCommShiftOppositeUnopUnopInt 📖	CompOp	5 math math: CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app_assoc, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app, CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app_assoc, CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop

CategoryTheory.Pretriangulated.Opposite.OpOpCommShift

Definitions

Name	Category	Theorems
iso 📖	CompOp	4 math math: iso_inv_app, iso_hom_app_assoc, iso_inv_app_assoc, iso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.opOp CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.Functor.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Pretriangulated.shiftFunctorOpIso CategoryTheory.Iso.inv	—	—
iso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.opOp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso Opposite.op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.op CategoryTheory.Pretriangulated.shiftFunctorOpIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_hom_app
iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.opOp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso CategoryTheory.CategoryStruct.comp CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite.op CategoryTheory.Functor.op CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	—
iso_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.opOp CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso CategoryTheory.Functor.op Opposite.op CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.shiftFunctorOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_inv_app

CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift

Definitions

Name	Category	Theorems
iso 📖	CompOp	4 math math: iso_inv_app, iso_inv_app_assoc, iso_hom_app_assoc, iso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.unopUnop CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Pretriangulated.shiftFunctorOpIso CategoryTheory.Iso.inv	—	—
iso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.unopUnop CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category iso Opposite.unop CategoryTheory.Functor.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Pretriangulated.shiftFunctorOpIso CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_hom_app
iso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.unopUnop CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Functor.op Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.shiftFunctorOpIso	—	—
iso_inv_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid Opposite CategoryTheory.Category.opposite CategoryTheory.unopUnop CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category iso Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.op CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.shiftFunctorOpIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_inv_app

---

← Back to Index