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	10 math math: DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc, homologyFunctor_shift, homologySequenceδ_quotient_mapTriangle_obj_assoc, homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, DerivedCategory.shiftMap_homologyFunctor_map_Q, 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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.homologyFunctor Int.instAddMonoid instHasShiftInt instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat	—	instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono
instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso 📖	mathematical	—	CategoryTheory.MorphismProperty.IsCompatibleWithShift HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso Int.instAddMonoid instHasShiftInt	—	instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.cycles 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 CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc HomologicalComplex.homology HomologicalComplex.liftCycles HomologicalComplex.homologyπ HomologicalComplex instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono CategoryTheory.Functor.comp CategoryTheory.Functor.shift HomologicalComplex.homologyFunctor instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat HomologicalComplex.X CategoryTheory.Iso.hom shiftFunctor shiftFunctorObjXIso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.shiftIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.cycles 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 CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.sc HomologicalComplex.liftCycles HomologicalComplex.homology HomologicalComplex.homologyπ HomologicalComplex.X CategoryTheory.Iso.hom shiftFunctor shiftFunctorObjXIso CategoryTheory.NatTrans.app HomologicalComplex instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono CategoryTheory.Functor.shift HomologicalComplex.homologyFunctor instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.shiftIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono
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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Functor.map CategoryTheory.shiftFunctorAdd'	—	CategoryTheory.ShortComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 HomologicalComplex.X Units Int.instMonoid CategoryTheory.Iso HomologicalComplex.eval CategoryTheory.Preadditive.instSMulUnitsIntIso Int.negOnePow CategoryTheory.Iso.app shiftEval	—	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 HomologicalComplex.X Units Int.instMonoid CategoryTheory.Iso HomologicalComplex.eval CategoryTheory.Preadditive.instSMulUnitsIntIso Int.negOnePow CategoryTheory.Iso.app shiftEval	—	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 HomologicalComplex.X Units Int.instMonoid CategoryTheory.Iso HomologicalComplex.eval CategoryTheory.Preadditive.instSMulUnitsIntIso Int.negOnePow CategoryTheory.Iso.app shiftEval	—	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 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 HomologicalComplex.X Units Int.instMonoid CategoryTheory.Iso HomologicalComplex.eval CategoryTheory.Preadditive.instSMulUnitsIntIso Int.negOnePow CategoryTheory.Iso.app shiftEval	—	AddRightCancelSemigroup.toIsRightCancelAdd
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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono CategoryTheory.Functor.obj CategoryTheory.shiftFunctor instHasShiftInt AddZero.toZero AddZeroClass.toAddZero CategoryTheory.Functor.id CategoryTheory.shiftFunctorZero	—	CategoryTheory.ShortComplex.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd zero_add instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono 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 AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CochainComplex.shiftFunctor HomologicalComplex.shortComplexFunctor CochainComplex.shiftShortComplexFunctorIso CategoryTheory.CategoryWithHomology.hasHomology	—	instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono 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 AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory HomologicalComplex.shortComplexFunctor CochainComplex.shiftFunctor CochainComplex.shiftShortComplexFunctorIso CategoryTheory.CategoryWithHomology.hasHomology	—	instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

HomotopyCategory

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologyFunctor_shiftMap 📖	mathematical	—	CategoryTheory.Functor.shiftMap HomotopyCategory ComplexShape.up instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory homologyFunctor Int.instAddMonoid hasShift instShiftSequenceIntUpHomologyFunctorOfNat CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instCategory AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd quotient CategoryTheory.ShiftedHom.map CochainComplex.instHasShiftInt commShiftQuotient CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex CategoryTheory.Functor.comp HomologicalComplex.homologyFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category homologyFunctorFactors CategoryTheory.Functor.shift CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.ShiftSequence.induced_shiftMap instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono
homologyFunctor_shiftMap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj HomotopyCategory ComplexShape.up instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Functor.shift homologyFunctor Int.instAddMonoid hasShift instShiftSequenceIntUpHomologyFunctorOfNat CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instCategory AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd quotient CategoryTheory.Functor.shiftMap CategoryTheory.ShiftedHom.map CochainComplex.instHasShiftInt commShiftQuotient HomologicalComplex HomologicalComplex.homologyFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category homologyFunctorFactors CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono Mathlib.Tactic.Reassoc.eq_whisker' homologyFunctor_shiftMap
homologyShiftIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopyCategory ComplexShape.up instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono 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 AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono

---

← Back to Index