Documentation Verification Report

CommShiftTwo

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

Statistics

Metric	Count
Definitions `CommShift₂Setup`, `int`, `toTwistShiftData`, `ε`, `CommShift₂`, `commShiftFlipObj`, `commShiftObj`, `precomp₁`, `precomp₂`, `CommShift₂Int`, `CommShift₂`, `CommShift₂Int`	12
Theorems `hε`, `int_z`, `int_ε`, `z_zero₁`, `z_zero₂`, `comm`, `commShift_flip_map`, `commShift_map`, `commShift₂_comm`, `commShift₂_comm_assoc`, `commShift_app`, `commShift_flipApp`, `instCompFunctor`, `instIdFunctor`	14
Total	26

CategoryTheory

Definitions

Name	Category	Theorems
`CommShift₂Setup` 📖	CompData	—

CategoryTheory.CommShift₂Setup

Definitions

Name	Category	Theorems
`int` 📖	CompOp	2 math math: `int_ε`, `int_z`
`toTwistShiftData` 📖	CompOp	4 math math: `z_zero₂`, `z_zero₁`, `hε`, `int_z`
`ε` 📖	CompOp	5 math math: `CategoryTheory.Functor.commShift₂_comm`, `CategoryTheory.Functor.CommShift₂.comm`, `int_ε`, `CategoryTheory.Functor.commShift₂_comm_assoc`, `hε`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hε` 📖	mathematical	—	`ε` `Units` `CategoryTheory.CatCenter` `CategoryTheory.PullbackShift` `Prod.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom.add` `AddMonoidHom.fst` `AddMonoidHom.snd` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `Units.instMul` `Units.instInv` `CategoryTheory.TwistShiftData.z` `CategoryTheory.instHasShiftPullbackShift` `toTwistShiftData` `AddZero.toZero`	—	—
`int_z` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`CategoryTheory.TwistShiftData.z` `CategoryTheory.PullbackShift` `Prod.instAddMonoid` `AddCommMonoid.toAddMonoid` `Int.instAddCommMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom.add` `AddMonoidHom.fst` `AddMonoidHom.snd` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.instHasShiftPullbackShift` `toTwistShiftData` `int` `Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `DivInvMonoid.toZPow` `Units.instDivInvMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CategoryTheory.Preadditive.instRingEnd` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.instPreadditivePullbackShift` `Units.instOne`	—	—
`int_ε` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid`	`ε` `Int.instAddCommMonoid` `int` `Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `DivInvMonoid.toZPow` `Units.instDivInvMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `CategoryTheory.Preadditive.instRingEnd` `CategoryTheory.functorCategoryPreadditive` `Units.instOne`	—	—
`z_zero₁` 📖	mathematical	—	`CategoryTheory.TwistShiftData.z` `CategoryTheory.PullbackShift` `Prod.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom.add` `AddMonoidHom.fst` `AddMonoidHom.snd` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.instHasShiftPullbackShift` `toTwistShiftData` `AddZero.toZero` `Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `Units.instOne`	—	—
`z_zero₂` 📖	mathematical	—	`CategoryTheory.TwistShiftData.z` `CategoryTheory.PullbackShift` `Prod.instAddMonoid` `AddCommMonoid.toAddMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `Prod.instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidHom.add` `AddMonoidHom.fst` `AddMonoidHom.snd` `CategoryTheory.instCategoryPullbackShift` `CategoryTheory.instHasShiftPullbackShift` `toTwistShiftData` `AddZero.toZero` `Units` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id` `Units.instOne`	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`CommShift₂` 📖	CompData	—
`CommShift₂Int` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift₂_comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `comp` `CategoryTheory.shiftFunctor` `AddCommMonoid.toAddMonoid` `CategoryTheory.Functor` `category` `flip` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CommShift.commShiftIso` `CommShift₂.commShiftObj` `map` `CommShift₂.commShiftFlipObj` `CategoryTheory.Iso.inv` `CategoryTheory.shiftComm` `CategoryTheory.CatCenter.app` `Units.val` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `id` `CategoryTheory.CommShift₂Setup.ε`	—	`CommShift₂.comm`
`commShift₂_comm_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `obj` `CategoryTheory.Functor` `category` `CategoryTheory.shiftFunctor` `AddCommMonoid.toAddMonoid` `CategoryTheory.NatTrans.app` `comp` `CategoryTheory.Iso.hom` `CommShift.commShiftIso` `CommShift₂.commShiftObj` `flip` `map` `CommShift₂.commShiftFlipObj` `CategoryTheory.Iso.inv` `CategoryTheory.shiftComm` `CategoryTheory.CatCenter.app` `Units.val` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `id` `CategoryTheory.CommShift₂Setup.ε`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `commShift₂_comm`

CategoryTheory.Functor.CommShift₂

Definitions

Name	Category	Theorems
`commShiftFlipObj` 📖	CompOp	5 math math: `CategoryTheory.Functor.commShift₂_comm`, `commShift_flip_map`, `CategoryTheory.NatTrans.CommShift₂.commShift_flipApp`, `comm`, `CategoryTheory.Functor.commShift₂_comm_assoc`
`commShiftObj` 📖	CompOp	5 math math: `CategoryTheory.Functor.commShift₂_comm`, `commShift_map`, `comm`, `CategoryTheory.Functor.commShift₂_comm_assoc`, `CategoryTheory.NatTrans.CommShift₂.commShift_app`
`precomp₁` 📖	CompOp	—
`precomp₂` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `AddCommMonoid.toAddMonoid` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor.CommShift.commShiftIso` `commShiftObj` `CategoryTheory.Functor.map` `commShiftFlipObj` `CategoryTheory.Iso.inv` `CategoryTheory.shiftComm` `CategoryTheory.CatCenter.app` `Units.val` `CategoryTheory.CatCenter` `CategoryTheory.End.monoid` `CategoryTheory.Functor.id` `CategoryTheory.CommShift₂Setup.ε`	—	—
`commShift_flip_map` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.Functor.map` `AddCommMonoid.toAddMonoid` `commShiftFlipObj`	—	—
`commShift_map` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.map` `AddCommMonoid.toAddMonoid` `commShiftObj`	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
`CommShift₂` 📖	CompData	2 math math: `CommShift₂.instCompFunctor`, `CommShift₂.instIdFunctor`
`CommShift₂Int` 📖	MathDef	—

CategoryTheory.NatTrans.CommShift₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShift_app` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.NatTrans.app` `AddCommMonoid.toAddMonoid` `CategoryTheory.Functor.CommShift₂.commShiftObj`	—	—
`commShift_flipApp` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.NatTrans.flipApp` `AddCommMonoid.toAddMonoid` `CategoryTheory.Functor.CommShift₂.commShiftFlipObj`	—	—
`instCompFunctor` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift₂` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.NatTrans.CommShift.comp` `commShift_app` `CategoryTheory.Functor.map_comp` `commShift_flipApp`
`instIdFunctor` 📖	mathematical	—	`CategoryTheory.NatTrans.CommShift₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.NatTrans.CommShift.id` `CategoryTheory.Functor.map_id`

---

← Back to Index