TotalComplexShift

📁 Source: Mathlib/Algebra/Homology/TotalComplexShift.lean

Statistics

Metric	Count
Definitions shiftFunctor₁, shiftFunctor₁XXIso, shiftFunctor₁₂CommIso, shiftFunctor₂, shiftFunctor₂XXIso, totalShift₁Iso, totalShift₁XIso, totalShift₂Iso, totalShift₂XIso	9
Theorems D₁_totalShift₁XIso_hom, D₁_totalShift₁XIso_hom_assoc, D₁_totalShift₂XIso_hom, D₁_totalShift₂XIso_hom_assoc, D₂_totalShift₁XIso_hom, D₂_totalShift₁XIso_hom_assoc, D₂_totalShift₂XIso_hom, D₂_totalShift₂XIso_hom_assoc, instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, instHasTotalIntObjUpShiftFunctor₁, instHasTotalIntObjUpShiftFunctor₂, shiftFunctor₁XXIso_refl, shiftFunctor₂XXIso_refl, totalShift₁Iso_hom_naturality, totalShift₁Iso_hom_naturality_assoc, totalShift₁Iso_hom_totalShift₂Iso_hom, totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, totalShift₁Iso_trans_totalShift₂Iso, totalShift₂Iso_hom_naturality, totalShift₂Iso_hom_naturality_assoc, ι_totalShift₁Iso_hom_f, ι_totalShift₁Iso_hom_f_assoc, ι_totalShift₁Iso_inv_f, ι_totalShift₁Iso_inv_f_assoc, ι_totalShift₂Iso_hom_f, ι_totalShift₂Iso_hom_f_assoc, ι_totalShift₂Iso_inv_f, ι_totalShift₂Iso_inv_f_assoc	29
Total	38

HomologicalComplex₂

Definitions

Name	Category	Theorems
shiftFunctor₁ 📖	CompOp	19 math math: D₂_totalShift₁XIso_hom_assoc, ι_totalShift₁Iso_hom_f_assoc, ι_totalShift₁Iso_inv_f, instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, totalShift₁Iso_hom_totalShift₂Iso_hom, shiftFunctor₁XXIso_refl, D₁_totalShift₁XIso_hom_assoc, instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, ι_totalShift₁Iso_inv_f_assoc, D₁_totalShift₁XIso_hom, D₂_totalShift₁XIso_hom, totalShift₁Iso_trans_totalShift₂Iso, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, totalShift₁Iso_hom_naturality_assoc, instHasTotalIntObjUpShiftFunctor₁, totalShift₁Iso_hom_naturality, ι_totalShift₁Iso_hom_f
shiftFunctor₁XXIso 📖	CompOp	5 math math: ι_totalShift₁Iso_hom_f_assoc, ι_totalShift₁Iso_inv_f, shiftFunctor₁XXIso_refl, ι_totalShift₁Iso_inv_f_assoc, ι_totalShift₁Iso_hom_f
shiftFunctor₁₂CommIso 📖	CompOp	3 math math: totalShift₁Iso_hom_totalShift₂Iso_hom, totalShift₁Iso_trans_totalShift₂Iso, totalShift₁Iso_hom_totalShift₂Iso_hom_assoc
shiftFunctor₂ 📖	CompOp	19 math math: totalShift₂Iso_hom_naturality_assoc, shiftFunctor₂XXIso_refl, D₂_totalShift₂XIso_hom_assoc, ι_totalShift₂Iso_inv_f_assoc, instHasTotalIntObjUpShiftFunctor₂, instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, totalShift₁Iso_hom_totalShift₂Iso_hom, D₁_totalShift₂XIso_hom_assoc, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, ι_totalShift₂Iso_hom_f_assoc, totalShift₁Iso_trans_totalShift₂Iso, ι_totalShift₂Iso_inv_f, totalShift₂Iso_hom_naturality, totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, ι_totalShift₂Iso_hom_f, D₁_totalShift₂XIso_hom, D₂_totalShift₂XIso_hom
shiftFunctor₂XXIso 📖	CompOp	5 math math: shiftFunctor₂XXIso_refl, ι_totalShift₂Iso_inv_f_assoc, ι_totalShift₂Iso_hom_f_assoc, ι_totalShift₂Iso_inv_f, ι_totalShift₂Iso_hom_f
totalShift₁Iso 📖	CompOp	9 math math: ι_totalShift₁Iso_hom_f_assoc, ι_totalShift₁Iso_inv_f, totalShift₁Iso_hom_totalShift₂Iso_hom, ι_totalShift₁Iso_inv_f_assoc, totalShift₁Iso_trans_totalShift₂Iso, totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, totalShift₁Iso_hom_naturality_assoc, totalShift₁Iso_hom_naturality, ι_totalShift₁Iso_hom_f
totalShift₁XIso 📖	CompOp	4 math math: D₂_totalShift₁XIso_hom_assoc, D₁_totalShift₁XIso_hom_assoc, D₁_totalShift₁XIso_hom, D₂_totalShift₁XIso_hom
totalShift₂Iso 📖	CompOp	9 math math: totalShift₂Iso_hom_naturality_assoc, ι_totalShift₂Iso_inv_f_assoc, totalShift₁Iso_hom_totalShift₂Iso_hom, ι_totalShift₂Iso_hom_f_assoc, totalShift₁Iso_trans_totalShift₂Iso, ι_totalShift₂Iso_inv_f, totalShift₂Iso_hom_naturality, totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, ι_totalShift₂Iso_hom_f
totalShift₂XIso 📖	CompOp	4 math math: D₂_totalShift₂XIso_hom_assoc, D₁_totalShift₂XIso_hom_assoc, D₁_totalShift₂XIso_hom, D₂_totalShift₂XIso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
D₁_totalShift₁XIso_hom 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ ComplexShape.π instHasTotalIntObjUpShiftFunctor₁ HomologicalComplex.X total D₁ CategoryTheory.Iso.hom totalShift₁XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ total.hom_ext ι_D₁_assoc CategoryTheory.Linear.comp_units_smul ι_totalDesc_assoc ι_D₁ d₁_eq one_smul CategoryTheory.Category.assoc ι_totalDesc CategoryTheory.Linear.units_smul_comp D₁_shape CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero smul_zero
D₁_totalShift₁XIso_hom_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ ComplexShape.π instHasTotalIntObjUpShiftFunctor₁ D₁ HomologicalComplex.X total CategoryTheory.Iso.hom totalShift₁XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₁_totalShift₁XIso_hom
D₁_totalShift₂XIso_hom 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₂ ComplexShape.π instHasTotalIntObjUpShiftFunctor₂ HomologicalComplex.X total D₁ CategoryTheory.Iso.hom totalShift₂XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ total.hom_ext ι_D₁_assoc CategoryTheory.Linear.comp_units_smul ι_totalDesc_assoc CategoryTheory.Linear.units_smul_comp ι_D₁ smul_smul d₁_eq one_smul CategoryTheory.Category.assoc ι_totalDesc Int.negOnePow_add 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.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add 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 D₁_shape CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero smul_zero
D₁_totalShift₂XIso_hom_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₂ ComplexShape.π instHasTotalIntObjUpShiftFunctor₂ D₁ HomologicalComplex.X total CategoryTheory.Iso.hom totalShift₂XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₁_totalShift₂XIso_hom
D₂_totalShift₁XIso_hom 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ ComplexShape.π instHasTotalIntObjUpShiftFunctor₁ HomologicalComplex.X total D₂ CategoryTheory.Iso.hom totalShift₁XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ total.hom_ext ι_D₂_assoc CategoryTheory.Linear.comp_units_smul ι_totalDesc_assoc ι_D₂ d₂_eq smul_smul CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc ι_totalDesc add_comm Int.negOnePow_add mul_assoc Int.units_mul_self one_mul D₂_shape CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero smul_zero
D₂_totalShift₁XIso_hom_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ ComplexShape.π instHasTotalIntObjUpShiftFunctor₁ D₂ HomologicalComplex.X total CategoryTheory.Iso.hom totalShift₁XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₂_totalShift₁XIso_hom
D₂_totalShift₂XIso_hom 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₂ ComplexShape.π instHasTotalIntObjUpShiftFunctor₂ HomologicalComplex.X total D₂ CategoryTheory.Iso.hom totalShift₂XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ total.hom_ext ι_D₂_assoc CategoryTheory.Linear.comp_units_smul ι_totalDesc_assoc CategoryTheory.Linear.units_smul_comp smul_smul ι_D₂ d₂_eq CategoryTheory.Category.assoc ι_totalDesc Int.negOnePow_add D₂_shape CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero smul_zero
D₂_totalShift₂XIso_hom_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₂ ComplexShape.π instHasTotalIntObjUpShiftFunctor₂ D₂ HomologicalComplex.X total CategoryTheory.Iso.hom totalShift₂XIso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₂_totalShift₂XIso_hom
instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.comp shiftFunctor₁ shiftFunctor₂	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ instHasTotalIntObjUpShiftFunctor₁
instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.comp shiftFunctor₂ shiftFunctor₁	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ instHasTotalIntObjUpShiftFunctor₂
instHasTotalIntObjUpShiftFunctor₁ 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso
instHasTotalIntObjUpShiftFunctor₂ 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms shiftFunctor₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso add_sub_cancel_right Subtype.coe_eta sub_add_cancel
shiftFunctor₁XXIso_refl 📖	mathematical	—	shiftFunctor₁XXIso CategoryTheory.Iso.refl HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
shiftFunctor₂XXIso_refl 📖	mathematical	—	shiftFunctor₂XXIso CategoryTheory.Iso.refl HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₂	—	AddRightCancelSemigroup.toIsRightCancelAdd
totalShift₁Iso_hom_naturality 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory total CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt total.map CategoryTheory.Functor.map CategoryTheory.Iso.hom totalShift₁Iso	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext instHasTotalIntObjUpShiftFunctor₁ total.hom_ext ιTotal_map_assoc ι_totalShift₁Iso_hom_f ι_totalShift₁Iso_hom_f_assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id ιTotal_map
totalShift₁Iso_hom_naturality_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory total CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ instHasTotalIntObjUpShiftFunctor₁ total.map CategoryTheory.Functor.map CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt CategoryTheory.Iso.hom totalShift₁Iso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' totalShift₁Iso_hom_naturality
totalShift₁Iso_hom_totalShift₂Iso_hom 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory total CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ shiftFunctor₂ instHasTotalIntObjUpShiftFunctor₁ instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt CategoryTheory.Iso.hom totalShift₁Iso CategoryTheory.Functor.map totalShift₂Iso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.comp instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddCommMonoid.toAddMonoid Int.instAddCommMonoid Units.instSMul HomologicalComplex.hasIntScalar Int.negOnePow instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ total.map CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctor₁₂CommIso CategoryTheory.shiftFunctorComm	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ instHasTotalIntObjUpShiftFunctor₂ instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ totalShift₁Iso_trans_totalShift₂Iso
totalShift₁Iso_hom_totalShift₂Iso_hom_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory total CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ shiftFunctor₂ instHasTotalIntObjUpShiftFunctor₁ instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt CategoryTheory.Iso.hom totalShift₁Iso CategoryTheory.Functor.map totalShift₂Iso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddCommMonoid.toAddMonoid Int.instAddCommMonoid Units.instSMul HomologicalComplex.hasIntScalar Int.negOnePow instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ total.map CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category shiftFunctor₁₂CommIso CategoryTheory.shiftFunctorComm	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ instHasTotalIntObjUpShiftFunctor₂ instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' totalShift₁Iso_hom_totalShift₂Iso_hom
totalShift₁Iso_trans_totalShift₂Iso 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.Iso.trans HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory total CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms shiftFunctor₁ shiftFunctor₂ instHasTotalIntObjUpShiftFunctor₁ instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup totalShift₁Iso CategoryTheory.Functor.mapIso totalShift₂Iso Units Int.instMonoid CategoryTheory.Iso CategoryTheory.Functor.comp instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ AddCommMonoid.toAddMonoid Int.instAddCommMonoid CategoryTheory.Preadditive.instSMulUnitsIntIso HomologicalComplex.instPreadditive Int.negOnePow instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ total.mapIso CategoryTheory.Iso.app shiftFunctor₁₂CommIso CategoryTheory.shiftFunctorComm	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Iso.ext instHasTotalIntObjUpShiftFunctor₁ instHasTotalIntObjUpShiftFunctor₂ instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁ instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂ HomologicalComplex.hom_ext total.hom_ext CategoryTheory.Linear.comp_units_smul ι_totalShift₁Iso_hom_f_assoc ιTotal_map_assoc ι_totalShift₂Iso_hom_f_assoc CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id ι_totalShift₂Iso_hom_f smul_smul Int.negOnePow_add add_mul Distrib.rightDistribClass add_comm CochainComplex.shiftFunctorComm_hom_app_f CategoryTheory.Iso.inv_hom_id
totalShift₂Iso_hom_naturality 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory total CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms shiftFunctor₂ instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt total.map CategoryTheory.Functor.map CategoryTheory.Iso.hom totalShift₂Iso	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext instHasTotalIntObjUpShiftFunctor₂ total.hom_ext ιTotal_map_assoc ι_totalShift₂Iso_hom_f ι_totalShift₂Iso_hom_f_assoc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Linear.comp_units_smul CategoryTheory.Linear.units_smul_comp ιTotal_map
totalShift₂Iso_hom_naturality_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory total CategoryTheory.Functor.obj HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms shiftFunctor₂ instHasTotalIntObjUpShiftFunctor₂ total.map CategoryTheory.Functor.map CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt CategoryTheory.Iso.hom totalShift₂Iso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' totalShift₂Iso_hom_naturality
ι_totalShift₁Iso_hom_f 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₁ total instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt ιTotal HomologicalComplex.Hom.f CategoryTheory.Iso.hom totalShift₁Iso AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex CochainComplex.shiftFunctor shiftFunctor₁XXIso CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ ι_totalDesc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
ι_totalShift₁Iso_hom_f_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₁ total instHasTotalIntObjUpShiftFunctor₁ ιTotal CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt HomologicalComplex.Hom.f CategoryTheory.Iso.hom totalShift₁Iso shiftFunctor₁XXIso CategoryTheory.Iso.inv AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex CochainComplex.shiftFunctor CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_totalShift₁Iso_hom_f
ι_totalShift₁Iso_inv_f 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₁ instHasTotalIntObjUpShiftFunctor₁ ιTotal AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex CochainComplex.shiftFunctor CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso HomologicalComplex.Hom.f CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt totalShift₁Iso shiftFunctor₁XXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.Category.id_comp ι_totalDesc
ι_totalShift₁Iso_inv_f_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.obj CochainComplex CochainComplex.shiftFunctor CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso HomologicalComplex₂ shiftFunctor₁ instHasTotalIntObjUpShiftFunctor₁ HomologicalComplex.Hom.f CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt totalShift₁Iso shiftFunctor₁XXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₁ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_totalShift₁Iso_inv_f
ι_totalShift₂Iso_hom_f 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₂ total instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt ιTotal HomologicalComplex.Hom.f CategoryTheory.Iso.hom totalShift₂Iso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex CochainComplex.shiftFunctor Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow shiftFunctor₂XXIso CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ ι_totalDesc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
ι_totalShift₂Iso_hom_f_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₂ total instHasTotalIntObjUpShiftFunctor₂ ιTotal CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt HomologicalComplex.Hom.f CategoryTheory.Iso.hom totalShift₂Iso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex CochainComplex.shiftFunctor Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow shiftFunctor₂XXIso CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_totalShift₂Iso_hom_f
ι_totalShift₂Iso_inv_f 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total CategoryTheory.Functor.obj HomologicalComplex₂ shiftFunctor₂ instHasTotalIntObjUpShiftFunctor₂ ιTotal AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex CochainComplex.shiftFunctor CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso HomologicalComplex.Hom.f CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt totalShift₂Iso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow shiftFunctor₂XXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.Category.id_comp ι_totalDesc
ι_totalShift₂Iso_inv_f_assoc 📖	mathematical	HasTotal ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.instTotalComplexShape Int.instAddMonoid ComplexShape.instTensorSignsIntUp	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.obj CochainComplex CochainComplex.shiftFunctor CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso HomologicalComplex₂ shiftFunctor₂ instHasTotalIntObjUpShiftFunctor₂ HomologicalComplex.Hom.f CategoryTheory.shiftFunctor CochainComplex.instHasShiftInt totalShift₂Iso Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Int.negOnePow shiftFunctor₂XXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasTotalIntObjUpShiftFunctor₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_totalShift₂Iso_inv_f

---

← Back to Index