ShiftSequence

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

Statistics

Metric	Count
Definitions ShiftSequence, isoZero, sequence, shiftIso, tautological, isoShift, isoShiftZero, shift, shiftIso, shiftMap	10
Theorems shiftIso_add, shiftIso_zero, instAdditiveShift, instPreservesZeroMorphismsShift, isoShift_hom_naturality, isoShift_hom_naturality_assoc, isoShift_inv_naturality, isoShift_inv_naturality_assoc, shiftIso_add, shiftIso_add', shiftIso_add'_hom_app, shiftIso_add'_inv_app, shiftIso_add_hom_app, shiftIso_add_inv_app, shiftIso_hom_app_comp, shiftIso_hom_app_comp_assoc, shiftIso_hom_app_comp_shiftMap, shiftIso_hom_app_comp_shiftMap_of_add_eq_zero, shiftIso_hom_naturality, shiftIso_hom_naturality_assoc, shiftIso_inv_naturality, shiftIso_inv_naturality_assoc, shiftIso_zero, shiftIso_zero_hom_app, shiftIso_zero_inv_app, shiftMap_comp, shiftMap_comp', shiftMap_comp'_assoc, shiftMap_comp_assoc, shiftMap_zero	30
Total	40

CategoryTheory.Functor

Definitions

Name	Category	Theorems
ShiftSequence 📖	CompData	—
isoShift 📖	CompOp	4 math math: isoShift_inv_naturality_assoc, isoShift_inv_naturality, isoShift_hom_naturality, isoShift_hom_naturality_assoc
isoShiftZero 📖	CompOp	3 math math: ShiftSequence.induced.isoZero_hom_app_obj, ShiftSequence.induced_isoShiftZero_hom_app_obj_assoc, ShiftSequence.induced_isoShiftZero_hom_app_obj
shift 📖	CompOp	66 math math: shiftIso_add_inv_app, shiftIso_add', shiftIso_hom_app_comp, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, homologySequence_comp_assoc, shiftIso_zero_inv_app, homologySequence_comp, mem_homologicalKernel_iff, ShiftSequence.induced.isoZero_hom_app_obj, shiftMap_comp', homologySequenceδ_naturality, shiftIso_zero_hom_app, isoShift_inv_naturality_assoc, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, isoShift_inv_naturality, CochainComplex.homologyFunctor_shift, isoShift_hom_naturality, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, shiftIso_add_hom_app, shiftMap_comp, shiftIso_add'_hom_app, shiftIso_inv_naturality, homologySequence_epi_shift_map_mor₁_iff, shiftMap_comp'_assoc, instPreservesZeroMorphismsShift, homologySequence_exact₂, ShiftSequence.induced_shiftIso_hom_app_obj, homologySequenceδ_comp_assoc, homologySequence_mono_shift_map_mor₁_iff, shiftIso_zero, CategoryTheory.Pretriangulated.preadditiveYoneda_homologySequenceδ_apply, shiftIso_add, ShiftSequence.induced.shiftIso_hom_app_obj, ShiftSequence.induced_shiftIso_hom_app_obj_assoc, comp_homologySequenceδ, ShiftSequence.induced_isoShiftZero_hom_app_obj_assoc, homologySequence_exact₃, shiftMap_zero, shiftIso_hom_naturality_assoc, shiftIso_hom_app_comp_assoc, homologySequence_exact₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, isoShift_hom_naturality_assoc, shiftIso_hom_app_comp_shiftMap, shiftIso_add'_inv_app, HomotopyCategory.homologyShiftIso_hom_app, homologySequenceδ_naturality_assoc, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, shiftIso_inv_naturality_assoc, instAdditiveShift, ShiftSequence.induced_shiftMap, HomotopyCategory.homologyFunctor_shiftMap, shiftMap_comp_assoc, ShiftSequence.induced_isoShiftZero_hom_app_obj, shiftIso_hom_app_comp_shiftMap_of_add_eq_zero, shiftIso_hom_naturality, CochainComplex.liftCycles_shift_homologyπ_assoc, homologySequenceδ_comp, ShiftSequence.induced_shiftMap_assoc, homologySequence_mono_shift_map_mor₂_iff, comp_homologySequenceδ_assoc, mem_homologicalKernel_trW_iff, CochainComplex.liftCycles_shift_homologyπ, CategoryTheory.Pretriangulated.preadditiveCoyoneda_homologySequenceδ_apply, homologySequence_epi_shift_map_mor₂_iff
shiftIso 📖	CompOp	23 math math: shiftIso_add_inv_app, shiftIso_add', shiftIso_hom_app_comp, shiftIso_zero_inv_app, shiftIso_zero_hom_app, shiftIso_add_hom_app, shiftIso_add'_hom_app, shiftIso_inv_naturality, ShiftSequence.induced_shiftIso_hom_app_obj, shiftIso_zero, shiftIso_add, ShiftSequence.induced.shiftIso_hom_app_obj, ShiftSequence.induced_shiftIso_hom_app_obj_assoc, shiftIso_hom_naturality_assoc, shiftIso_hom_app_comp_assoc, shiftIso_hom_app_comp_shiftMap, shiftIso_add'_inv_app, HomotopyCategory.homologyShiftIso_hom_app, shiftIso_inv_naturality_assoc, shiftIso_hom_app_comp_shiftMap_of_add_eq_zero, shiftIso_hom_naturality, CochainComplex.liftCycles_shift_homologyπ_assoc, CochainComplex.liftCycles_shift_homologyπ
shiftMap 📖	CompOp	14 math math: shiftMap_comp', CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, shiftMap_comp, shiftMap_comp'_assoc, shiftMap_zero, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, shiftIso_hom_app_comp_shiftMap, CategoryTheory.Pretriangulated.preadditiveYoneda_shiftMap_apply, ShiftSequence.induced_shiftMap, HomotopyCategory.homologyFunctor_shiftMap, shiftMap_comp_assoc, shiftIso_hom_app_comp_shiftMap_of_add_eq_zero, ShiftSequence.induced_shiftMap_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveShift 📖	mathematical	Additive CategoryTheory.shiftFunctor	shift	—	additive_of_iso instAdditiveComp
instPreservesZeroMorphismsShift 📖	mathematical	PreservesZeroMorphisms CategoryTheory.shiftFunctor	shift	—	preservesZeroMorphisms_of_iso preservesZeroMorphisms_comp
isoShift_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.shiftFunctor shift map CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category isoShift	—	CategoryTheory.NatTrans.naturality
isoShift_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.shiftFunctor map shift CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category isoShift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoShift_hom_naturality
isoShift_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift comp CategoryTheory.shiftFunctor map CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category isoShift	—	CategoryTheory.NatTrans.naturality
isoShift_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift map CategoryTheory.shiftFunctor CategoryTheory.NatTrans.app comp CategoryTheory.Iso.inv CategoryTheory.Functor category isoShift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoShift_inv_naturality
shiftIso_add 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftIso CategoryTheory.Iso.trans CategoryTheory.Functor category comp CategoryTheory.shiftFunctor shift isoWhiskerRight CategoryTheory.shiftFunctorAdd associator isoWhiskerLeft	—	ShiftSequence.shiftIso_add
shiftIso_add' 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftIso CategoryTheory.Iso.trans CategoryTheory.Functor category comp CategoryTheory.shiftFunctor shift isoWhiskerRight CategoryTheory.shiftFunctorAdd' associator isoWhiskerLeft	—	CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd shiftIso_add
shiftIso_add'_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app comp CategoryTheory.shiftFunctor shift CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map CategoryTheory.shiftFunctorAdd'	—	shiftIso_add' CategoryTheory.Category.id_comp
shiftIso_add'_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app shift comp CategoryTheory.shiftFunctor CategoryTheory.Iso.inv CategoryTheory.Functor category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map CategoryTheory.shiftFunctorAdd'	—	shiftIso_add' CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
shiftIso_add_hom_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app comp CategoryTheory.shiftFunctor shift CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map CategoryTheory.shiftFunctorAdd	—	shiftIso_add CategoryTheory.Category.id_comp
shiftIso_add_inv_app 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.NatTrans.app shift comp CategoryTheory.shiftFunctor CategoryTheory.Iso.inv CategoryTheory.Functor category shiftIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj map CategoryTheory.shiftFunctorAdd	—	shiftIso_add CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
shiftIso_hom_app_comp 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp CategoryTheory.shiftFunctor shift CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso map CategoryTheory.Iso.inv CategoryTheory.shiftFunctorAdd'	—	shiftIso_add'_hom_app map_comp_assoc CategoryTheory.Iso.inv_hom_id_app map_id CategoryTheory.Category.id_comp
shiftIso_hom_app_comp_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift CategoryTheory.shiftFunctor CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso map CategoryTheory.Iso.inv CategoryTheory.shiftFunctorAdd'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftIso_hom_app_comp
shiftIso_hom_app_comp_shiftMap 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp CategoryTheory.shiftFunctor shift CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso shiftMap map CategoryTheory.Iso.inv CategoryTheory.shiftFunctorAdd'	—	shiftIso_add'_hom_app CategoryTheory.Iso.inv_hom_id_app map_id CategoryTheory.Category.id_comp shiftIso_hom_naturality_assoc
shiftIso_hom_app_comp_shiftMap_of_add_eq_zero 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj comp CategoryTheory.shiftFunctor shift CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso shiftMap map id CategoryTheory.shiftFunctorCompIsoId	—	AddRightCancelSemigroup.toIsRightCancelAdd add_assoc zero_add add_zero shiftIso_hom_app_comp_shiftMap shiftIso_zero_hom_app map_comp
shiftIso_hom_naturality 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift CategoryTheory.shiftFunctor map CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso	—	CategoryTheory.NatTrans.naturality
shiftIso_hom_naturality_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift CategoryTheory.shiftFunctor map CategoryTheory.NatTrans.app comp CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftIso_hom_naturality
shiftIso_inv_naturality 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift comp CategoryTheory.shiftFunctor map CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category shiftIso	—	CategoryTheory.NatTrans.naturality
shiftIso_inv_naturality_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift map CategoryTheory.shiftFunctor CategoryTheory.NatTrans.app comp CategoryTheory.Iso.inv CategoryTheory.Functor category shiftIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftIso_inv_naturality
shiftIso_zero 📖	mathematical	—	shiftIso AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass zero_add CategoryTheory.Iso.trans CategoryTheory.Functor category comp CategoryTheory.shiftFunctor shift id isoWhiskerRight CategoryTheory.shiftFunctorZero leftUnitor	—	ShiftSequence.shiftIso_zero
shiftIso_zero_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app comp CategoryTheory.shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass shift CategoryTheory.Iso.hom CategoryTheory.Functor category shiftIso zero_add map obj id CategoryTheory.shiftFunctorZero	—	zero_add shiftIso_zero CategoryTheory.Category.comp_id
shiftIso_zero_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app shift comp CategoryTheory.shiftFunctor AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Iso.inv CategoryTheory.Functor category shiftIso zero_add map obj id CategoryTheory.shiftFunctorZero	—	zero_add shiftIso_zero CategoryTheory.Category.id_comp
shiftMap_comp 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.shiftFunctor map shift	—	map_comp CategoryTheory.Category.assoc shiftIso_hom_naturality
shiftMap_comp' 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj CategoryTheory.shiftFunctor shift map	—	map_comp CategoryTheory.Category.assoc
shiftMap_comp'_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift shiftMap CategoryTheory.shiftFunctor map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftMap_comp'
shiftMap_comp_assoc 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj shift shiftMap CategoryTheory.shiftFunctor map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shiftMap_comp
shiftMap_zero 📖	mathematical	PreservesZeroMorphisms CategoryTheory.shiftFunctor AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftMap Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Limits.HasZeroMorphisms.zero shift	—	map_zero instPreservesZeroMorphismsShift CategoryTheory.Limits.zero_comp

CategoryTheory.Functor.ShiftSequence

Definitions

Name	Category	Theorems
isoZero 📖	CompOp	—
sequence 📖	CompOp	2 math math: shiftIso_add, shiftIso_zero
shiftIso 📖	CompOp	2 math math: shiftIso_add, shiftIso_zero
tautological 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shiftIso_add 📖	mathematical	AddSemigroup.toAdd AddMonoid.toAddSemigroup	shiftIso CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.shiftFunctor sequence CategoryTheory.Functor.isoWhiskerRight CategoryTheory.shiftFunctorAdd CategoryTheory.Functor.associator CategoryTheory.Functor.isoWhiskerLeft	—	—
shiftIso_zero 📖	mathematical	—	shiftIso AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass zero_add CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.shiftFunctor sequence CategoryTheory.Functor.id CategoryTheory.Functor.isoWhiskerRight CategoryTheory.shiftFunctorZero CategoryTheory.Functor.leftUnitor	—	—

---

← Back to Index