Documentation Verification Report

Twist

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

Statistics

Metric	Count
Definitions `TwistShiftData`, `hasShift`, `instCategoryCategory`, `shiftIso`, `shiftMkCore`, `z`	6
Theorems `assoc`, `commShift`, `shiftFunctorAdd'_hom_app`, `shiftFunctorAdd'_inv_app`, `shiftFunctorZero_hom_app`, `shiftFunctorZero_inv_app`, `shiftFunctor_map`, `shift_z_app`, `z_zero_left`, `z_zero_right`, `z_zero_zero`	11
Total	17

CategoryTheory

Definitions

Name	Category	Theorems
`TwistShiftData` 📖	CompData	—

CategoryTheory.TwistShiftData

Definitions

Name	Category	Theorems
`hasShift` 📖	CompOp	5 math math: `shiftFunctorZero_hom_app`, `shiftFunctorAdd'_inv_app`, `shiftFunctorAdd'_hom_app`, `shiftFunctor_map`, `shiftFunctorZero_inv_app`
`instCategoryCategory` 📖	CompOp	5 math math: `shiftFunctorZero_hom_app`, `shiftFunctorAdd'_inv_app`, `shiftFunctorAdd'_hom_app`, `shiftFunctor_map`, `shiftFunctorZero_inv_app`
`shiftIso` 📖	CompOp	5 math math: `shiftFunctorZero_hom_app`, `shiftFunctorAdd'_inv_app`, `shiftFunctorAdd'_hom_app`, `shiftFunctor_map`, `shiftFunctorZero_inv_app`
`shiftMkCore` 📖	CompOp	—
`z` 📖	CompOp	12 math math: `z_zero_zero`, `assoc`, `shift_z_app`, `z_zero_left`, `shiftFunctorAdd'_inv_app`, `shiftFunctorAdd'_hom_app`, `commShift`, `CategoryTheory.CommShift₂Setup.z_zero₂`, `CategoryTheory.CommShift₂Setup.z_zero₁`, `CategoryTheory.CommShift₂Setup.hε`, `CategoryTheory.CommShift₂Setup.int_z`, `z_zero_right`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc` 📖	mathematical	—	`Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `Units.instMul` `z` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`commShift` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.id` `Units.val` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `z` `CategoryTheory.Functor.CommShift.id`	—	—
`shiftFunctorAdd'_hom_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.NatTrans.app` `Category` `instCategoryCategory` `CategoryTheory.shiftFunctor` `hasShift` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorAdd'` `CategoryTheory.CatCenter` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.CatCenter.instSMulHom` `Units.val` `CategoryTheory.End.monoid` `CategoryTheory.Functor.id` `z` `CategoryTheory.CategoryStruct.comp` `shiftIso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id`
`shiftFunctorAdd'_inv_app` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.NatTrans.app` `Category` `instCategoryCategory` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `hasShift` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorAdd'` `CategoryTheory.CatCenter` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.CatCenter.instSMulHom` `Units.val` `CategoryTheory.End.monoid` `CategoryTheory.Functor.id` `Units` `Units.instInv` `z` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Iso.hom` `shiftIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.comp_id` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp`
`shiftFunctorZero_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Category` `instCategoryCategory` `CategoryTheory.shiftFunctor` `hasShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorZero` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `shiftIso`	—	`CategoryTheory.Category.id_comp`
`shiftFunctorZero_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Category` `instCategoryCategory` `CategoryTheory.Functor.id` `CategoryTheory.shiftFunctor` `hasShift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.shiftFunctorZero` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `shiftIso`	—	`CategoryTheory.Category.comp_id`
`shiftFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Category` `instCategoryCategory` `CategoryTheory.shiftFunctor` `hasShift` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `shiftIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.NatTrans.naturality` `CategoryTheory.Iso.hom_inv_id_app_assoc`
`shift_z_app` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.shiftFunctor` `CategoryTheory.CatCenter.app` `Units.val` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `z` `CategoryTheory.Functor.obj`	—	`CategoryTheory.Functor.commShiftIso_id_hom_app` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.NatTrans.shift_app_comm` `commShift`
`z_zero_left` 📖	mathematical	—	`z` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `Units.instOne`	—	`add_zero` `z_zero_right` `mul_one` `zero_add` `LeftCancelSemigroup.toIsLeftCancelMul` `CategoryTheory.CatCenter.instIsMulCommutative` `assoc`
`z_zero_right` 📖	mathematical	—	`z` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `Units.instOne`	—	`add_zero` `z_zero_zero` `mul_one` `LeftCancelSemigroup.toIsLeftCancelMul` `CategoryTheory.CatCenter.instIsMulCommutative` `assoc`
`z_zero_zero` 📖	mathematical	—	`z` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `Units.instOne`	—	—

---

← Back to Index