HomComplexShift

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

Statistics

Metric	Count
Definitions leftShift, leftShiftAddEquiv, leftShiftLinearEquiv, leftUnshift, rightShift, rightShiftAddEquiv, rightShiftLinearEquiv, rightUnshift, shift, shiftAddHom, shiftLinearMap, equivHomShift, equivHomShift', leftShift, leftShiftAddEquiv, leftUnshift, rightShift, rightShiftAddEquiv, rightUnshift, shift	20
Theorems leftShiftAddEquiv_apply, leftShiftAddEquiv_symm_apply, leftShiftLinearEquiv_apply, leftShiftLinearEquiv_symm_apply, leftShift_add, leftShift_comp, leftShift_comp_zero_cochain, leftShift_leftUnshift, leftShift_neg, leftShift_rightShift, leftShift_rightShift_eq_negOnePow_rightShift_leftShift, leftShift_smul, leftShift_units_smul, leftShift_v, leftShift_zero, leftUnshift_add, leftUnshift_leftShift, leftUnshift_neg, leftUnshift_smul, leftUnshift_units_smul, leftUnshift_v, leftUnshift_zero, rightShiftAddEquiv_apply, rightShiftAddEquiv_symm_apply, rightShiftLinearEquiv_apply, rightShiftLinearEquiv_symm_apply, rightShift_add, rightShift_leftShift, rightShift_neg, rightShift_rightUnshift, rightShift_smul, rightShift_units_smul, rightShift_v, rightShift_zero, rightUnshift_add, rightUnshift_comp, rightUnshift_neg, rightUnshift_rightShift, rightUnshift_smul, rightUnshift_units_smul, rightUnshift_v, rightUnshift_zero, shiftAddHom_apply, shiftLinearMap_apply, shift_add, shift_neg, shift_smul, shift_units_smul, shift_v, shift_v', shift_zero, δ_leftShift, δ_leftUnshift, δ_rightShift, δ_rightUnshift, δ_shift, equivHomShift'_apply, equivHomShift'_symm_apply, equivHomShift_apply, equivHomShift_comp, equivHomShift_comp_shift, equivHomShift_symm_apply, equivHomShift_symm_postcomp, equivHomShift_symm_precomp, leftShiftAddEquiv_apply, leftShiftAddEquiv_symm_apply, leftShift_coe, leftUnshift_coe, rightShiftAddEquiv_apply, rightShiftAddEquiv_symm_apply, rightShift_coe, rightUnshift_coe, shift_coe	73
Total	93

CochainComplex.HomComplex.Cochain

Definitions

Name	Category	Theorems
leftShift 📖	CompOp	17 math math: leftShift_smul, leftShiftLinearEquiv_apply, leftShift_comp, leftShift_leftUnshift, leftShift_rightShift_eq_negOnePow_rightShift_leftShift, leftShift_rightShift, leftShiftAddEquiv_apply, rightShift_leftShift, leftShift_zero, leftShift_v, leftShift_add, leftShift_comp_zero_cochain, leftShift_units_smul, leftUnshift_leftShift, CochainComplex.HomComplex.Cocycle.leftShift_coe, δ_leftShift, leftShift_neg
leftShiftAddEquiv 📖	CompOp	2 math math: leftShiftAddEquiv_apply, leftShiftAddEquiv_symm_apply
leftShiftLinearEquiv 📖	CompOp	2 math math: leftShiftLinearEquiv_apply, leftShiftLinearEquiv_symm_apply
leftUnshift 📖	CompOp	12 math math: leftShift_leftUnshift, leftUnshift_v, leftUnshift_smul, CochainComplex.HomComplex.Cocycle.leftUnshift_coe, leftShiftLinearEquiv_symm_apply, leftUnshift_add, leftUnshift_units_smul, δ_leftUnshift, leftUnshift_leftShift, leftShiftAddEquiv_symm_apply, leftUnshift_neg, leftUnshift_zero
rightShift 📖	CompOp	15 math math: leftShift_rightShift_eq_negOnePow_rightShift_leftShift, leftShift_rightShift, rightShiftAddEquiv_apply, rightShift_leftShift, rightShift_zero, rightShift_rightUnshift, rightShift_smul, rightShift_units_smul, rightShiftLinearEquiv_apply, δ_rightShift, rightUnshift_rightShift, rightShift_neg, rightShift_v, rightShift_add, CochainComplex.HomComplex.Cocycle.rightShift_coe
rightShiftAddEquiv 📖	CompOp	2 math math: rightShiftAddEquiv_symm_apply, rightShiftAddEquiv_apply
rightShiftLinearEquiv 📖	CompOp	2 math math: rightShiftLinearEquiv_apply, rightShiftLinearEquiv_symm_apply
rightUnshift 📖	CompOp	13 math math: rightShiftAddEquiv_symm_apply, rightUnshift_neg, rightUnshift_comp, rightUnshift_units_smul, rightUnshift_v, rightShift_rightUnshift, rightUnshift_smul, δ_rightUnshift, rightUnshift_add, rightUnshift_rightShift, rightShiftLinearEquiv_symm_apply, rightUnshift_zero, CochainComplex.HomComplex.Cocycle.rightUnshift_coe
shift 📖	CompOp	13 math math: shift_add, shift_neg, shift_zero, leftShift_rightShift, shift_smul, rightShift_leftShift, shiftLinearMap_apply, shift_units_smul, δ_shift, CochainComplex.HomComplex.Cocycle.shift_coe, shift_v, shiftAddHom_apply, shift_v'
shiftAddHom 📖	CompOp	1 math math: shiftAddHom_apply
shiftLinearMap 📖	CompOp	1 math math: shiftLinearMap_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leftShiftAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain EquivLike.toFunLike AddEquiv.instEquivLike leftShiftAddEquiv leftShift	—	AddRightCancelSemigroup.toIsRightCancelAdd
leftShiftAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm leftShiftAddEquiv leftUnshift	—	AddRightCancelSemigroup.toIsRightCancelAdd
leftShiftLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.instModuleCochain EquivLike.toFunLike LinearEquiv.instEquivLike leftShiftLinearEquiv leftShift	—	RingHomInvPair.ids AddRightCancelSemigroup.toIsRightCancelAdd
leftShiftLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.instModuleCochain EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm leftShiftLinearEquiv leftUnshift	—	RingHomInvPair.ids AddRightCancelSemigroup.toIsRightCancelAdd
leftShift_add 📖	mathematical	—	leftShift CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	ext AddRightCancelSemigroup.toIsRightCancelAdd leftShift_v CategoryTheory.Preadditive.comp_add smul_add
leftShift_comp 📖	mathematical	—	leftShift comp Units Int.instMonoid CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow	—	ext AddRightCancelSemigroup.toIsRightCancelAdd leftShift_v Int.negOnePow_add comp_v CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc smul_smul add_comm mul_add Distrib.leftDistribClass
leftShift_comp_zero_cochain 📖	mathematical	—	leftShift comp add_zero AddMonoid.toAddZeroClass Int.instAddMonoid CategoryTheory.Functor.obj 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.shiftFunctor CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero leftShift_comp MulZeroClass.mul_zero Int.negOnePow_zero one_smul
leftShift_leftUnshift 📖	mathematical	—	leftShift leftUnshift	—	AddRightCancelSemigroup.toIsRightCancelAdd ext leftShift_v leftUnshift_v CategoryTheory.Linear.comp_units_smul smul_smul CategoryTheory.Iso.hom_inv_id_assoc Int.units_mul_self one_smul
leftShift_neg 📖	mathematical	—	leftShift CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd map_neg AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
leftShift_rightShift 📖	mathematical	—	leftShift CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt rightShift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow shift	—	ext AddRightCancelSemigroup.toIsRightCancelAdd leftShift_v rightShift_v shift_v' CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
leftShift_rightShift_eq_negOnePow_rightShift_leftShift 📖	mathematical	—	leftShift CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt rightShift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd leftShift_rightShift rightShift_leftShift smul_smul add_comm mul_add Distrib.leftDistribClass Int.negOnePow_add Int.negOnePow_mul_self mul_assoc Int.units_mul_self one_mul
leftShift_smul 📖	mathematical	—	leftShift CochainComplex.HomComplex.Cochain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	ext AddRightCancelSemigroup.toIsRightCancelAdd leftShift_v CategoryTheory.Linear.comp_smul SMulCommClass.smul_comm Units.smulCommClass_right AddGroup.int_smulCommClass'
leftShift_units_smul 📖	mathematical	—	leftShift Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	leftShift_smul
leftShift_v 📖	mathematical	—	v CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt leftShift Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CochainComplex.shiftFunctor Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
leftShift_zero 📖	mathematical	—	leftShift CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
leftUnshift_add 📖	mathematical	—	leftUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_add AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
leftUnshift_leftShift 📖	mathematical	—	leftUnshift leftShift	—	ext AddRightCancelSemigroup.toIsRightCancelAdd leftUnshift_v leftShift_v CategoryTheory.Linear.comp_units_smul CategoryTheory.Iso.inv_hom_id_assoc smul_smul Int.units_mul_self one_smul
leftUnshift_neg 📖	mathematical	—	leftUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_neg AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
leftUnshift_smul 📖	mathematical	—	leftUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_smul RingHomInvPair.ids SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
leftUnshift_units_smul 📖	mathematical	—	leftUnshift Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd leftUnshift_smul
leftUnshift_v 📖	mathematical	—	v leftUnshift Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct 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 Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CochainComplex.shiftFunctor CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd
leftUnshift_zero 📖	mathematical	—	leftUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
rightShiftAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain EquivLike.toFunLike AddEquiv.instEquivLike rightShiftAddEquiv rightShift	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightShiftAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm rightShiftAddEquiv rightUnshift	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightShiftLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.instModuleCochain EquivLike.toFunLike LinearEquiv.instEquivLike rightShiftLinearEquiv rightShift	—	RingHomInvPair.ids AddRightCancelSemigroup.toIsRightCancelAdd
rightShiftLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.instModuleCochain EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm rightShiftLinearEquiv rightUnshift	—	RingHomInvPair.ids AddRightCancelSemigroup.toIsRightCancelAdd
rightShift_add 📖	mathematical	—	rightShift CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	ext AddRightCancelSemigroup.toIsRightCancelAdd rightShift_v CategoryTheory.Preadditive.add_comp
rightShift_leftShift 📖	mathematical	—	rightShift CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt leftShift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow shift	—	ext AddRightCancelSemigroup.toIsRightCancelAdd rightShift_v leftShift_v shift_v' CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
rightShift_neg 📖	mathematical	—	rightShift CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd map_neg AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
rightShift_rightUnshift 📖	mathematical	—	rightShift rightUnshift	—	AddRightCancelSemigroup.toIsRightCancelAdd ext rightShift_v rightUnshift_v CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
rightShift_smul 📖	mathematical	—	rightShift CochainComplex.HomComplex.Cochain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	ext AddRightCancelSemigroup.toIsRightCancelAdd rightShift_v CategoryTheory.Linear.smul_comp
rightShift_units_smul 📖	mathematical	—	rightShift Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	rightShift_smul
rightShift_v 📖	mathematical	—	v CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt rightShift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CochainComplex.shiftFunctor CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightShift_zero 📖	mathematical	—	rightShift CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
rightUnshift_add 📖	mathematical	—	rightUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_add AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
rightUnshift_comp 📖	mathematical	—	rightUnshift comp CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd ext rightUnshift_v comp_v CategoryTheory.Category.assoc
rightUnshift_neg 📖	mathematical	—	rightUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_neg AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
rightUnshift_rightShift 📖	mathematical	—	rightUnshift rightShift	—	ext AddRightCancelSemigroup.toIsRightCancelAdd rightUnshift_v rightShift_v CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
rightUnshift_smul 📖	mathematical	—	rightUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_smul RingHomInvPair.ids SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
rightUnshift_units_smul 📖	mathematical	—	rightUnshift Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd rightUnshift_smul
rightUnshift_v 📖	mathematical	—	v rightUnshift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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 CochainComplex.instHasShiftInt CategoryTheory.Iso.hom CochainComplex.shiftFunctor CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightUnshift_zero 📖	mathematical	—	rightUnshift CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
shiftAddHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain AddMonoidHom.instFunLike shiftAddHom shift	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.instModuleCochain LinearMap.instFunLike shiftLinearMap shift	—	AddRightCancelSemigroup.toIsRightCancelAdd
shift_add 📖	mathematical	—	shift CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	ext AddRightCancelSemigroup.toIsRightCancelAdd shift_v'
shift_neg 📖	mathematical	—	shift CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd map_neg AddMonoidHom.instAddMonoidHomClass
shift_smul 📖	mathematical	—	shift CochainComplex.HomComplex.Cochain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	ext AddRightCancelSemigroup.toIsRightCancelAdd shift_v'
shift_units_smul 📖	mathematical	—	shift Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	ext AddRightCancelSemigroup.toIsRightCancelAdd shift_v'
shift_v 📖	mathematical	—	v CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt shift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CochainComplex.shiftFunctor CategoryTheory.Iso.hom CochainComplex.shiftFunctorObjXIso CategoryTheory.Iso.inv	—	AddRightCancelSemigroup.toIsRightCancelAdd
shift_v' 📖	mathematical	—	v CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt shift	—	AddRightCancelSemigroup.toIsRightCancelAdd shift_v CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
shift_zero 📖	mathematical	—	shift CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
δ_leftShift 📖	mathematical	—	CochainComplex.HomComplex.δ CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt leftShift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd ext leftShift_v CochainComplex.HomComplex.δ_v CategoryTheory.Category.id_comp CategoryTheory.Linear.units_smul_comp CategoryTheory.Linear.comp_units_smul smul_smul smul_add add_comm mul_add Distrib.leftDistribClass mul_one Int.negOnePow_add Int.units_mul_self one_mul Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing CochainComplex.HomComplex.δ_shape leftShift_zero smul_zero
δ_leftUnshift 📖	mathematical	—	CochainComplex.HomComplex.δ leftUnshift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.surjective leftUnshift_leftShift δ_leftShift leftUnshift_units_smul smul_smul Int.units_mul_self one_smul
δ_rightShift 📖	mathematical	—	CochainComplex.HomComplex.δ CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt rightShift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd ext rightShift_v CochainComplex.HomComplex.δ_v CategoryTheory.Linear.comp_units_smul CategoryTheory.Category.assoc HomologicalComplex.XIsoOfEq_inv_comp_d CategoryTheory.Preadditive.add_comp HomologicalComplex.d_comp_XIsoOfEq_inv CategoryTheory.Linear.units_smul_comp smul_add smul_smul AddLeftCancelSemigroup.toIsLeftCancelAdd add_comm Int.negOnePow_add Int.units_mul_self one_mul CochainComplex.HomComplex.δ_shape rightShift_zero smul_zero
δ_rightUnshift 📖	mathematical	—	CochainComplex.HomComplex.δ rightUnshift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.surjective rightUnshift_rightShift δ_rightShift rightUnshift_units_smul smul_smul Int.units_mul_self one_smul
δ_shift 📖	mathematical	—	CochainComplex.HomComplex.δ CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt shift Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.δ_v shift_v' CategoryTheory.Linear.comp_units_smul CategoryTheory.Linear.units_smul_comp smul_add AddLeftCancelSemigroup.toIsLeftCancelAdd SMulCommClass.smul_comm Units.smulCommClass_left AddGroup.int_smulCommClass CochainComplex.HomComplex.δ_shape shift_zero smul_zero

CochainComplex.HomComplex.Cocycle

Definitions

Name	Category	Theorems
equivHomShift 📖	CompOp	13 math math: equivHomShift_symm_postcomp, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, CategoryTheory.ProjectiveResolution.extMk_hom, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, equivHomShift_symm_apply, CategoryTheory.InjectiveResolution.extMk_hom, equivHomShift_comp, equivHomShift_symm_precomp, equivHomShift_comp_shift, CochainComplex.HomComplex.CohomologyClass.toHom_mk, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, equivHomShift_apply
equivHomShift' 📖	CompOp	2 math math: equivHomShift'_symm_apply, equivHomShift'_apply
leftShift 📖	CompOp	3 math math: equivHomShift'_symm_apply, leftShift_coe, leftShiftAddEquiv_apply
leftShiftAddEquiv 📖	CompOp	2 math math: leftShiftAddEquiv_symm_apply, leftShiftAddEquiv_apply
leftUnshift 📖	CompOp	3 math math: leftShiftAddEquiv_symm_apply, leftUnshift_coe, equivHomShift'_apply
rightShift 📖	CompOp	3 math math: equivHomShift_symm_apply, rightShiftAddEquiv_apply, rightShift_coe
rightShiftAddEquiv 📖	CompOp	2 math math: rightShiftAddEquiv_symm_apply, rightShiftAddEquiv_apply
rightUnshift 📖	CompOp	3 math math: rightShiftAddEquiv_symm_apply, rightUnshift_coe, equivHomShift_apply
shift 📖	CompOp	1 math math: shift_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivHomShift'_apply 📖	mathematical	—	DFunLike.coe AddEquiv Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.HomComplex.Cocycle HomologicalComplex.instAddHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike equivHomShift' leftUnshift ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHomShift'_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm equivHomShift' homOf leftShift	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHomShift_apply 📖	mathematical	—	DFunLike.coe AddEquiv Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.HomComplex.Cocycle HomologicalComplex.instAddHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike equivHomShift rightUnshift AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHomShift_comp 📖	mathematical	—	DFunLike.coe AddEquiv Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.HomComplex.Cocycle HomologicalComplex.instAddHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike equivHomShift CategoryTheory.CategoryStruct.comp precomp	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext add_zero zero_add CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.ofHom_comp CochainComplex.HomComplex.Cochain.rightUnshift_v CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v CategoryTheory.Category.assoc CochainComplex.HomComplex.Cochain.zero_cochain_comp_v
equivHomShift_comp_shift 📖	mathematical	—	DFunLike.coe AddEquiv Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.HomComplex.Cocycle HomologicalComplex.instAddHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike equivHomShift CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map postcomp	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.Cochain.ext zero_add add_zero CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.ofHom_comp CochainComplex.HomComplex.Cochain.rightUnshift_v CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v CategoryTheory.Category.comp_id
equivHomShift_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm equivHomShift homOf rightShift AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHomShift_symm_postcomp 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm equivHomShift postcomp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.injective AddEquiv.apply_symm_apply equivHomShift_comp_shift
equivHomShift_symm_precomp 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm equivHomShift precomp CategoryTheory.CategoryStruct.comp	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.injective AddEquiv.apply_symm_apply equivHomShift_comp
leftShiftAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike leftShiftAddEquiv leftShift	—	AddRightCancelSemigroup.toIsRightCancelAdd
leftShiftAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm leftShiftAddEquiv leftUnshift	—	AddRightCancelSemigroup.toIsRightCancelAdd
leftShift_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle leftShift CochainComplex.HomComplex.Cochain.leftShift	—	AddRightCancelSemigroup.toIsRightCancelAdd
leftUnshift_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle leftUnshift CochainComplex.HomComplex.Cochain.leftUnshift CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightShiftAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike rightShiftAddEquiv rightShift	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightShiftAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm rightShiftAddEquiv rightUnshift	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightShift_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle rightShift CochainComplex.HomComplex.Cochain.rightShift	—	AddRightCancelSemigroup.toIsRightCancelAdd
rightUnshift_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle rightUnshift CochainComplex.HomComplex.Cochain.rightUnshift CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd
shift_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain CategoryTheory.Functor.obj 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.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle shift CochainComplex.HomComplex.Cochain.shift	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index