BifunctorAssociator

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

Statistics

Metric	Count
Definitions HasGoodTrifunctor₁₂Obj, HasGoodTrifunctor₂₃Obj, mapBifunctorAssociator, mapBifunctorAssociatorX, D₁, D₂, D₃, d₁, d₂, d₃, mapBifunctor₁₂Desc, ι, ιOrZero, D₁, D₂, D₃, d₁, d₂, d₃, mapBifunctor₂₃Desc, ι, ιOrZero	22
Theorems instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX, instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ, instHasMapProdObjGradedObjectFunctorMapBifunctorXπ, mapBifunctorAssociatorX_hom_D₁, mapBifunctorAssociatorX_hom_D₁_assoc, mapBifunctorAssociatorX_hom_D₂, mapBifunctorAssociatorX_hom_D₂_assoc, mapBifunctorAssociatorX_hom_D₃, mapBifunctorAssociatorX_hom_D₃_assoc, d_eq, d₁_eq, d₁_eq_zero, d₂_eq, d₂_eq_zero, d₃_eq, d₃_eq_zero, hom_ext, hom_ext_iff, ιOrZero_eq, ιOrZero_eq_zero, ι_D₁, ι_D₁_assoc, ι_D₂, ι_D₂_assoc, ι_D₃, ι_D₃_assoc, ι_eq, ι_mapBifunctor₁₂Desc, ι_mapBifunctor₁₂Desc_assoc, d_eq, d₁_eq, d₁_eq_zero, d₂_eq, d₂_eq_zero, d₃_eq, d₃_eq_zero, hom_ext, ιOrZero_eq, ιOrZero_eq_zero, ι_D₁, ι_D₁_assoc, ι_D₂, ι_D₂_assoc, ι_D₃, ι_D₃_assoc, ι_eq, ι_mapBifunctor₂₃Desc, ι_mapBifunctor₂₃Desc_assoc, ιOrZero_mapBifunctorAssociatorX_hom, ιOrZero_mapBifunctorAssociatorX_hom_assoc, ι_mapBifunctorAssociatorX_hom, ι_mapBifunctorAssociatorX_hom_assoc	52
Total	74

HomologicalComplex

Definitions

Name	Category	Theorems
HasGoodTrifunctor₁₂Obj 📖	MathDef	—
HasGoodTrifunctor₂₃Obj 📖	MathDef	—
mapBifunctorAssociator 📖	CompOp	—
mapBifunctorAssociatorX 📖	CompOp	10 math math: ι_mapBifunctorAssociatorX_hom, mapBifunctorAssociatorX_hom_D₂, mapBifunctorAssociatorX_hom_D₃_assoc, ι_mapBifunctorAssociatorX_hom_assoc, ιOrZero_mapBifunctorAssociatorX_hom, mapBifunctorAssociatorX_hom_D₂_assoc, mapBifunctorAssociatorX_hom_D₁, mapBifunctorAssociatorX_hom_D₃, mapBifunctorAssociatorX_hom_D₁_assoc, ιOrZero_mapBifunctorAssociatorX_hom_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive	CategoryTheory.GradedObject.HasMap CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.mapBifunctor CategoryTheory.GradedObject.mapBifunctorMapObj ComplexShape.π X instHasMapProdObjGradedObjectFunctorMapBifunctorXπ	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive	CategoryTheory.GradedObject.HasMap CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.mapBifunctor X CategoryTheory.GradedObject.mapBifunctorMapObj ComplexShape.π instHasMapProdObjGradedObjectFunctorMapBifunctorXπ	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
instHasMapProdObjGradedObjectFunctorMapBifunctorXπ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor	CategoryTheory.GradedObject.HasMap CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.mapBifunctor X ComplexShape.π	—	—
mapBifunctorAssociatorX_hom_D₁ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom mapBifunctorAssociatorX mapBifunctor₂₃.D₁ mapBifunctor₁₂.D₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive mapBifunctor₁₂.hom_ext mapBifunctor₁₂.ι_D₁_assoc ι_mapBifunctorAssociatorX_hom_assoc mapBifunctor₂₃.ι_D₁ CategoryTheory.NatTrans.naturality_app_app mapBifunctor₁₂.d₁_eq mapBifunctor₂₃.d₁_eq CategoryTheory.Linear.comp_units_smul CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc ComplexShape.associative_ε₁_eq_mul ιOrZero_mapBifunctorAssociatorX_hom smul_left_cancel_iff Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctor₁₂.d₁_eq_zero mapBifunctor₂₃.d₁_eq_zero CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
mapBifunctorAssociatorX_hom_D₁_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom mapBifunctorAssociatorX mapBifunctor₂₃.D₁ mapBifunctor₁₂.D₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctorAssociatorX_hom_D₁
mapBifunctorAssociatorX_hom_D₂ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom mapBifunctorAssociatorX mapBifunctor₂₃.D₂ mapBifunctor₁₂.D₂	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive mapBifunctor₁₂.hom_ext mapBifunctor₁₂.ι_D₂_assoc ι_mapBifunctorAssociatorX_hom_assoc mapBifunctor₂₃.ι_D₂ CategoryTheory.NatTrans.naturality_app mapBifunctor₁₂.d₂_eq mapBifunctor₂₃.d₂_eq CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc ιOrZero_mapBifunctorAssociatorX_hom Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Linear.comp_units_smul ComplexShape.associative_ε₂_ε₁ mapBifunctor₁₂.d₂_eq_zero mapBifunctor₂₃.d₂_eq_zero CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
mapBifunctorAssociatorX_hom_D₂_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom mapBifunctorAssociatorX mapBifunctor₂₃.D₂ mapBifunctor₁₂.D₂	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctorAssociatorX_hom_D₂
mapBifunctorAssociatorX_hom_D₃ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom mapBifunctorAssociatorX mapBifunctor₂₃.D₃ mapBifunctor₁₂.D₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive mapBifunctor₁₂.hom_ext mapBifunctor₁₂.ι_D₃_assoc ι_mapBifunctorAssociatorX_hom_assoc mapBifunctor₂₃.ι_D₃ mapBifunctor₁₂.d₃_eq mapBifunctor₂₃.d₃_eq CategoryTheory.Linear.comp_units_smul CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc ιOrZero_mapBifunctorAssociatorX_hom CategoryTheory.NatTrans.naturality_assoc ComplexShape.associative_ε₂_eq_mul mapBifunctor₁₂.d₃_eq_zero mapBifunctor₂₃.d₃_eq_zero CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
mapBifunctorAssociatorX_hom_D₃_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom mapBifunctorAssociatorX mapBifunctor₂₃.D₃ mapBifunctor₁₂.D₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapBifunctorAssociatorX_hom_D₃
ιOrZero_mapBifunctorAssociatorX_hom 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X mapBifunctor₁₂.ιOrZero CategoryTheory.Iso.hom mapBifunctorAssociatorX CategoryTheory.bifunctorComp₁₂ CategoryTheory.bifunctorComp₂₃ CategoryTheory.NatTrans.app mapBifunctor₂₃.ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive mapBifunctor₁₂.ιOrZero_eq mapBifunctor₂₃.ιOrZero_eq ι_mapBifunctorAssociatorX_hom mapBifunctor₁₂.ιOrZero_eq_zero mapBifunctor₂₃.ιOrZero_eq_zero CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
ιOrZero_mapBifunctorAssociatorX_hom_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X mapBifunctor₁₂.ιOrZero CategoryTheory.Iso.hom mapBifunctorAssociatorX CategoryTheory.bifunctorComp₂₃ CategoryTheory.NatTrans.app CategoryTheory.bifunctorComp₁₂ mapBifunctor₂₃.ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιOrZero_mapBifunctorAssociatorX_hom
ι_mapBifunctorAssociatorX_hom 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X mapBifunctor₁₂.ι CategoryTheory.Iso.hom mapBifunctorAssociatorX CategoryTheory.bifunctorComp₁₂ CategoryTheory.bifunctorComp₂₃ CategoryTheory.NatTrans.app mapBifunctor₂₃.ι	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom instHasMapProdObjGradedObjectFunctorMapBifunctorXπ
ι_mapBifunctorAssociatorX_hom_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HasMapBifunctor mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X mapBifunctor₁₂.ι CategoryTheory.Iso.hom mapBifunctorAssociatorX CategoryTheory.bifunctorComp₂₃ CategoryTheory.NatTrans.app CategoryTheory.bifunctorComp₁₂ mapBifunctor₂₃.ι	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorAssociatorX_hom

HomologicalComplex.mapBifunctor₁₂

Definitions

Name	Category	Theorems
D₁ 📖	CompOp	5 math math: d_eq, ι_D₁_assoc, ι_D₁, HomologicalComplex.mapBifunctorAssociatorX_hom_D₁, HomologicalComplex.mapBifunctorAssociatorX_hom_D₁_assoc
D₂ 📖	CompOp	5 math math: d_eq, ι_D₂_assoc, HomologicalComplex.mapBifunctorAssociatorX_hom_D₂, HomologicalComplex.mapBifunctorAssociatorX_hom_D₂_assoc, ι_D₂
D₃ 📖	CompOp	5 math math: ι_D₃_assoc, d_eq, HomologicalComplex.mapBifunctorAssociatorX_hom_D₃_assoc, ι_D₃, HomologicalComplex.mapBifunctorAssociatorX_hom_D₃
d₁ 📖	CompOp	4 math math: ι_D₁_assoc, ι_D₁, d₁_eq_zero, d₁_eq
d₂ 📖	CompOp	4 math math: ι_D₂_assoc, d₂_eq_zero, ι_D₂, d₂_eq
d₃ 📖	CompOp	4 math math: ι_D₃_assoc, ι_D₃, d₃_eq_zero, d₃_eq
mapBifunctor₁₂Desc 📖	CompOp	2 math math: ι_mapBifunctor₁₂Desc, ι_mapBifunctor₁₂Desc_assoc
ι 📖	CompOp	13 math math: ι_D₃_assoc, HomologicalComplex.ι_mapBifunctorAssociatorX_hom, ι_D₁_assoc, hom_ext_iff, ι_mapBifunctor₁₂Desc, ι_D₂_assoc, ι_D₁, HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc, ι_D₃, ιOrZero_eq, ι_eq, ι_D₂, ι_mapBifunctor₁₂Desc_assoc
ιOrZero 📖	CompOp	7 math math: ιOrZero_eq_zero, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom, ιOrZero_eq, d₁_eq, d₃_eq, d₂_eq, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HomologicalComplex.HasGoodTrifunctor₁₂Obj	HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup D₁ D₂ D₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.mapBifunctor.d_eq hom_ext CategoryTheory.Preadditive.comp_add ι_D₁ ι_D₂ ι_eq CategoryTheory.Category.assoc HomologicalComplex.mapBifunctor.ι_D₁ HomologicalComplex.mapBifunctor.d₁_eq CategoryTheory.Functor.map_add CategoryTheory.Preadditive.add_comp smul_add CategoryTheory.Linear.comp_units_smul CategoryTheory.NatTrans.comp_app_assoc CategoryTheory.Functor.map_comp ComplexShape.next_π₁ d₁_eq ιOrZero_eq CategoryTheory.Functor.map_units_smul CategoryTheory.Functor.intLinear CategoryTheory.NatTrans.app_units_zsmul CategoryTheory.NatTrans.comp_app CategoryTheory.Linear.units_smul_comp smul_smul d₁_eq_zero HomologicalComplex.mapBifunctor.d₁_eq_zero CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_app CategoryTheory.Limits.zero_comp smul_zero HomologicalComplex.mapBifunctor.ι_D₂ ComplexShape.next_π₂ HomologicalComplex.mapBifunctor.d₂_eq d₂_eq d₂_eq_zero HomologicalComplex.mapBifunctor.d₂_eq_zero HomologicalComplex.mapBifunctor.d₁_eq_zero' CategoryTheory.Limits.comp_zero add_zero ιOrZero_eq_zero ComplexShape.rel_π₁ ComplexShape.next_eq' ComplexShape.rel_π₂ zero_add
d₁_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel	d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Units.instMul ComplexShape.ε₁ ComplexShape.π CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.d ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.next_eq'
d₁_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel ComplexShape.next	d₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.shape CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_app CategoryTheory.Limits.zero_comp smul_zero
d₂_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel	d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Units.instMul ComplexShape.ε₁ ComplexShape.π ComplexShape.ε₂ CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.d ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.next_eq'
d₂_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel ComplexShape.next	d₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.shape CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_app CategoryTheory.Limits.zero_comp smul_zero
d₃_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel	d₃ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ ComplexShape.π CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map HomologicalComplex.d ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.next_eq'
d₃_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.Rel ComplexShape.next	d₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.shape CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_comp smul_zero
hom_ext 📖	—	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HomologicalComplex.HasGoodTrifunctor₁₂Obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι	—	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ
hom_ext_iff 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HomologicalComplex.HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive hom_ext
ιOrZero_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.r	ιOrZero ι	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
ιOrZero_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive	ιOrZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
ι_D₁ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₁ d₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ι_mapBifunctor₁₂Desc
ι_D₁_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₁ d₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₁
ι_D₂ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₂ d₂	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ι_mapBifunctor₁₂Desc
ι_D₂_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₂ d₂	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₂
ι_D₃ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₃ d₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ι_eq CategoryTheory.Category.assoc HomologicalComplex.mapBifunctor.ι_D₂ d₃_eq HomologicalComplex.mapBifunctor.d₂_eq ιOrZero_eq CategoryTheory.Linear.comp_units_smul smul_left_cancel_iff CategoryTheory.NatTrans.naturality_assoc HomologicalComplex.mapBifunctor.d₂_eq_zero' CategoryTheory.Limits.comp_zero ιOrZero_eq_zero smul_zero HomologicalComplex.mapBifunctor.d₂_eq_zero d₃_eq_zero
ι_D₃_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₃ d₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₃
ι_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive ComplexShape.π	ι CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.ιMapBifunctor	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
ι_mapBifunctor₁₂Desc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HomologicalComplex.HasGoodTrifunctor₁₂Obj ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι mapBifunctor₁₂Desc	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.GradedObject.ι_mapBifunctor₁₂BifunctorDesc HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ
ι_mapBifunctor₁₂Desc_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.functorCategoryPreadditive HomologicalComplex.HasGoodTrifunctor₁₂Obj ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι mapBifunctor₁₂Desc	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctor₁₂Desc

HomologicalComplex.mapBifunctor₂₃

Definitions

Name	Category	Theorems
D₁ 📖	CompOp	5 math math: ι_D₁, HomologicalComplex.mapBifunctorAssociatorX_hom_D₁, ι_D₁_assoc, d_eq, HomologicalComplex.mapBifunctorAssociatorX_hom_D₁_assoc
D₂ 📖	CompOp	5 math math: HomologicalComplex.mapBifunctorAssociatorX_hom_D₂, ι_D₂, HomologicalComplex.mapBifunctorAssociatorX_hom_D₂_assoc, d_eq, ι_D₂_assoc
D₃ 📖	CompOp	5 math math: ι_D₃, HomologicalComplex.mapBifunctorAssociatorX_hom_D₃_assoc, d_eq, HomologicalComplex.mapBifunctorAssociatorX_hom_D₃, ι_D₃_assoc
d₁ 📖	CompOp	4 math math: ι_D₁, d₁_eq, ι_D₁_assoc, d₁_eq_zero
d₂ 📖	CompOp	4 math math: d₂_eq, ι_D₂, d₂_eq_zero, ι_D₂_assoc
d₃ 📖	CompOp	4 math math: ι_D₃, d₃_eq, d₃_eq_zero, ι_D₃_assoc
mapBifunctor₂₃Desc 📖	CompOp	2 math math: ι_mapBifunctor₂₃Desc, ι_mapBifunctor₂₃Desc_assoc
ι 📖	CompOp	12 math math: ι_D₃, HomologicalComplex.ι_mapBifunctorAssociatorX_hom, ι_mapBifunctor₂₃Desc, ι_D₁, ι_mapBifunctor₂₃Desc_assoc, ι_D₂, ιOrZero_eq, HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc, ι_eq, ι_D₁_assoc, ι_D₃_assoc, ι_D₂_assoc
ιOrZero 📖	CompOp	7 math math: d₂_eq, d₃_eq, ιOrZero_eq_zero, ιOrZero_eq, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom, d₁_eq, HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.HasGoodTrifunctor₂₃Obj	HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup D₁ D₂ D₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.mapBifunctor.d_eq add_assoc hom_ext CategoryTheory.Preadditive.comp_add ι_D₂ ι_D₃ ComplexShape.assoc ι_eq CategoryTheory.Category.assoc HomologicalComplex.mapBifunctor.ι_D₂ HomologicalComplex.mapBifunctor.d₂_eq CategoryTheory.Linear.comp_units_smul CategoryTheory.Functor.map_add CategoryTheory.Preadditive.add_comp smul_add CategoryTheory.Functor.map_comp_assoc HomologicalComplex.mapBifunctor.ι_D₁ d₂_eq ComplexShape.next_π₁ HomologicalComplex.mapBifunctor.d₁_eq CategoryTheory.Functor.map_units_smul CategoryTheory.Functor.intLinear CategoryTheory.Functor.map_comp CategoryTheory.Linear.units_smul_comp smul_smul smul_left_cancel_iff ιOrZero_eq d₂_eq_zero HomologicalComplex.mapBifunctor.d₁_eq_zero CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_comp smul_zero d₃_eq ComplexShape.next_π₂ d₃_eq_zero HomologicalComplex.mapBifunctor.d₂_eq_zero HomologicalComplex.mapBifunctor.d₂_eq_zero' CategoryTheory.Limits.comp_zero add_zero ιOrZero_eq_zero ComplexShape.rel_π₁ ComplexShape.rel_π₂
d₁_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.Rel	d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ ComplexShape.π CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.d ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.next_eq'
d₁_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.Rel ComplexShape.next	d₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.shape CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_app CategoryTheory.Limits.zero_comp smul_zero
d₂_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.Rel	d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Units.instMul ComplexShape.ε₂ ComplexShape.π ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map CategoryTheory.NatTrans.app HomologicalComplex.d ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.next_eq'
d₂_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.Rel ComplexShape.next	d₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.shape CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_app CategoryTheory.Limits.zero_comp smul_zero
d₃_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.Rel	d₃ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup Units.instMul ComplexShape.ε₂ ComplexShape.π CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map HomologicalComplex.d ιOrZero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.next_eq'
d₃_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.Rel ComplexShape.next	d₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.shape CategoryTheory.Functor.map_zero CategoryTheory.Limits.zero_comp smul_zero
hom_ext 📖	—	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.HasGoodTrifunctor₂₃Obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι	—	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ
ιOrZero_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.r	ιOrZero ι	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
ιOrZero_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive	ιOrZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
ι_D₁ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₁ d₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.assoc ι_eq CategoryTheory.Category.assoc HomologicalComplex.mapBifunctor.ι_D₁ d₁_eq HomologicalComplex.mapBifunctor.d₁_eq ιOrZero_eq CategoryTheory.Linear.comp_units_smul CategoryTheory.NatTrans.naturality_assoc HomologicalComplex.mapBifunctor.d₁_eq_zero' CategoryTheory.Limits.comp_zero ιOrZero_eq_zero smul_zero HomologicalComplex.mapBifunctor.d₁_eq_zero d₁_eq_zero
ι_D₁_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₁ d₁	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₁
ι_D₂ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₂ d₂	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ι_mapBifunctor₂₃Desc
ι_D₂_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₂ d₂	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₂
ι_D₃ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₃ d₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive ι_mapBifunctor₂₃Desc
ι_D₃_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.r HomologicalComplex.HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι D₃ d₃	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₃
ι_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive ComplexShape.π	ι CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Functor.map HomologicalComplex.ιMapBifunctor	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
ι_mapBifunctor₂₃Desc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.HasGoodTrifunctor₂₃Obj ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι mapBifunctor₂₃Desc	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.GradedObject.ι_mapBifunctorBifunctor₂₃Desc HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ
ι_mapBifunctor₂₃Desc_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.Additive HomologicalComplex.HasMapBifunctor HomologicalComplex.mapBifunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.HasGoodTrifunctor₂₃Obj ComplexShape.r	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ι mapBifunctor₂₃Desc	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctor₂₃Desc

---

← Back to Index