Documentation Verification Report

BifunctorShift

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

Statistics

Metric	Count
Definitions `instCommShiftCochainComplexIntObjFlipMap₂CochainComplex`, `instCommShiftCochainComplexIntObjMap₂CochainComplex`, `instCommShift₂IntCochainComplexIntMap₂CochainComplex`, `HasMapBifunctor`, `mapBifunctor`, `mapBifunctorHomologicalComplexShift₁Iso`, `mapBifunctorHomologicalComplexShift₂Iso`, `mapBifunctorShift₁Iso`, `mapBifunctorShift₂Iso`, `ιMapBifunctor`	10
Theorems `commShiftIso_map₂CochainComplex_flip_hom_app`, `commShiftIso_map₂CochainComplex_flip_inv_app`, `commShiftIso_map₂CochainComplex_hom_app`, `commShiftIso_map₂CochainComplex_inv_app`, `instCommShiftCochainComplexIntMapFlipMap₂CochainComplex`, `instCommShiftCochainComplexIntMapMap₂CochainComplex`, `instHasMapBifunctorObjIntShiftFunctor`, `instHasMapBifunctorObjIntShiftFunctor_1`, `mapBifunctorHomologicalComplexShift₁Iso_hom_f_f`, `mapBifunctorHomologicalComplexShift₁Iso_inv_f_f`, `mapBifunctorHomologicalComplexShift₂Iso_hom_f_f`, `mapBifunctorHomologicalComplexShift₂Iso_inv_f_f`, `mapBifunctorShift₁Iso_hom_naturality₁`, `mapBifunctorShift₁Iso_hom_naturality₁_assoc`, `mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso`, `mapBifunctorShift₂Iso_hom_naturality₂`, `mapBifunctorShift₂Iso_hom_naturality₂_assoc`, `ι_mapBifunctorShift₁Iso_hom_f`, `ι_mapBifunctorShift₁Iso_hom_f_assoc`, `ι_mapBifunctorShift₂Iso_hom_f`, `ι_mapBifunctorShift₂Iso_hom_f_assoc`	21
Total	31

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`instCommShiftCochainComplexIntObjFlipMap₂CochainComplex` 📖	CompOp	3 math math: `commShiftIso_map₂CochainComplex_flip_hom_app`, `commShiftIso_map₂CochainComplex_flip_inv_app`, `instCommShiftCochainComplexIntMapFlipMap₂CochainComplex`
`instCommShiftCochainComplexIntObjMap₂CochainComplex` 📖	CompOp	3 math math: `commShiftIso_map₂CochainComplex_inv_app`, `instCommShiftCochainComplexIntMapMap₂CochainComplex`, `commShiftIso_map₂CochainComplex_hom_app`
`instCommShift₂IntCochainComplexIntMap₂CochainComplex` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commShiftIso_map₂CochainComplex_flip_hom_app` 📖	mathematical	`Additive` `obj` `CategoryTheory.Functor` `category` `CochainComplex.HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.NatTrans.app` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `obj` `CategoryTheory.Functor` `category` `flip` `map₂CochainComplex` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Iso.hom` `CommShift.commShiftIso` `instCommShiftCochainComplexIntObjFlipMap₂CochainComplex` `CochainComplex.mapBifunctor` `CochainComplex.instHasMapBifunctorObjIntShiftFunctor` `CochainComplex.mapBifunctorShift₁Iso`	—	`preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd`
`commShiftIso_map₂CochainComplex_flip_inv_app` 📖	mathematical	`Additive` `obj` `CategoryTheory.Functor` `category` `CochainComplex.HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.NatTrans.app` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `comp` `obj` `CategoryTheory.Functor` `category` `flip` `map₂CochainComplex` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `CategoryTheory.Iso.inv` `CommShift.commShiftIso` `instCommShiftCochainComplexIntObjFlipMap₂CochainComplex` `CochainComplex.mapBifunctor` `CochainComplex.instHasMapBifunctorObjIntShiftFunctor` `CochainComplex.mapBifunctorShift₁Iso`	—	`preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd`
`commShiftIso_map₂CochainComplex_hom_app` 📖	mathematical	`Additive` `obj` `CategoryTheory.Functor` `category` `CochainComplex.HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.NatTrans.app` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `comp` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `obj` `CategoryTheory.Functor` `category` `map₂CochainComplex` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.Iso.hom` `CommShift.commShiftIso` `instCommShiftCochainComplexIntObjMap₂CochainComplex` `CochainComplex.mapBifunctor` `CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1` `CochainComplex.mapBifunctorShift₂Iso`	—	`preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd`
`commShiftIso_map₂CochainComplex_inv_app` 📖	mathematical	`Additive` `obj` `CategoryTheory.Functor` `category` `CochainComplex.HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.NatTrans.app` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `comp` `obj` `CategoryTheory.Functor` `category` `map₂CochainComplex` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `CategoryTheory.Iso.inv` `CommShift.commShiftIso` `instCommShiftCochainComplexIntObjMap₂CochainComplex` `CochainComplex.mapBifunctor` `CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1` `CochainComplex.mapBifunctorShift₂Iso`	—	`preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd`
`instCommShiftCochainComplexIntMapFlipMap₂CochainComplex` 📖	mathematical	`Additive` `obj` `CategoryTheory.Functor` `category` `CochainComplex.HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.NatTrans.CommShift` `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` `obj` `CategoryTheory.Functor` `category` `flip` `map₂CochainComplex` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `map` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `instCommShiftCochainComplexIntObjFlipMap₂CochainComplex`	—	`preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.NatTrans.ext'` `HomologicalComplex.hom_ext` `HomologicalComplex.mapBifunctor.hom_ext` `CochainComplex.instHasMapBifunctorObjIntShiftFunctor` `CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc` `map_id` `CategoryTheory.Category.id_comp` `HomologicalComplex.ι_mapBifunctorMap` `HomologicalComplex.ι_mapBifunctorMap_assoc` `CochainComplex.ι_mapBifunctorShift₁Iso_hom_f` `CategoryTheory.Category.comp_id`
`instCommShiftCochainComplexIntMapMap₂CochainComplex` 📖	mathematical	`Additive` `obj` `CategoryTheory.Functor` `category` `CochainComplex.HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.NatTrans.CommShift` `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` `obj` `CategoryTheory.Functor` `category` `map₂CochainComplex` `preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `map` `Int.instAddMonoid` `CochainComplex.instHasShiftInt` `instCommShiftCochainComplexIntObjMap₂CochainComplex`	—	`preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.NatTrans.ext'` `HomologicalComplex.hom_ext` `HomologicalComplex.mapBifunctor.hom_ext` `CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1` `CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc` `map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Linear.units_smul_comp` `HomologicalComplex.ι_mapBifunctorMap` `HomologicalComplex.ι_mapBifunctorMap_assoc` `CochainComplex.ι_mapBifunctorShift₂Iso_hom_f` `CategoryTheory.Linear.comp_units_smul`

CochainComplex

Definitions

Name	Category	Theorems
`HasMapBifunctor` 📖	MathDef	2 math math: `instHasMapBifunctorObjIntShiftFunctor_1`, `instHasMapBifunctorObjIntShiftFunctor`
`mapBifunctor` 📖	CompOp	13 math math: `mapBifunctorShift₂Iso_hom_naturality₂_assoc`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app`, `mapBifunctorShift₁Iso_hom_naturality₁_assoc`, `ι_mapBifunctorShift₂Iso_hom_f_assoc`, `mapBifunctorShift₂Iso_hom_naturality₂`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app`, `ι_mapBifunctorShift₂Iso_hom_f`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app`, `ι_mapBifunctorShift₁Iso_hom_f_assoc`, `mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso`, `mapBifunctorShift₁Iso_hom_naturality₁`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app`, `ι_mapBifunctorShift₁Iso_hom_f`
`mapBifunctorHomologicalComplexShift₁Iso` 📖	CompOp	2 math math: `mapBifunctorHomologicalComplexShift₁Iso_hom_f_f`, `mapBifunctorHomologicalComplexShift₁Iso_inv_f_f`
`mapBifunctorHomologicalComplexShift₂Iso` 📖	CompOp	2 math math: `mapBifunctorHomologicalComplexShift₂Iso_inv_f_f`, `mapBifunctorHomologicalComplexShift₂Iso_hom_f_f`
`mapBifunctorShift₁Iso` 📖	CompOp	7 math math: `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app`, `mapBifunctorShift₁Iso_hom_naturality₁_assoc`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app`, `ι_mapBifunctorShift₁Iso_hom_f_assoc`, `mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso`, `mapBifunctorShift₁Iso_hom_naturality₁`, `ι_mapBifunctorShift₁Iso_hom_f`
`mapBifunctorShift₂Iso` 📖	CompOp	7 math math: `mapBifunctorShift₂Iso_hom_naturality₂_assoc`, `ι_mapBifunctorShift₂Iso_hom_f_assoc`, `mapBifunctorShift₂Iso_hom_naturality₂`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app`, `ι_mapBifunctorShift₂Iso_hom_f`, `mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app`
`ιMapBifunctor` 📖	CompOp	4 math math: `ι_mapBifunctorShift₂Iso_hom_f_assoc`, `ι_mapBifunctorShift₂Iso_hom_f`, `ι_mapBifunctorShift₁Iso_hom_f_assoc`, `ι_mapBifunctorShift₁Iso_hom_f`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasMapBifunctorObjIntShiftFunctor` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `HomologicalComplex₂.hasTotal_of_iso` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁`
`instHasMapBifunctorObjIntShiftFunctor_1` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`	`HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `HomologicalComplex₂.hasTotal_of_iso` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂`
`mapBifunctorHomologicalComplexShift₁Iso_hom_f_f` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.X` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Functor.obj` `HomologicalComplex₂` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.mapBifunctorHomologicalComplex` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `HomologicalComplex₂.shiftFunctor₁` `CategoryTheory.Iso.hom` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `mapBifunctorHomologicalComplexShift₁Iso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono`
`mapBifunctorHomologicalComplexShift₁Iso_inv_f_f` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.X` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Functor.obj` `HomologicalComplex₂` `HomologicalComplex₂.shiftFunctor₁` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.mapBifunctorHomologicalComplex` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Iso.inv` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `mapBifunctorHomologicalComplexShift₁Iso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono`
`mapBifunctorHomologicalComplexShift₂Iso_hom_f_f` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.X` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Functor.obj` `HomologicalComplex₂` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.mapBifunctorHomologicalComplex` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `HomologicalComplex₂.shiftFunctor₂` `CategoryTheory.Iso.hom` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `mapBifunctorHomologicalComplexShift₂Iso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono`
`mapBifunctorHomologicalComplexShift₂Iso_inv_f_f` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category`	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.X` `HomologicalComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Functor.obj` `HomologicalComplex₂` `HomologicalComplex₂.shiftFunctor₂` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.mapBifunctorHomologicalComplex` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Iso.inv` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `mapBifunctorHomologicalComplexShift₂Iso` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono`
`mapBifunctorShift₁Iso_hom_naturality₁` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.mapBifunctor` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `ComplexShape.instTotalComplexShape` `ComplexShape.instTensorSignsIntUp` `instHasMapBifunctorObjIntShiftFunctor` `CochainComplex` `mapBifunctor` `HomologicalComplex.mapBifunctorMap` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.hom` `mapBifunctorShift₁Iso`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `HomologicalComplex.hom_ext` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `instHasMapBifunctorObjIntShiftFunctor` `HomologicalComplex.mapBifunctor.hom_ext` `HomologicalComplex.ι_mapBifunctorMap_assoc` `CategoryTheory.Functor.map_id` `ι_mapBifunctorShift₁Iso_hom_f` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `ι_mapBifunctorShift₁Iso_hom_f_assoc` `HomologicalComplex.ι_mapBifunctorMap`
`mapBifunctorShift₁Iso_hom_naturality₁_assoc` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.mapBifunctor` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `ComplexShape.instTotalComplexShape` `ComplexShape.instTensorSignsIntUp` `instHasMapBifunctorObjIntShiftFunctor` `HomologicalComplex.mapBifunctorMap` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.id` `CochainComplex` `mapBifunctor` `CategoryTheory.Iso.hom` `mapBifunctorShift₁Iso`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `instHasMapBifunctorObjIntShiftFunctor` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mapBifunctorShift₁Iso_hom_naturality₁`
`mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.Iso.trans` `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` `mapBifunctor` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.functorCategoryPreadditive` `instHasMapBifunctorObjIntShiftFunctor` `instHasMapBifunctorObjIntShiftFunctor_1` `mapBifunctorShift₁Iso` `CategoryTheory.Functor.mapIso` `mapBifunctorShift₂Iso` `Units` `Int.instMonoid` `CategoryTheory.Iso` `CategoryTheory.Functor.comp` `AddCommMonoid.toAddMonoid` `Int.instAddCommMonoid` `CategoryTheory.Preadditive.instSMulUnitsIntIso` `HomologicalComplex.instPreadditive` `Int.negOnePow` `CategoryTheory.Iso.app` `CategoryTheory.shiftFunctorComm`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Iso.ext` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasMapBifunctorObjIntShiftFunctor` `instHasMapBifunctorObjIntShiftFunctor_1` `CategoryTheory.Functor.map_comp` `CategoryTheory.Category.assoc` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁` `HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc` `HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁` `HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂` `HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂` `HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom` `HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc` `CategoryTheory.Linear.comp_units_smul` `smul_left_cancel_iff` `HomologicalComplex₂.total.map_comp_assoc` `HomologicalComplex.hom_ext` `CategoryTheory.Category.id_comp`
`mapBifunctorShift₂Iso_hom_naturality₂` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.mapBifunctor` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `ComplexShape.instTotalComplexShape` `ComplexShape.instTensorSignsIntUp` `instHasMapBifunctorObjIntShiftFunctor_1` `CochainComplex` `mapBifunctor` `HomologicalComplex.mapBifunctorMap` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `mapBifunctorShift₂Iso`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `HomologicalComplex.hom_ext` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `instHasMapBifunctorObjIntShiftFunctor_1` `HomologicalComplex.mapBifunctor.hom_ext` `HomologicalComplex.ι_mapBifunctorMap_assoc` `CategoryTheory.Functor.map_id` `ι_mapBifunctorShift₂Iso_hom_f` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.Linear.comp_units_smul` `ι_mapBifunctorShift₂Iso_hom_f_assoc` `CategoryTheory.Linear.units_smul_comp` `HomologicalComplex.ι_mapBifunctorMap`
`mapBifunctorShift₂Iso_hom_naturality₂_assoc` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`	`CategoryTheory.CategoryStruct.comp` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.instCategory` `HomologicalComplex.mapBifunctor` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `ComplexShape.instTotalComplexShape` `ComplexShape.instTensorSignsIntUp` `instHasMapBifunctorObjIntShiftFunctor_1` `HomologicalComplex.mapBifunctorMap` `CategoryTheory.CategoryStruct.id` `CochainComplex` `CategoryTheory.Functor.map` `mapBifunctor` `CategoryTheory.Iso.hom` `mapBifunctorShift₂Iso`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `instHasMapBifunctorObjIntShiftFunctor_1` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mapBifunctorShift₂Iso_hom_naturality₂`
`ι_mapBifunctorShift₁Iso_hom_f` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `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` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `mapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `instHasMapBifunctorObjIntShiftFunctor` `ιMapBifunctor` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `mapBifunctorShift₁Iso` `shiftFunctor` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.map` `shiftFunctorObjXIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasMapBifunctorObjIntShiftFunctor` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `HomologicalComplex₂.ιTotal_map_assoc` `HomologicalComplex₂.ι_totalShift₁Iso_hom_f` `CategoryTheory.Functor.congr_obj` `CategoryTheory.Category.id_comp` `CategoryTheory.eqToHom_map` `CategoryTheory.eqToHom_app`
`ι_mapBifunctorShift₁Iso_hom_f_assoc` 📖	mathematical	`CategoryTheory.Functor.PreservesZeroMorphisms` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `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` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `mapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `instHasMapBifunctorObjIntShiftFunctor` `ιMapBifunctor` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `mapBifunctorShift₁Iso` `CategoryTheory.NatTrans.app` `shiftFunctor` `CategoryTheory.Functor.map` `shiftFunctorObjXIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasMapBifunctorObjIntShiftFunctor` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_mapBifunctorShift₁Iso_hom_f`
`ι_mapBifunctorShift₂Iso_hom_f` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HomologicalComplex.X` `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.Preadditive.preadditiveHasZeroMorphisms` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `mapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instHasMapBifunctorObjIntShiftFunctor_1` `ιMapBifunctor` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `mapBifunctorShift₂Iso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `shiftFunctor` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `Int.negOnePow` `CategoryTheory.Functor.map` `shiftFunctorObjXIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasMapBifunctorObjIntShiftFunctor_1` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `HomologicalComplex₂.ιTotal_map_assoc` `HomologicalComplex₂.ι_totalShift₂Iso_hom_f` `CategoryTheory.Linear.comp_units_smul` `CategoryTheory.Category.id_comp` `CategoryTheory.eqToHom_map`
`ι_mapBifunctorShift₂Iso_hom_f_assoc` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HasMapBifunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `HomologicalComplex.X` `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.Preadditive.preadditiveHasZeroMorphisms` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `mapBifunctor` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instHasMapBifunctorObjIntShiftFunctor_1` `ιMapBifunctor` `HomologicalComplex.Hom.f` `CategoryTheory.Iso.hom` `mapBifunctorShift₂Iso` `Units` `Int.instMonoid` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `shiftFunctor` `Units.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `Int.negOnePow` `CategoryTheory.Functor.map` `shiftFunctorObjXIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasMapBifunctorObjIntShiftFunctor_1` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_mapBifunctorShift₂Iso_hom_f`

---

← Back to Index