Induced

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

Statistics

Metric	Count
Definitions ofInduced, add, zero, induced	4
Theorems commShiftIso_eq_ofInduced, add_hom_app_obj, add_inv_app_obj, zero_hom_app_obj, zero_inv_app_obj, shiftFunctorAdd_hom_app_obj_of_induced, shiftFunctorAdd_inv_app_obj_of_induced, shiftFunctorZero_hom_app_obj_of_induced, shiftFunctorZero_inv_app_obj_of_induced, shiftFunctor_of_induced	10
Total	14

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shiftFunctorAdd_hom_app_obj_of_induced 📖	mathematical	—	NatTrans.app shiftFunctor HasShift.induced AddSemigroup.toAdd AddMonoid.toAddSemigroup Functor.comp Iso.hom Functor Functor.category shiftFunctorAdd Functor.obj CategoryStruct.comp Category.toCategoryStruct Functor.map Iso.inv	—	HasShift.Induced.add_hom_app_obj
shiftFunctorAdd_inv_app_obj_of_induced 📖	mathematical	—	NatTrans.app Functor.comp shiftFunctor HasShift.induced AddSemigroup.toAdd AddMonoid.toAddSemigroup Iso.inv Functor Functor.category shiftFunctorAdd Functor.obj CategoryStruct.comp Category.toCategoryStruct Functor.map Iso.hom	—	HasShift.Induced.add_inv_app_obj
shiftFunctorZero_hom_app_obj_of_induced 📖	mathematical	—	NatTrans.app shiftFunctor HasShift.induced AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Functor.id Iso.hom Functor Functor.category shiftFunctorZero Functor.obj CategoryStruct.comp Category.toCategoryStruct Functor.comp Functor.map	—	HasShift.Induced.zero_hom_app_obj
shiftFunctorZero_inv_app_obj_of_induced 📖	mathematical	—	NatTrans.app Functor.id shiftFunctor HasShift.induced AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Iso.inv Functor Functor.category shiftFunctorZero Functor.obj CategoryStruct.comp Category.toCategoryStruct Functor.comp Functor.map	—	HasShift.Induced.zero_inv_app_obj
shiftFunctor_of_induced 📖	mathematical	—	shiftFunctor HasShift.induced	—	—

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commShiftIso_eq_ofInduced 📖	mathematical	—	CommShift.commShiftIso CategoryTheory.HasShift.induced CommShift.ofInduced CategoryTheory.Iso.symm CategoryTheory.Functor category comp CategoryTheory.shiftFunctor	—	—

CategoryTheory.Functor.CommShift

Definitions

Name	Category	Theorems
ofInduced 📖	CompOp	1 math math: CategoryTheory.Functor.commShiftIso_eq_ofInduced

CategoryTheory.HasShift

Definitions

Name	Category	Theorems
induced 📖	CompOp	6 math math: CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced, CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced, CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced, CategoryTheory.shiftFunctor_of_induced, CategoryTheory.Functor.commShiftIso_eq_ofInduced, CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced

CategoryTheory.HasShift.Induced

Definitions

Name	Category	Theorems
add 📖	CompOp	2 math math: add_inv_app_obj, add_hom_app_obj
zero 📖	CompOp	2 math math: zero_inv_app_obj, zero_hom_app_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_hom_app_obj 📖	mathematical	—	CategoryTheory.NatTrans.app AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor CategoryTheory.Functor.map CategoryTheory.shiftFunctorAdd CategoryTheory.Iso.inv	—	CategoryTheory.Functor.map_preimage CategoryTheory.NatTrans.congr_app CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
add_inv_app_obj 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.comp AddSemigroup.toAdd AddMonoid.toAddSemigroup CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category add CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor CategoryTheory.Functor.map CategoryTheory.Iso.hom CategoryTheory.shiftFunctorAdd	—	CategoryTheory.Functor.map_preimage CategoryTheory.NatTrans.congr_app CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
zero_hom_app_obj 📖	mathematical	—	CategoryTheory.NatTrans.app AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category zero CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.comp CategoryTheory.shiftFunctor CategoryTheory.Functor.map CategoryTheory.shiftFunctorZero	—	CategoryTheory.Functor.map_preimage CategoryTheory.NatTrans.congr_app CategoryTheory.Category.comp_id
zero_inv_app_obj 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.id AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category zero CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.shiftFunctor CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.shiftFunctorZero	—	CategoryTheory.Functor.map_preimage CategoryTheory.NatTrans.congr_app CategoryTheory.Category.assoc CategoryTheory.Category.id_comp

---

← Back to Index