Shift

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

Statistics

Metric	Count
Definitions commShiftMapCochainComplex, mapCochainComplexShiftIso, instHasShiftInt, shiftEval, shiftFunctor, shiftFunctorAdd', shiftFunctorObjXIso, shiftFunctorZero', shift, commShiftQuotient, hasShift, instCommShiftIntUpMapHomotopyCategory	12
Theorems mapCochainComplexShiftIso_hom_app_f, mapCochainComplexShiftIso_inv_app_f, mapHomologicalComplex_commShiftIso_eq, mapHomologicalComplex_commShiftIso_hom_app_f, mapHomologicalComplex_commShiftIso_inv_app_f, XIsoOfEq_shift, instAdditiveHomologicalComplexIntUpShiftFunctor, instAdditiveIntShiftFunctor, instLinearHomologicalComplexIntUpShiftFunctor, instLinearIntShiftFunctor, shiftEval_hom_app, shiftEval_inv_app, shiftFunctorAdd'_eq, shiftFunctorAdd'_hom_app_f, shiftFunctorAdd'_hom_app_f', shiftFunctorAdd'_inv_app_f, shiftFunctorAdd'_inv_app_f', shiftFunctorAdd_eq, shiftFunctorAdd_hom_app_f, shiftFunctorAdd_inv_app_f, shiftFunctorComm_hom_app_f, shiftFunctorZero'_hom_app_f, shiftFunctorZero'_inv_app_f, shiftFunctorZero_eq, shiftFunctorZero_hom_app_f, shiftFunctorZero_inv_app_f, shiftFunctor_map_f, shiftFunctor_map_f', shiftFunctor_obj_X, shiftFunctor_obj_X', shiftFunctor_obj_d, shiftFunctor_obj_d', instAdditiveIntUpShiftFunctor, instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic, instLinearIntUpShiftFunctor	36
Total	48

CategoryTheory.Functor

Definitions

Name	Category	Theorems
commShiftMapCochainComplex 📖	CompOp	6 math math: mapHomologicalComplex_commShiftIso_eq, instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, mapHomologicalComplex_commShiftIso_inv_app_f, mapHomologicalComplex_commShiftIso_hom_app_f, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, CochainComplex.mappingCone.map_δ
mapCochainComplexShiftIso 📖	CompOp	3 math math: mapHomologicalComplex_commShiftIso_eq, mapCochainComplexShiftIso_inv_app_f, mapCochainComplexShiftIso_hom_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCochainComplexShiftIso_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing obj HomologicalComplex HomologicalComplex.instCategory comp CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup category mapCochainComplexShiftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup	—	preservesZeroMorphisms_of_additive AddRightCancelSemigroup.toIsRightCancelAdd
mapCochainComplexShiftIso_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing obj HomologicalComplex HomologicalComplex.instCategory comp mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup category mapCochainComplexShiftIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup	—	preservesZeroMorphisms_of_additive AddRightCancelSemigroup.toIsRightCancelAdd
mapHomologicalComplex_commShiftIso_eq 📖	mathematical	—	CommShift.commShiftIso 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 mapHomologicalComplex preservesZeroMorphisms_of_additive Int.instAddMonoid CochainComplex.instHasShiftInt commShiftMapCochainComplex mapCochainComplexShiftIso	—	AddRightCancelSemigroup.toIsRightCancelAdd preservesZeroMorphisms_of_additive
mapHomologicalComplex_commShiftIso_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing obj HomologicalComplex HomologicalComplex.instCategory comp CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category CommShift.commShiftIso commShiftMapCochainComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd preservesZeroMorphisms_of_additive
mapHomologicalComplex_commShiftIso_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing obj HomologicalComplex HomologicalComplex.instCategory comp mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category CommShift.commShiftIso commShiftMapCochainComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd preservesZeroMorphisms_of_additive

CochainComplex

Definitions

Name	Category	Theorems
instHasShiftInt 📖	CompOp	250 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, triangleOfDegreewiseSplit_obj₁, mappingConeCompTriangleh_comm₁_assoc, HomComplex.Cochain.rightShiftAddEquiv_symm_apply, HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, mappingConeCompTriangle_obj₂, isStrictlyGE_shift, shiftFunctorZero_eq, HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, HomComplex.Cochain.leftShift_smul, mappingCone.triangle_mor₁, shiftShortComplexFunctorIso_hom_app_τ₂, shiftShortComplexFunctorIso_hom_app_τ₃, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, HomComplex.Cocycle.equivHomShift_symm_postcomp, instLinearIntFunctorSingleFunctors, mapBifunctorShift₂Iso_hom_naturality₂_assoc, HomComplex.Cochain.rightUnshift_neg, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app, mappingConeCompTriangle_mor₃, HomComplex.Cochain.shift_add, mappingCone.rotateHomotopyEquiv_comm₂_assoc, mapBifunctorShift₁Iso_hom_naturality₁_assoc, shiftShortComplexFunctorIso_add'_hom_app, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso, HomComplex.Cochain.leftShiftLinearEquiv_apply, HomComplex.Cochain.shift_neg, ι_mapBifunctorShift₂Iso_hom_f_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, HomComplex.Cocycle.equivHomShift'_symm_apply, mappingCone.inl_v_triangle_mor₃_f, XIsoOfEq_shift, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, HomComplex.Cochain.rightUnshift_comp, HomComplex.Cochain.rightUnshift_units_smul, mappingCone.inr_triangleδ, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, mappingConeCompHomotopyEquiv_comm₂_assoc, mappingConeCompHomotopyEquiv_hom_inv_id, HomComplex.Cochain.shift_zero, shiftFunctorZero_inv_app_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, HomComplex.Cochain.leftShift_comp, triangleOfDegreewiseSplit_obj₂, MappingConeCompHomotopyEquiv.hom_inv_id_assoc, homologyFunctor_shift, isKInjective_shift_iff, HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, HomComplex.Cochain.leftShift_rightShift, instAdditiveIntFunctorSingleFunctors, mappingConeCompHomotopyEquiv_comm₁, mappingCone.triangleMap_hom₂, mappingCone.rotateHomotopyEquiv_comm₂, homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.ProjectiveResolution.extMk_hom, mappingCone.triangleRotateShortComplex_X₂, HomComplex.Cochain.shift_smul, HomComplex.Cochain.leftShiftAddEquiv_apply, shiftShortComplexFunctor'_hom_app_τ₁, HomComplex.Cochain.rightShiftAddEquiv_apply, shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, HomComplex.Cochain.leftUnshift_v, mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, mappingCone.triangleRotateShortComplex_X₃, HomComplex.Cochain.rightShift_leftShift, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, instLinearHomologicalComplexIntUpShiftFunctor, HomComplex.Cochain.leftUnshift_smul, instIsKInjectiveObjIntShiftFunctor, mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, HomComplex.Cochain.shiftLinearMap_apply, mappingCone.triangleRotateShortComplex_X₁, shiftFunctor_map_f', HomComplex.Cochain.rightShift_zero, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, quasiIso_shift_iff, HomComplex.Cochain.rightUnshift_v, shiftShortComplexFunctor'_hom_app_τ₂, shiftFunctorAdd'_inv_app_f', mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f, shiftFunctorAdd'_eq, mapBifunctorShift₂Iso_hom_naturality₂, mappingCone.inl_v_triangle_mor₃_f_assoc, mappingConeCompTriangle_mor₁, mappingCone.inr_triangleδ_assoc, HomComplex.Cochain.leftShift_zero, triangleOfDegreewiseSplit_mor₂, mappingCone.inr_f_triangle_mor₃_f, mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, triangleOfDegreewiseSplit_obj₃, mappingCone.triangle_mor₂, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomComplex.Cocycle.leftUnshift_coe, MappingConeCompHomotopyEquiv.hom_inv_id, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, quasiIsoAt_shift_iff, HomComplex.Cocycle.equivHomShift_symm_apply, instIsKProjectiveObjIntShiftFunctor, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, HomComplex.Cochain.rightShift_smul, homOfDegreewiseSplit_f, shiftFunctorAdd_inv_app_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, shiftShortComplexFunctorIso_hom_app_τ₁, shiftShortComplexFunctorIso_inv_app_τ₂, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app, mappingConeCompTriangle_obj₃, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f, HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, HomComplex.Cochain.shift_units_smul, shiftFunctorAdd_eq, HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, ι_mapBifunctorShift₂Iso_hom_f, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, mappingConeCompHomotopyEquiv_comm₂, HomComplex.CohomologyClass.toHom_bijective, HomComplex.Cochain.leftUnshift_add, mappingCone.rotateHomotopyEquiv_comm₃_assoc, HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic, HomComplex.Cochain.rightShift_units_smul, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, HomComplex.Cochain.rightUnshift_smul, HomComplex.Cocycle.equivHomShift'_apply, instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, HomComplex.Cochain.δ_shift, shiftShortComplexFunctor'_hom_app_τ₃, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app, CategoryTheory.InjectiveResolution.extMk_hom, HomComplex.Cochain.δ_rightUnshift, HomComplex.Cochain.leftUnshift_units_smul, HomComplex.Cochain.rightShiftLinearEquiv_apply, mappingCone.trianglehMapOfHomotopy_hom₃, HomComplex.Cocycle.shift_coe, isStrictlyLE_shift, mappingCone.trianglehMapOfHomotopy_hom₁, HomComplex.Cochain.δ_rightShift, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, HomComplex.Cochain.leftShift_v, HomComplex.Cochain.rightUnshift_add, homologySequenceδ_quotient_mapTriangle_obj, mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, HomotopyCategory.homologyFunctor_shiftMap_assoc, HomologicalComplex₂.totalShift₂Iso_hom_naturality, shiftFunctor_obj_X', HomComplex.Cochain.shift_v, shiftFunctorZero_hom_app_f, triangleOfDegreewiseSplit_mor₃, shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, HomComplex.Cochain.shiftAddHom_apply, mappingCone.trianglehMapOfHomotopy_hom₂, HomComplex.Cochain.δ_leftUnshift, shiftFunctorAdd'_hom_app_f', HomComplex.Cochain.leftShift_add, HomComplex.Cochain.leftShift_comp_zero_cochain, mappingCone.triangleMapOfHomotopy_comm₃_assoc, shiftEval_hom_app, mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, instHasMapBifunctorObjIntShiftFunctor_1, HomComplex.Cocycle.equivHomShift_comp, mappingCone.triangleRotateShortComplex_g, shiftFunctor_obj_d', instHasMapBifunctorObjIntShiftFunctor, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, ι_mapBifunctorShift₁Iso_hom_f_assoc, triangleOfDegreewiseSplit_mor₁, mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, HomComplex.Cochain.leftShift_units_smul, HomotopyCategory.homologyShiftIso_hom_app, shiftFunctorAdd_hom_app_f, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, shiftShortComplexFunctor'_inv_app_τ₃, mappingCone.inr_f_triangle_mor₃_f_assoc, mappingCone.triangleMap_hom₁, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, shiftFunctorComm_hom_app_f, mappingConeHomOfDegreewiseSplitIso_inv_f, HomComplex.Cochain.leftShiftAddEquiv_symm_apply, HomComplex.Cochain.rightShift_neg, HomologicalComplex₂.totalShift₁Iso_hom_naturality, mappingConeCompTriangle_mor₃_naturality_assoc, mappingCone.triangleMapOfHomotopy_comm₃, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, shiftShortComplexFunctor'_inv_app_τ₂, HomComplex.Cocycle.equivHomShift_symm_precomp, CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f, shiftEval_inv_app, mapBifunctorShift₁Iso_hom_naturality₁, HomComplex.Cocycle.rightShiftAddEquiv_apply, HomComplex.Cocycle.equivHomShift_comp_shift, HomotopyCategory.homologyFunctor_shiftMap, HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, shiftShortComplexFunctor'_inv_app_τ₁, shiftShortComplexFunctorIso_zero_add_hom_app, isKProjective_shift_iff, mappingCone.triangle_obj₂, mappingCone.triangleMap_hom₃, shiftShortComplexFunctorIso_inv_app_τ₃, mappingConeCompTriangle_mor₂, HomComplex.Cochain.rightShift_v, HomComplex.Cochain.rightUnshift_zero, mappingConeCompTriangleh_comm₁, HomComplex.Cocycle.leftShift_coe, HomComplex.Cochain.shift_v', DerivedCategory.mem_distTriang_iff, CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex, HomComplex.Cochain.rightShift_add, ShiftSequence.shiftIso_inv_app, CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex, isGE_shift, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app, mappingCone.triangleRotateShortComplex_f, HomComplex.Cocycle.rightUnshift_coe, mappingCone.rotateHomotopyEquiv_comm₃, HomComplex.Cochain.δ_leftShift, HomComplex.CohomologyClass.toHom_mk, HomComplex.Cocycle.leftShiftAddEquiv_apply, mappingConeHomOfDegreewiseSplitIso_hom_f, HomComplex.Cochain.leftShift_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, HomComplex.Cocycle.equivHomShift_apply, shiftShortComplexFunctorIso_inv_app_τ₁, HomComplex.Cochain.leftUnshift_neg, isLE_shift, mappingCone.triangle_obj₁, HomComplex.Cocycle.rightShift_coe, mappingConeCompHomotopyEquiv_hom_inv_id_assoc, HomComplex.Cochain.leftUnshift_zero, mappingCone.triangle_obj₃, HomComplex.CohomologyClass.homAddEquiv_apply, mappingConeCompTriangle_obj₁, instAdditiveHomologicalComplexIntUpShiftFunctor, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, ι_mapBifunctorShift₁Iso_hom_f, ShiftSequence.shiftIso_hom_app, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, mappingCone.map_δ
shiftEval 📖	CompOp	2 math math: shiftEval_hom_app, shiftEval_inv_app
shiftFunctor 📖	CompOp	40 math math: shiftShortComplexFunctorIso_hom_app_τ₂, shiftShortComplexFunctorIso_hom_app_τ₃, shiftShortComplexFunctorIso_add'_hom_app, ι_mapBifunctorShift₂Iso_hom_f_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, mappingCone.inl_v_triangle_mor₃_f, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, shiftFunctor_obj_X, HomComplex.Cochain.leftUnshift_v, HomComplex.Cochain.rightUnshift_v, shiftFunctorAdd'_inv_app_f, mappingCone.inl_v_triangle_mor₃_f_assoc, instLinearIntShiftFunctor, shiftFunctorZero'_hom_app_f, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, instAdditiveIntShiftFunctor, shiftFunctor_map_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, shiftShortComplexFunctorIso_hom_app_τ₁, shiftShortComplexFunctorIso_inv_app_τ₂, ι_mapBifunctorShift₂Iso_hom_f, shiftFunctorZero'_inv_app_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, HomComplex.Cochain.leftShift_v, HomComplex.Cochain.shift_v, ι_mapBifunctorShift₁Iso_hom_f_assoc, shiftFunctorAdd'_hom_app_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, shiftShortComplexFunctorIso_zero_add_hom_app, shiftShortComplexFunctorIso_inv_app_τ₃, HomComplex.Cochain.rightShift_v, ShiftSequence.shiftIso_inv_app, liftCycles_shift_homologyπ_assoc, shiftShortComplexFunctorIso_inv_app_τ₁, shiftFunctor_obj_d, liftCycles_shift_homologyπ, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, ι_mapBifunctorShift₁Iso_hom_f, ShiftSequence.shiftIso_hom_app
shiftFunctorAdd' 📖	CompOp	4 math math: shiftFunctorAdd'_eq, shiftFunctorAdd'_inv_app_f, shiftFunctorAdd_eq, shiftFunctorAdd'_hom_app_f
shiftFunctorObjXIso 📖	CompOp	21 math math: ι_mapBifunctorShift₂Iso_hom_f_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, mappingCone.inl_v_triangle_mor₃_f, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, HomComplex.Cochain.leftUnshift_v, HomComplex.Cochain.rightUnshift_v, mappingCone.inl_v_triangle_mor₃_f_assoc, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, ι_mapBifunctorShift₂Iso_hom_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, HomComplex.Cochain.leftShift_v, HomComplex.Cochain.shift_v, ι_mapBifunctorShift₁Iso_hom_f_assoc, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, HomComplex.Cochain.rightShift_v, liftCycles_shift_homologyπ_assoc, liftCycles_shift_homologyπ, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, ι_mapBifunctorShift₁Iso_hom_f
shiftFunctorZero' 📖	CompOp	3 math math: shiftFunctorZero_eq, shiftFunctorZero'_hom_app_f, shiftFunctorZero'_inv_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
XIsoOfEq_shift 📖	mathematical	—	HomologicalComplex.XIsoOfEq 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	—	AddRightCancelSemigroup.toIsRightCancelAdd
instAdditiveHomologicalComplexIntUpShiftFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive 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.instPreadditive CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd instAdditiveIntShiftFunctor
instAdditiveIntShiftFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive 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 HomologicalComplex.instPreadditive shiftFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd
instLinearHomologicalComplexIntUpShiftFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring 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.instPreadditive HomologicalComplex.instLinear CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd
instLinearIntShiftFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring 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 HomologicalComplex.instPreadditive HomologicalComplex.instLinear shiftFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftEval_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 CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex.eval CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftEval HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftEval_inv_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 HomologicalComplex.eval CategoryTheory.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftEval HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorAdd'_eq 📖	mathematical	—	CategoryTheory.shiftFunctorAdd' 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 Int.instAddMonoid instHasShiftInt shiftFunctorAdd'	—	CategoryTheory.Iso.ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.NatTrans.ext' HomologicalComplex.hom_ext shiftFunctorAdd'_hom_app_f'
shiftFunctorAdd'_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory shiftFunctor CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctorAdd' HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorAdd'_hom_app_f' 📖	mathematical	—	HomologicalComplex.Hom.f 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.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorAdd' HomologicalComplex.X CategoryTheory.Discrete.as HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd shiftFunctorAdd_hom_app_f
shiftFunctorAdd'_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.Functor.comp shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctorAdd' HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorAdd'_inv_app_f' 📖	mathematical	—	HomologicalComplex.Hom.f 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.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorAdd' CategoryTheory.Iso.hom HomologicalComplex.X CategoryTheory.Discrete.as HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd shiftFunctorAdd_inv_app_f
shiftFunctorAdd_eq 📖	mathematical	—	CategoryTheory.shiftFunctorAdd 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 Int.instAddMonoid instHasShiftInt shiftFunctorAdd'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd shiftFunctorAdd'_eq
shiftFunctorAdd_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f 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 AddMonoid.toAddSemigroup CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorAdd HomologicalComplex.X CategoryTheory.Discrete.as HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorAdd_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f 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.Functor.comp CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt AddMonoid.toAddSemigroup CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorAdd CategoryTheory.Iso.hom HomologicalComplex.X CategoryTheory.Discrete.as HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorComm_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f 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.Functor.comp CategoryTheory.shiftFunctor AddCommMonoid.toAddMonoid Int.instAddCommMonoid instHasShiftInt CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorComm HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctorComm_eq shiftFunctorAdd'_inv_app_f' shiftFunctorAdd'_hom_app_f' CategoryTheory.eqToHom_trans
shiftFunctorZero'_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory shiftFunctor CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctorZero' HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorZero'_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.Functor.id shiftFunctor CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category shiftFunctorZero' HomologicalComplex.X HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorZero_eq 📖	mathematical	—	CategoryTheory.shiftFunctorZero 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 Int.instAddMonoid instHasShiftInt shiftFunctorZero'	—	CategoryTheory.Iso.ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.NatTrans.ext' HomologicalComplex.hom_ext shiftFunctorZero_hom_app_f shiftFunctorZero'_hom_app_f
shiftFunctorZero_hom_app_f 📖	mathematical	—	HomologicalComplex.Hom.f 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 AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorZero HomologicalComplex.X CategoryTheory.Discrete.as HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctorZero_inv_app_f 📖	mathematical	—	HomologicalComplex.Hom.f 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.Functor.id CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.shiftFunctorZero CategoryTheory.Iso.hom HomologicalComplex.X CategoryTheory.Discrete.as HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctor_map_f 📖	mathematical	—	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.X Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow HomologicalComplex.d CategoryTheory.Functor.map CochainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd shiftFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctor_map_f' 📖	mathematical	—	HomologicalComplex.Hom.f 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.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctor_obj_X 📖	mathematical	—	HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd shiftFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctor_obj_X' 📖	mathematical	—	HomologicalComplex.X 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	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctor_obj_d 📖	mathematical	—	HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory AddRightCancelSemigroup.toIsRightCancelAdd shiftFunctor 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	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctor_obj_d' 📖	mathematical	—	HomologicalComplex.d 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 Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Discrete.as Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd

Homotopy

Definitions

Name	Category	Theorems
shift 📖	CompOp	—

HomotopyCategory

Definitions

Name	Category	Theorems
commShiftQuotient 📖	CompOp	8 math math: spectralObjectMappingCone_δ'_app, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, homologyFunctor_shiftMap_assoc, homologyShiftIso_hom_app, homologyFunctor_shiftMap, instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors
hasShift 📖	CompOp	32 math math: spectralObjectMappingCone_δ'_app, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CochainComplex.mappingCone.homologySequenceδ_triangleh, instIsHomologicalIntUpHomologyFunctor, instAdditiveIntUpShiftFunctor, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, mappingCone_triangleh_distinguished, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, instLinearIntUpShiftFunctor, Pretriangulated.distinguished_cocone_triangle, Pretriangulated.contractible_distinguished, instIsTriangulatedIntUpSubcategoryAcyclic, instIsTriangulatedIntUp, instIsTriangulatedIntUpMapHomotopyCategory, quasiIso_eq_subcategoryAcyclic_W, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, homologyFunctor_shiftMap_assoc, distinguished_iff_iso_trianglehOfDegreewiseSplit, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, spectralObjectMappingCone_ω₁, homologyShiftIso_hom_app, DerivedCategory.Qh_obj_singleFunctors_obj, Pretriangulated.rotate_distinguished_triangle, homologyFunctor_shiftMap, CochainComplex.mappingConeCompTriangleh_comm₁, mappingConeCompTriangleh_distinguished, instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic
instCommShiftIntUpMapHomotopyCategory 📖	CompOp	3 math math: CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedIntUpMapHomotopyCategory, instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveIntUpShiftFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory instPreadditive CategoryTheory.shiftFunctor Int.instAddMonoid hasShift	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.additive_of_iso CategoryTheory.Functor.instAdditiveComp CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor instAdditiveHomologicalComplexQuotient CategoryTheory.Functor.additive_of_full_essSurj_comp instFullHomologicalComplexQuotient instEssSurjHomologicalComplexQuotient
instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors 📖	mathematical	—	CategoryTheory.NatTrans.CommShift HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomotopyCategory HomologicalComplex.instCategory instCategoryHomotopyCategory CategoryTheory.Functor.comp quotient CategoryTheory.Functor.mapHomotopyCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapHomotopyCategoryFactors Int.instAddMonoid CochainComplex.instHasShiftInt hasShift CategoryTheory.Functor.CommShift.comp commShiftQuotient instCommShiftIntUpMapHomotopyCategory CategoryTheory.Functor.commShiftMapCochainComplex	—	CategoryTheory.Quotient.liftCommShift_compatibility AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic
instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic 📖	mathematical	—	HomRel.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 homotopic Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd
instLinearIntUpShiftFunctor 📖	mathematical	—	CategoryTheory.Functor.Linear Ring.toSemiring HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory instPreadditive instLinear CategoryTheory.shiftFunctor Int.instAddMonoid hasShift	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_surjective instFullHomologicalComplexQuotient CategoryTheory.NatIso.naturality_1 CategoryTheory.Functor.map_smul instLinearHomologicalComplexQuotient CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor CategoryTheory.Linear.smul_comp CategoryTheory.Functor.commShiftIso_hom_naturality CategoryTheory.Linear.comp_smul CategoryTheory.Iso.inv_hom_id_app_assoc

---

← Back to Index