ShiftSequence

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean

Statistics

Metric	Count
Definitions shiftIso, instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat, shiftShortComplexFunctor', shiftShortComplexFunctorIso, instShiftSequenceIntUpHomologyFunctorOfNat	5
Theorems shiftIso_hom_app, shiftIso_inv_app, homologyFunctor_shift, instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso, instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, liftCycles_shift_homologyπ, liftCycles_shift_homologyπ_assoc, quasiIsoAt_shift_iff, quasiIso_shift_iff, shiftShortComplexFunctor'_hom_app_τ₁, shiftShortComplexFunctor'_hom_app_τ₂, shiftShortComplexFunctor'_hom_app_τ₃, shiftShortComplexFunctor'_inv_app_τ₁, shiftShortComplexFunctor'_inv_app_τ₂, shiftShortComplexFunctor'_inv_app_τ₃, shiftShortComplexFunctorIso_add'_hom_app, shiftShortComplexFunctorIso_hom_app_τ₁, shiftShortComplexFunctorIso_hom_app_τ₂, shiftShortComplexFunctorIso_hom_app_τ₃, shiftShortComplexFunctorIso_inv_app_τ₁, shiftShortComplexFunctorIso_inv_app_τ₂, shiftShortComplexFunctorIso_inv_app_τ₃, shiftShortComplexFunctorIso_zero_add_hom_app, homologyFunctor_shiftMap, homologyFunctor_shiftMap_assoc, homologyShiftIso_hom_app	26
Total	31

CochainComplex

Definitions

Name	Category	Theorems
instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat 📖	CompOp	8 math math: homologyFunctor_shift, homologySequenceδ_quotient_mapTriangle_obj_assoc, homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, HomotopyCategory.homologyShiftIso_hom_app, HomotopyCategory.homologyFunctor_shiftMap, liftCycles_shift_homologyπ_assoc, liftCycles_shift_homologyπ
shiftShortComplexFunctor' 📖	CompOp	6 math math: shiftShortComplexFunctor'_hom_app_τ₁, shiftShortComplexFunctor'_hom_app_τ₂, shiftShortComplexFunctor'_hom_app_τ₃, shiftShortComplexFunctor'_inv_app_τ₃, shiftShortComplexFunctor'_inv_app_τ₂, shiftShortComplexFunctor'_inv_app_τ₁
shiftShortComplexFunctorIso 📖	CompOp	10 math math: shiftShortComplexFunctorIso_hom_app_τ₂, shiftShortComplexFunctorIso_hom_app_τ₃, shiftShortComplexFunctorIso_add'_hom_app, shiftShortComplexFunctorIso_hom_app_τ₁, shiftShortComplexFunctorIso_inv_app_τ₂, shiftShortComplexFunctorIso_zero_add_hom_app, shiftShortComplexFunctorIso_inv_app_τ₃, ShiftSequence.shiftIso_inv_app, shiftShortComplexFunctorIso_inv_app_τ₁, ShiftSequence.shiftIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologyFunctor_shift 📖	mathematical	—	CategoryTheory.Functor.shift HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.homologyFunctor Int.instAddMonoid instHasShiftInt instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat	—	AddRightCancelSemigroup.toIsRightCancelAdd
instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsCompatibleWithShift HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.MorphismProperty.ext quasiIso_shift_iff
instQuasiIsoIntMapHomologicalComplexUpShiftFunctor 📖	mathematical	—	QuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Functor.map CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology quasiIso_shift_iff
liftCycles_shift_homologyπ 📖	mathematical	ComplexShape.next ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.cycles CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc HomologicalComplex.homology HomologicalComplex.liftCycles HomologicalComplex.homologyπ HomologicalComplex CategoryTheory.Functor.comp CategoryTheory.Functor.shift HomologicalComplex.homologyFunctor instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Iso.hom shiftFunctor shiftFunctorObjXIso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.shiftIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id ShiftSequence.shiftIso_inv_app CategoryTheory.ShortComplex.homologyπ_naturality CategoryTheory.ShortComplex.liftCycles_comp_cyclesMap_assoc CategoryTheory.ShortComplex.liftCycles.congr_simp
liftCycles_shift_homologyπ_assoc 📖	mathematical	ComplexShape.next ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.cycles CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc HomologicalComplex.liftCycles HomologicalComplex.homology HomologicalComplex.homologyπ CategoryTheory.Iso.hom shiftFunctor shiftFunctorObjXIso CategoryTheory.NatTrans.app HomologicalComplex CategoryTheory.Functor.shift HomologicalComplex.homologyFunctor instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.shiftIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCycles_shift_homologyπ
quasiIsoAt_shift_iff 📖	mathematical	—	QuasiIsoAt CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Functor.map CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.NatIso.isIso_map_iff
quasiIso_shift_iff 📖	mathematical	—	QuasiIso CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Functor.map CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology quasiIsoAt_shift_iff
shiftShortComplexFunctor'_hom_app_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.shortComplexFunctor' CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftShortComplexFunctor' Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctor'_hom_app_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.shortComplexFunctor' CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftShortComplexFunctor' HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctor'_hom_app_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.shortComplexFunctor' CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftShortComplexFunctor' Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctor'_inv_app_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftShortComplexFunctor' Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd Int.units_inv_eq_self
shiftShortComplexFunctor'_inv_app_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftShortComplexFunctor' HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctor'_inv_app_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftShortComplexFunctor' Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd Int.units_inv_eq_self
shiftShortComplexFunctorIso_add'_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp shiftFunctor HomologicalComplex.shortComplexFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftShortComplexFunctorIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Functor.map CategoryTheory.shiftFunctorAdd'	—	CategoryTheory.ShortComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd Int.negOnePow_add shiftFunctorAdd'_hom_app_f' CategoryTheory.Linear.comp_units_smul CategoryTheory.Linear.units_smul_comp HomologicalComplex.XIsoOfEq_hom_comp_XIsoOfEq_hom smul_smul
shiftShortComplexFunctorIso_hom_app_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.shortComplexFunctor' ComplexShape.prev ComplexShape.next CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctor HomologicalComplex.shortComplexFunctor shiftShortComplexFunctorIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctorIso_hom_app_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.shortComplexFunctor' ComplexShape.prev ComplexShape.next CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctor HomologicalComplex.shortComplexFunctor shiftShortComplexFunctorIso HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctorIso_hom_app_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.shortComplexFunctor' ComplexShape.prev ComplexShape.next CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctor HomologicalComplex.shortComplexFunctor shiftShortComplexFunctorIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctorIso_inv_app_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' ComplexShape.prev ComplexShape.next CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctor HomologicalComplex.shortComplexFunctor shiftShortComplexFunctorIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd Int.units_inv_eq_self
shiftShortComplexFunctorIso_inv_app_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' ComplexShape.prev ComplexShape.next CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctor HomologicalComplex.shortComplexFunctor shiftShortComplexFunctorIso HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftShortComplexFunctorIso_inv_app_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor' ComplexShape.prev ComplexShape.next CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctor HomologicalComplex.shortComplexFunctor shiftShortComplexFunctorIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd Int.units_inv_eq_self
shiftShortComplexFunctorIso_zero_add_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.Functor.comp shiftFunctor HomologicalComplex.shortComplexFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftShortComplexFunctorIso zero_add AddMonoid.toAddZeroClass Int.instAddMonoid CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Functor.obj CategoryTheory.shiftFunctor instHasShiftInt AddZero.toZero AddZeroClass.toAddZero CategoryTheory.Functor.id CategoryTheory.shiftFunctorZero	—	CategoryTheory.ShortComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd zero_add one_smul shiftFunctorZero_hom_app_f

CochainComplex.ShiftSequence

Definitions

Name	Category	Theorems
shiftIso 📖	CompOp	2 math math: shiftIso_inv_app, shiftIso_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shiftIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt HomologicalComplex.homologyFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category shiftIso CategoryTheory.ShortComplex.homologyMap CategoryTheory.Functor.obj CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CochainComplex.shiftFunctor HomologicalComplex.shortComplexFunctor CochainComplex.shiftShortComplexFunctorIso CategoryTheory.CategoryWithHomology.hasHomology	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
shiftIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.homologyFunctor CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category shiftIso CategoryTheory.ShortComplex.homologyMap CategoryTheory.Functor.obj CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor CochainComplex.shiftFunctor CochainComplex.shiftShortComplexFunctorIso CategoryTheory.CategoryWithHomology.hasHomology	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

HomotopyCategory

Definitions

Name	Category	Theorems
instShiftSequenceIntUpHomologyFunctorOfNat 📖	CompOp	6 math math: CochainComplex.mappingCone.homologySequenceδ_triangleh, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, homologyFunctor_shiftMap_assoc, homologyShiftIso_hom_app, homologyFunctor_shiftMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologyFunctor_shiftMap 📖	mathematical	—	CategoryTheory.Functor.shiftMap HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory homologyFunctor Int.instAddMonoid hasShift instShiftSequenceIntUpHomologyFunctorOfNat CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory quotient AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CochainComplex CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso commShiftQuotient HomologicalComplex.homologyFunctor homologyFunctorFactors CategoryTheory.Functor.shift CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.ShiftSequence.induced_shiftMap
homologyFunctor_shiftMap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Functor.shift homologyFunctor Int.instAddMonoid hasShift instShiftSequenceIntUpHomologyFunctorOfNat HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory quotient AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.shiftMap CochainComplex CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso commShiftQuotient HomologicalComplex.homologyFunctor homologyFunctorFactors CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyFunctor_shiftMap
homologyShiftIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid hasShift CategoryTheory.Functor.shift homologyFunctor instShiftSequenceIntUpHomologyFunctorOfNat CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.shiftIso CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory quotient CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex.instHasShiftInt CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Functor.CommShift.commShiftIso commShiftQuotient HomologicalComplex.homologyFunctor homologyFunctorFactors CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat	—	CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index