Documentation Verification Report

InducedShiftSequence

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

Statistics

Metric	Count
Definitions `induced`, `isoZero`, `shiftIso`	3
Theorems `isoZero_hom_app_obj`, `shiftIso_hom_app_obj`, `induced_isoShiftZero_hom_app_obj`, `induced_isoShiftZero_hom_app_obj_assoc`, `induced_shiftIso_hom_app_obj`, `induced_shiftIso_hom_app_obj_assoc`, `induced_shiftMap`, `induced_shiftMap_assoc`	8
Total	11

CategoryTheory.Functor.ShiftSequence

Definitions

Name	Category	Theorems
`induced` 📖	CompOp	6 math math: `induced_shiftIso_hom_app_obj`, `induced_shiftIso_hom_app_obj_assoc`, `induced_isoShiftZero_hom_app_obj_assoc`, `induced_shiftMap`, `induced_isoShiftZero_hom_app_obj`, `induced_shiftMap_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induced_isoShiftZero_hom_app_obj` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.shift` `induced` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.isoShiftZero` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv`	—	`induced.isoZero_hom_app_obj`
`induced_isoShiftZero_hom_app_obj_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.shift` `induced` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.isoShiftZero` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `induced_isoShiftZero_hom_app_obj`
`induced_shiftIso_hom_app_obj` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.shift` `induced` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.shiftIso` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`induced.shiftIso_hom_app_obj`
`induced_shiftIso_hom_app_obj_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.shift` `induced` `CategoryTheory.shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.shiftIso` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.CommShift.commShiftIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `induced_shiftIso_hom_app_obj`
`induced_shiftMap` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.Functor.shiftMap` `induced` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.shift` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.map_comp` `induced_shiftIso_hom_app_obj` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.Iso.hom_inv_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.id_comp` `CategoryTheory.NatTrans.naturality_assoc`
`induced_shiftMap_assoc` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.shift` `induced` `CategoryTheory.Functor.shiftMap` `CategoryTheory.shiftFunctor` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `induced_shiftMap`

CategoryTheory.Functor.ShiftSequence.induced

Definitions

Name	Category	Theorems
`isoZero` 📖	CompOp	1 math math: `isoZero_hom_app_obj`
`shiftIso` 📖	CompOp	1 math math: `shiftIso_hom_app_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isoZero_hom_app_obj` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `isoZero` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.shift` `CategoryTheory.Functor.isoShiftZero` `CategoryTheory.Iso.inv`	—	`CategoryTheory.NatTrans.congr_app` `CategoryTheory.Functor.map_preimage`
`shiftIso_hom_app_obj` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.shiftFunctor` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `shiftIso` `CategoryTheory.Functor.obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.Functor.CommShift.commShiftIso` `CategoryTheory.Functor.shift` `CategoryTheory.Functor.shiftIso`	—	`CategoryTheory.NatTrans.congr_app` `CategoryTheory.Functor.map_preimage` `CategoryTheory.Category.id_comp`

---

← Back to Index