Documentation Verification Report

Opposite

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

Statistics

Metric	Count
Definitions `commShiftOp`, `commShiftUnop`, `mkShiftCoreOp`, `natIsoComp`, `natIsoId`, `OppositeShift`, `adjunction`, `functor`, `natTrans`, `instCategoryOppositeShift`, `instHasShiftOppositeShift`, `instPreadditiveOppositeShift`	12
Theorems `commShift_op`, `commShiftOp_iso_eq`, `commShiftUnop_commShiftIso`, `commShift_op`, `instCommShiftOppositeShiftHomFunctorNatIsoComp`, `instCommShiftOppositeShiftHomFunctorNatIsoId`, `adjunction_counit`, `adjunction_unit`, `instAdditiveOppositeShiftShiftFunctor`, `instHasZeroObjectOppositeShift`, `oppositeShiftFunctorAdd'_hom_app`, `oppositeShiftFunctorAdd'_inv_app`, `oppositeShiftFunctorAdd_hom_app`, `oppositeShiftFunctorAdd_inv_app`, `oppositeShiftFunctorZero_hom_app`, `oppositeShiftFunctorZero_inv_app`	16
Total	28

CategoryTheory

Definitions

Name	Category	Theorems
`OppositeShift` 📖	CompOp	16 math math: `instHasZeroObjectOppositeShift`, `Functor.commShiftOp_iso_eq`, `OppositeShift.adjunction_unit`, `oppositeShiftFunctorAdd_inv_app`, `NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId`, `NatTrans.commShift_op`, `Adjunction.commShift_op`, `oppositeShiftFunctorZero_inv_app`, `oppositeShiftFunctorZero_hom_app`, `oppositeShiftFunctorAdd'_hom_app`, `OppositeShift.adjunction_counit`, `NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp`, `oppositeShiftFunctorAdd_hom_app`, `Functor.commShiftUnop_commShiftIso`, `oppositeShiftFunctorAdd'_inv_app`, `instAdditiveOppositeShiftShiftFunctor`
`instCategoryOppositeShift` 📖	CompOp	16 math math: `instHasZeroObjectOppositeShift`, `Functor.commShiftOp_iso_eq`, `OppositeShift.adjunction_unit`, `oppositeShiftFunctorAdd_inv_app`, `NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId`, `NatTrans.commShift_op`, `Adjunction.commShift_op`, `oppositeShiftFunctorZero_inv_app`, `oppositeShiftFunctorZero_hom_app`, `oppositeShiftFunctorAdd'_hom_app`, `OppositeShift.adjunction_counit`, `NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp`, `oppositeShiftFunctorAdd_hom_app`, `Functor.commShiftUnop_commShiftIso`, `oppositeShiftFunctorAdd'_inv_app`, `instAdditiveOppositeShiftShiftFunctor`
`instHasShiftOppositeShift` 📖	CompOp	13 math math: `Functor.commShiftOp_iso_eq`, `oppositeShiftFunctorAdd_inv_app`, `NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId`, `NatTrans.commShift_op`, `Adjunction.commShift_op`, `oppositeShiftFunctorZero_inv_app`, `oppositeShiftFunctorZero_hom_app`, `oppositeShiftFunctorAdd'_hom_app`, `NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp`, `oppositeShiftFunctorAdd_hom_app`, `Functor.commShiftUnop_commShiftIso`, `oppositeShiftFunctorAdd'_inv_app`, `instAdditiveOppositeShiftShiftFunctor`
`instPreadditiveOppositeShift` 📖	CompOp	1 math math: `instAdditiveOppositeShiftShiftFunctor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAdditiveOppositeShiftShiftFunctor` 📖	mathematical	—	`Functor.Additive` `OppositeShift` `instCategoryOppositeShift` `instPreadditiveOppositeShift` `shiftFunctor` `instHasShiftOppositeShift`	—	`Functor.op_additive`
`instHasZeroObjectOppositeShift` 📖	mathematical	—	`Limits.HasZeroObject` `OppositeShift` `instCategoryOppositeShift`	—	`Limits.hasZeroObject_op`
`oppositeShiftFunctorAdd'_hom_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`NatTrans.app` `OppositeShift` `instCategoryOppositeShift` `shiftFunctor` `instHasShiftOppositeShift` `Functor.comp` `Iso.hom` `Functor` `Functor.category` `shiftFunctorAdd'` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.obj` `Opposite.unop` `Iso.inv`	—	`shiftFunctorAdd'_eq_shiftFunctorAdd` `oppositeShiftFunctorAdd_hom_app`
`oppositeShiftFunctorAdd'_inv_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`NatTrans.app` `OppositeShift` `instCategoryOppositeShift` `Functor.comp` `shiftFunctor` `instHasShiftOppositeShift` `Iso.inv` `Functor` `Functor.category` `shiftFunctorAdd'` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.obj` `Opposite.unop` `Iso.hom`	—	`shiftFunctorAdd'_eq_shiftFunctorAdd`
`oppositeShiftFunctorAdd_hom_app` 📖	mathematical	—	`NatTrans.app` `OppositeShift` `instCategoryOppositeShift` `shiftFunctor` `instHasShiftOppositeShift` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Functor.comp` `Iso.hom` `Functor` `Functor.category` `shiftFunctorAdd` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.obj` `Opposite.unop` `Iso.inv`	—	`cancel_mono` `mono_of_strongMono` `strongMono_of_isIso` `NatIso.inv_app_isIso` `Iso.hom_inv_id_app` `oppositeShiftFunctorAdd_inv_app` `op_comp` `op_id`
`oppositeShiftFunctorAdd_inv_app` 📖	mathematical	—	`NatTrans.app` `OppositeShift` `instCategoryOppositeShift` `Functor.comp` `shiftFunctor` `instHasShiftOppositeShift` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Iso.inv` `Functor` `Functor.category` `shiftFunctorAdd` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.obj` `Opposite.unop` `Iso.hom`	—	—
`oppositeShiftFunctorZero_hom_app` 📖	mathematical	—	`NatTrans.app` `OppositeShift` `instCategoryOppositeShift` `shiftFunctor` `instHasShiftOppositeShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Functor.id` `Iso.hom` `Functor` `Functor.category` `shiftFunctorZero` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.obj` `Opposite.unop` `Iso.inv`	—	`cancel_mono` `mono_of_strongMono` `strongMono_of_isIso` `NatIso.inv_app_isIso` `Iso.hom_inv_id_app` `oppositeShiftFunctorZero_inv_app` `op_comp` `op_id`
`oppositeShiftFunctorZero_inv_app` 📖	mathematical	—	`NatTrans.app` `OppositeShift` `instCategoryOppositeShift` `Functor.id` `shiftFunctor` `instHasShiftOppositeShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Iso.inv` `Functor` `Functor.category` `shiftFunctorZero` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Functor.obj` `Opposite.unop` `Iso.hom`	—	—

CategoryTheory.Adjunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift_op` 📖	mathematical	—	`CommShift` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `CategoryTheory.OppositeShift.functor` `CategoryTheory.OppositeShift.adjunction` `CategoryTheory.instHasShiftOppositeShift` `CategoryTheory.Functor.commShiftOp`	—	`CategoryTheory.NatTrans.CommShift.comp` `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId` `CategoryTheory.NatTrans.commShift_op` `CommShift.commShift_counit` `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp` `CategoryTheory.NatTrans.CommShift.of_iso_inv` `CommShift.commShift_unit`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`commShiftOp` 📖	CompOp	5 math math: `commShiftOp_iso_eq`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId`, `CategoryTheory.NatTrans.commShift_op`, `CategoryTheory.Adjunction.commShift_op`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp`
`commShiftUnop` 📖	CompOp	1 math math: `commShiftUnop_commShiftIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftOp_iso_eq` 📖	mathematical	—	`CommShift.commShiftIso` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `CategoryTheory.OppositeShift.functor` `CategoryTheory.instHasShiftOppositeShift` `commShiftOp` `CategoryTheory.Iso.symm` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `category` `op` `comp` `CategoryTheory.shiftFunctor` `CategoryTheory.NatIso.op`	—	—
`commShiftUnop_commShiftIso` 📖	mathematical	—	`CommShift.commShiftIso` `commShiftUnop` `CategoryTheory.NatIso.removeOp` `comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.symm` `CategoryTheory.Functor` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `category` `CategoryTheory.instHasShiftOppositeShift` `CategoryTheory.OppositeShift.functor`	—	—

CategoryTheory.HasShift

Definitions

Name	Category	Theorems
`mkShiftCoreOp` 📖	CompOp	—

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift_op` 📖	mathematical	—	`CommShift` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `CategoryTheory.OppositeShift.functor` `CategoryTheory.OppositeShift.natTrans` `CategoryTheory.instHasShiftOppositeShift` `CategoryTheory.Functor.commShiftOp`	—	`ext'` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.strongMono_of_isIso` `CategoryTheory.NatIso.inv_app_isIso` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Category.comp_id` `Opposite.op_inj_iff` `shift_app_comm`
`instCommShiftOppositeShiftHomFunctorNatIsoComp` 📖	mathematical	—	`CommShift` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `CategoryTheory.OppositeShift.functor` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `OppositeShift.natIsoComp` `CategoryTheory.instHasShiftOppositeShift` `CategoryTheory.Functor.commShiftOp` `CategoryTheory.Functor.CommShift.comp`	—	`ext'` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`instCommShiftOppositeShiftHomFunctorNatIsoId` 📖	mathematical	—	`CommShift` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `CategoryTheory.Functor.id` `CategoryTheory.OppositeShift.functor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `OppositeShift.natIsoId` `CategoryTheory.instHasShiftOppositeShift` `CategoryTheory.Functor.CommShift.id` `CategoryTheory.Functor.commShiftOp`	—	`ext'` `CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.commShiftIso_id_inv_app` `CategoryTheory.Category.id_comp`

CategoryTheory.NatTrans.OppositeShift

Definitions

Name	Category	Theorems
`natIsoComp` 📖	CompOp	3 math math: `CategoryTheory.OppositeShift.adjunction_unit`, `CategoryTheory.OppositeShift.adjunction_counit`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp`
`natIsoId` 📖	CompOp	3 math math: `CategoryTheory.OppositeShift.adjunction_unit`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId`, `CategoryTheory.OppositeShift.adjunction_counit`

CategoryTheory.OppositeShift

Definitions

Name	Category	Theorems
`adjunction` 📖	CompOp	3 math math: `adjunction_unit`, `CategoryTheory.Adjunction.commShift_op`, `adjunction_counit`
`functor` 📖	CompOp	8 math math: `CategoryTheory.Functor.commShiftOp_iso_eq`, `adjunction_unit`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoId`, `CategoryTheory.NatTrans.commShift_op`, `CategoryTheory.Adjunction.commShift_op`, `adjunction_counit`, `CategoryTheory.NatTrans.instCommShiftOppositeShiftHomFunctorNatIsoComp`, `CategoryTheory.Functor.commShiftUnop_commShiftIso`
`natTrans` 📖	CompOp	3 math math: `adjunction_unit`, `CategoryTheory.NatTrans.commShift_op`, `adjunction_counit`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjunction_counit` 📖	mathematical	—	`CategoryTheory.Adjunction.counit` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `functor` `adjunction` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.id` `CategoryTheory.Iso.inv` `CategoryTheory.NatTrans.OppositeShift.natIsoComp` `natTrans` `CategoryTheory.Adjunction.unit` `CategoryTheory.NatTrans.OppositeShift.natIsoId`	—	—
`adjunction_unit` 📖	mathematical	—	`CategoryTheory.Adjunction.unit` `CategoryTheory.OppositeShift` `CategoryTheory.instCategoryOppositeShift` `functor` `adjunction` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.NatTrans.OppositeShift.natIsoId` `natTrans` `CategoryTheory.Adjunction.counit` `CategoryTheory.NatTrans.OppositeShift.natIsoComp`	—	—

---

← Back to Index