Documentation Verification Report

ShiftedHomOpposite

📁 Source: Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean

Statistics

Metric	Count
Definitions `opEquiv`, `opEquiv'`	2
Theorems `opEquiv'_add_symm`, `opEquiv'_apply`, `opEquiv'_symm_add`, `opEquiv'_symm_apply`, `opEquiv'_symm_comp`, `opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift`, `opEquiv'_zero_add_symm`, `opEquiv_symm_add`, `opEquiv_symm_apply`, `opEquiv_symm_apply_comp`, `opEquiv_symm_comp`	11
Total	13

CategoryTheory.ShiftedHom

Definitions

Name	Category	Theorems
`opEquiv` 📖	CompOp	7 math math: `opEquiv_symm_add`, `opEquiv'_symm_apply`, `opEquiv_symm_apply_comp`, `opEquiv_symm_apply`, `opEquiv'_apply`, `CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply`, `opEquiv_symm_comp`
`opEquiv'` 📖	CompOp	7 math math: `opEquiv'_symm_apply`, `opEquiv'_symm_add`, `opEquiv'_zero_add_symm`, `opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift`, `opEquiv'_symm_comp`, `opEquiv'_apply`, `opEquiv'_add_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`opEquiv'_add_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Opposite` `Quiver.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `CategoryTheory.ShiftedHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv'` `Quiver.Hom.op` `CategoryTheory.Discrete.as` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.addMonoidalFunctor` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Int.instAddGroup` `AddMonoidHom.mk'` `AddMonoid.toAddZeroClass` `Opposite.unop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.opposite` `CategoryTheory.NatTrans.app` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorAdd`	—	`add_comm` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.shiftFunctorAdd'_assoc_inv_app`
`opEquiv'_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.ShiftedHom` `Int.instAddMonoid` `Quiver.Hom` `Opposite` `Quiver.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `EquivLike.toFunLike` `Equiv.instEquivLike` `opEquiv'` `opEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorAdd'`	—	—
`opEquiv'_symm_add` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`DFunLike.coe` `Equiv` `Quiver.Hom` `Opposite` `Quiver.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.Functor.obj` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `CategoryTheory.ShiftedHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv'` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.instPreadditiveOpposite`	—	`opEquiv_symm_add` `CategoryTheory.Preadditive.add_comp`
`opEquiv'_symm_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` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `CategoryTheory.ShiftedHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv'` `CategoryTheory.CategoryStruct.comp` `opEquiv` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorAdd'`	—	—
`opEquiv'_symm_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Opposite` `Quiver.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `CategoryTheory.ShiftedHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.opposite` `CategoryTheory.Functor.map` `Quiver.Hom.op`	—	`CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality`
`opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Opposite` `Quiver.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `CategoryTheory.ShiftedHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.opposite` `Quiver.Hom.op` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence` `CategoryTheory.Equivalence.functor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `CategoryTheory.Functor.map` `comp`	—	`opEquiv'_symm_apply` `opEquiv_symm_apply` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality` `CategoryTheory.Equivalence.inverse_counitInv_comp_assoc`
`opEquiv'_zero_add_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `Opposite` `Quiver.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.op` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `CategoryTheory.ShiftedHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv'` `zero_add` `AddMonoid.toAddZeroClass` `CategoryTheory.CategoryStruct.comp` `Opposite.unop` `CategoryTheory.Functor.id` `AddZero.toZero` `AddZeroClass.toAddZero` `Quiver.Hom.unop` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorZero`	—	`zero_add` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app` `CategoryTheory.Category.assoc` `CategoryTheory.shiftFunctorAdd'_add_zero` `CategoryTheory.Category.comp_id` `CategoryTheory.NatTrans.naturality` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`opEquiv_symm_add` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`DFunLike.coe` `Equiv` `CategoryTheory.ShiftedHom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.instPreadditiveOpposite` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Preadditive.comp_add` `CategoryTheory.Functor.map_add`
`opEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.ShiftedHom` `Opposite` `CategoryTheory.Category.opposite` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.functor` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence` `CategoryTheory.Equivalence.inverse` `CategoryTheory.shiftFunctor` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `CategoryTheory.Functor.map`	—	—
`opEquiv_symm_apply_comp` 📖	mathematical	—	`comp` `Int.instAddMonoid` `DFunLike.coe` `Equiv` `CategoryTheory.ShiftedHom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorAdd'`	—	`opEquiv_symm_apply` `comp.eq_1` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp`
`opEquiv_symm_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.ShiftedHom` `Opposite` `CategoryTheory.Category.opposite` `Int.instAddMonoid` `CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt` `Opposite.op` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `opEquiv` `comp`	—	`opEquiv_symm_apply` `CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq` `comp.eq_1` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.unop_comp_assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.naturality_assoc` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Functor.map_comp_assoc`

---

← Back to Index