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 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 flip map₂CochainComplex 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 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 flip map₂CochainComplex 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 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 map₂CochainComplex 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 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 map₂CochainComplex 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 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 flip map₂CochainComplex 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 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 map₂CochainComplex 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	—
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	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 HomologicalComplex₂.hasTotal_of_iso 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	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 HomologicalComplex₂.hasTotal_of_iso 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 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 HomologicalComplex₂ CategoryTheory.Functor.mapBifunctorHomologicalComplex CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex₂.shiftFunctor₁ CategoryTheory.Iso.hom AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive mapBifunctorHomologicalComplexShift₁Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mapBifunctorHomologicalComplexShift₁Iso_inv_f_f 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category	HomologicalComplex.Hom.f 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 HomologicalComplex₂ HomologicalComplex₂.shiftFunctor₁ CategoryTheory.Functor.mapBifunctorHomologicalComplex CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Iso.inv AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive mapBifunctorHomologicalComplexShift₁Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
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 HomologicalComplex₂ CategoryTheory.Functor.mapBifunctorHomologicalComplex CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt HomologicalComplex₂.shiftFunctor₂ CategoryTheory.Iso.hom AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive mapBifunctorHomologicalComplexShift₂Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
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 HomologicalComplex₂ HomologicalComplex₂.shiftFunctor₂ CategoryTheory.Functor.mapBifunctorHomologicalComplex CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt CategoryTheory.Iso.inv AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive mapBifunctorHomologicalComplexShift₂Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
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 ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.mapBifunctor AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt 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 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 ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.mapBifunctor AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt 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 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 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.shiftFunctor Int.instAddMonoid instHasShiftInt 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 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 ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.mapBifunctor AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt 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 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 ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex.mapBifunctor AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt 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 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 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 CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt mapBifunctor 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 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 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 CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt mapBifunctor 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 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 CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt mapBifunctor 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 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 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 CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt mapBifunctor 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