Bifunctor

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

Statistics

Metric	Count
Definitions mapBifunctorHomologicalComplex, mapBifunctorHomologicalComplexObj, map₂CochainComplex, map₂HomologicalComplex, HasMapBifunctor, mapBifunctor, D₁, D₂, d₁, d₂, mapBifunctorDesc, mapBifunctorMap, ιMapBifunctor, ιMapBifunctorOrZero	14
Theorems mapBifunctorHomologicalComplexObj_map_f_f, mapBifunctorHomologicalComplexObj_obj_X_X, mapBifunctorHomologicalComplexObj_obj_X_d, mapBifunctorHomologicalComplexObj_obj_d_f, mapBifunctorHomologicalComplex_map_app_f_f, mapBifunctorHomologicalComplex_obj_map_f_f, mapBifunctorHomologicalComplex_obj_obj_X_X, mapBifunctorHomologicalComplex_obj_obj_X_d, mapBifunctorHomologicalComplex_obj_obj_d_f, mapBifunctorHomologicalComplex_obj_obj_toGradedObject, map₂HomologicalComplex_map_app, map₂HomologicalComplex_obj_map, map₂HomologicalComplex_obj_obj, d_eq, d₁_eq, d₁_eq', d₁_eq_zero, d₁_eq_zero', d₂_eq, d₂_eq', d₂_eq_zero, d₂_eq_zero', hom_ext, hom_ext_iff, ι_D₁, ι_D₁_assoc, ι_D₂, ι_D₂_assoc, ιMapBifunctorOrZero_eq, ιMapBifunctorOrZero_eq_zero, ι_mapBifunctorDesc, ι_mapBifunctorDesc_assoc, ι_mapBifunctorMap, ι_mapBifunctorMap_assoc	34
Total	48

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapBifunctorHomologicalComplex 📖	CompOp	11 math math: mapBifunctorHomologicalComplex_map_app_f_f, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, mapBifunctorHomologicalComplex_obj_obj_X_d, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, mapBifunctorHomologicalComplex_obj_obj_X_X, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, mapBifunctorHomologicalComplex_obj_map_f_f, mapBifunctorHomologicalComplex_obj_obj_toGradedObject, mapBifunctorHomologicalComplex_obj_obj_d_f
mapBifunctorHomologicalComplexObj 📖	CompOp	5 math math: mapBifunctorHomologicalComplexObj_map_f_f, mapBifunctorHomologicalComplexObj_obj_X_d, mapBifunctorHomologicalComplexObj_obj_X_X, mapBifunctorHomologicalComplex_map_app_f_f, mapBifunctorHomologicalComplexObj_obj_d_f
map₂CochainComplex 📖	CompOp	6 math math: commShiftIso_map₂CochainComplex_flip_hom_app, commShiftIso_map₂CochainComplex_inv_app, commShiftIso_map₂CochainComplex_flip_inv_app, instCommShiftCochainComplexIntMapMap₂CochainComplex, instCommShiftCochainComplexIntMapFlipMap₂CochainComplex, commShiftIso_map₂CochainComplex_hom_app
map₂HomologicalComplex 📖	CompOp	3 math math: map₂HomologicalComplex_map_app, map₂HomologicalComplex_obj_obj, map₂HomologicalComplex_obj_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapBifunctorHomologicalComplexObj_map_f_f 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂.ofGradedObject obj CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.Functor category CategoryTheory.GradedObject.mapBifunctor CategoryTheory.NatTrans.app map HomologicalComplex.d HomologicalComplex₂ mapBifunctorHomologicalComplexObj	—	—
mapBifunctorHomologicalComplexObj_obj_X_X 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms obj HomologicalComplex₂ mapBifunctorHomologicalComplexObj CategoryTheory.Functor category	—	—
mapBifunctorHomologicalComplexObj_obj_X_d 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.d HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms obj HomologicalComplex₂ mapBifunctorHomologicalComplexObj map CategoryTheory.Functor category	—	—
mapBifunctorHomologicalComplexObj_obj_d_f 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.Hom.f obj CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.Functor category CategoryTheory.GradedObject.mapBifunctor HomologicalComplex.X map HomologicalComplex.d HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂ mapBifunctorHomologicalComplexObj CategoryTheory.NatTrans.app	—	—
mapBifunctorHomologicalComplex_map_app_f_f 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms obj HomologicalComplex₂ mapBifunctorHomologicalComplexObj CategoryTheory.NatTrans.app map CategoryTheory.Functor category mapBifunctorHomologicalComplex	—	—
mapBifunctorHomologicalComplex_obj_map_f_f 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.Hom.f HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂.ofGradedObject obj CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.Functor category CategoryTheory.GradedObject.mapBifunctor CategoryTheory.NatTrans.app map HomologicalComplex.d HomologicalComplex₂ mapBifunctorHomologicalComplex	—	—
mapBifunctorHomologicalComplex_obj_obj_X_X 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms obj HomologicalComplex₂ CategoryTheory.Functor category mapBifunctorHomologicalComplex	—	—
mapBifunctorHomologicalComplex_obj_obj_X_d 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.d HomologicalComplex.X HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms obj HomologicalComplex₂ CategoryTheory.Functor category mapBifunctorHomologicalComplex map	—	—
mapBifunctorHomologicalComplex_obj_obj_d_f 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex.Hom.f obj CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.Functor category CategoryTheory.GradedObject.mapBifunctor HomologicalComplex.X map HomologicalComplex.d HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂ mapBifunctorHomologicalComplex CategoryTheory.NatTrans.app	—	—
mapBifunctorHomologicalComplex_obj_obj_toGradedObject 📖	mathematical	PreservesZeroMorphisms obj CategoryTheory.Functor category	HomologicalComplex₂.toGradedObject obj HomologicalComplex HomologicalComplex.instCategory HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms CategoryTheory.Functor category mapBifunctorHomologicalComplex CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.GradedObject.mapBifunctor HomologicalComplex.X	—	—
map₂HomologicalComplex_map_app 📖	mathematical	PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms obj CategoryTheory.Functor category HomologicalComplex.HasMapBifunctor	CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor HomologicalComplex.mapBifunctorMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct map CategoryTheory.Functor category map₂HomologicalComplex	—	—
map₂HomologicalComplex_obj_map 📖	mathematical	PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms obj CategoryTheory.Functor category HomologicalComplex.HasMapBifunctor	map HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms obj CategoryTheory.Functor category map₂HomologicalComplex HomologicalComplex.mapBifunctorMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
map₂HomologicalComplex_obj_obj 📖	mathematical	PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms obj CategoryTheory.Functor category HomologicalComplex.HasMapBifunctor	obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor category map₂HomologicalComplex HomologicalComplex.mapBifunctor	—	—

HomologicalComplex

Definitions

Name	Category	Theorems
HasMapBifunctor 📖	MathDef	2 math math: hasMapBifunctor_flip_iff, instHasMapBifunctorFlip
mapBifunctor 📖	CompOp	86 math math: mapBifunctor.ι_D₂, mapBifunctor₁₂.ι_D₃_assoc, mapBifunctor₁₂.d_eq, mapBifunctor.ι_D₂_assoc, mapBifunctor.ι_D₁_assoc, mapBifunctor₂₃.ι_D₃, mapBifunctor₂₃.d₂_eq, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, mapBifunctor₂₃.d₃_eq, ι_mapBifunctorAssociatorX_hom, mapBifunctor₁₂.ι_D₁_assoc, mapBifunctorMapHomotopy.comm₁, mapBifunctorFlipIso_hom_naturality_assoc, mapBifunctor₁₂.hom_ext_iff, mapBifunctor₂₃.ι_mapBifunctor₂₃Desc, mapBifunctor₁₂.ι_mapBifunctor₁₂Desc, mapBifunctor₁₂.ι_D₂_assoc, mapBifunctor₂₃.ιOrZero_eq_zero, mapBifunctor.hom_ext_iff, ι_mapBifunctorDesc, mapBifunctorAssociatorX_hom_D₂, mapBifunctorMapHomotopy.zero₁, mapBifunctor₂₃.d₃_eq_zero, mapBifunctor₁₂.d₂_eq_zero, mapBifunctor₁₂.ιOrZero_eq_zero, mapBifunctor₂₃.ι_D₁, mapBifunctor₂₃.ι_mapBifunctor₂₃Desc_assoc, mapBifunctorAssociatorX_hom_D₃_assoc, mapBifunctor.d₂_eq, ι_mapBifunctorFlipIso_inv_assoc, mapBifunctor.d₁_eq_zero, mapBifunctor₂₃.ι_D₂, CategoryTheory.Functor.map₂HomologicalComplex_map_app, mapBifunctorFlipIso_hom_naturality, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, mapBifunctor₁₂.ι_D₁, ι_mapBifunctorAssociatorX_hom_assoc, ιOrZero_mapBifunctorAssociatorX_hom, tensor_unit_d₂, mapBifunctorAssociatorX_hom_D₂_assoc, mapBifunctor.d_eq, mapBifunctor₂₃.d₁_eq, ι_mapBifunctorMap_assoc, ιMapBifunctorOrZero_eq_zero, mapBifunctor₂₃.ι_eq, CategoryTheory.Functor.map₂HomologicalComplex_obj_obj, mapBifunctor₁₂.ι_D₃, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, mapBifunctorAssociatorX_hom_D₁, mapBifunctor₂₃.ι_D₁_assoc, ι_mapBifunctorDesc_assoc, mapBifunctorFlipIso_flip, mapBifunctor₁₂.d₃_eq_zero, mapBifunctorMapHomotopy.comm₁_aux, mapBifunctor.ι_D₁, mapBifunctor.d₁_eq', mapBifunctor.d₂_eq_zero, mapBifunctor₂₃.d_eq, mapBifunctorAssociatorX_hom_D₃, ι_mapBifunctorFlipIso_hom, mapBifunctor₁₂.d₁_eq_zero, mapBifunctor.d₂_eq_zero', mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, mapBifunctor.d₂_eq', mapBifunctor.d₁_eq_zero', unit_tensor_d₁, mapBifunctor₂₃.ι_D₃_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, mapBifunctor₁₂.ι_eq, mapBifunctor₁₂.d₁_eq, mapBifunctor₁₂.d₃_eq, mapBifunctor₁₂.ι_D₂, mapBifunctor₁₂.ι_mapBifunctor₁₂Desc_assoc, mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, mapBifunctor₁₂.d₂_eq, mapBifunctor₂₃.d₁_eq_zero, ι_mapBifunctorFlipIso_hom_assoc, mapBifunctorAssociatorX_hom_D₁_assoc, mapBifunctor.d₁_eq, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, ι_mapBifunctorMap, mapBifunctor₂₃.d₂_eq_zero, ιOrZero_mapBifunctorAssociatorX_hom_assoc, ι_mapBifunctorFlipIso_inv, mapBifunctor₂₃.ι_D₂_assoc
mapBifunctorDesc 📖	CompOp	2 math math: ι_mapBifunctorDesc, ι_mapBifunctorDesc_assoc
mapBifunctorMap 📖	CompOp	11 math math: CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, mapBifunctorMapHomotopy.comm₁, mapBifunctorFlipIso_hom_naturality_assoc, CategoryTheory.Functor.map₂HomologicalComplex_map_app, mapBifunctorFlipIso_hom_naturality, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, ι_mapBifunctorMap_assoc, CategoryTheory.Functor.map₂HomologicalComplex_obj_map, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, ι_mapBifunctorMap
ιMapBifunctor 📖	CompOp	22 math math: mapBifunctor.ι_D₂, mapBifunctor.ι_D₂_assoc, mapBifunctor.ι_D₁_assoc, mapBifunctor.hom_ext_iff, ι_mapBifunctorDesc, mapBifunctor.d₂_eq, ι_mapBifunctorFlipIso_inv_assoc, ι_mapBifunctorMap_assoc, mapBifunctor₂₃.ι_eq, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, ι_mapBifunctorDesc_assoc, ιMapBifunctorOrZero_eq, mapBifunctor.ι_D₁, ι_mapBifunctorFlipIso_hom, mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, mapBifunctor₁₂.ι_eq, mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, ι_mapBifunctorFlipIso_hom_assoc, mapBifunctor.d₁_eq, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, ι_mapBifunctorMap, ι_mapBifunctorFlipIso_inv
ιMapBifunctorOrZero 📖	CompOp	8 math math: ιMapBifunctorOrZero_eq_zero, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, ιMapBifunctorOrZero_eq, mapBifunctor.d₁_eq', mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, mapBifunctor.d₂_eq', mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ιMapBifunctorOrZero_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor ComplexShape.π	ιMapBifunctorOrZero ιMapBifunctor	—	—
ιMapBifunctorOrZero_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor	ιMapBifunctorOrZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mapBifunctor CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ι_mapBifunctorDesc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mapBifunctor ιMapBifunctor mapBifunctorDesc	—	HomologicalComplex₂.ι_totalDesc
ι_mapBifunctorDesc_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mapBifunctor ιMapBifunctor mapBifunctorDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorDesc
ι_mapBifunctorMap 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mapBifunctor ιMapBifunctor Hom.f mapBifunctorMap CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	HomologicalComplex₂.ιTotal_map CategoryTheory.Category.assoc
ι_mapBifunctorMap_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HasMapBifunctor ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms mapBifunctor ιMapBifunctor Hom.f mapBifunctorMap CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorMap

HomologicalComplex.mapBifunctor

Definitions

Name	Category	Theorems
D₁ 📖	CompOp	3 math math: ι_D₁_assoc, d_eq, ι_D₁
D₂ 📖	CompOp	3 math math: ι_D₂, ι_D₂_assoc, d_eq
d₁ 📖	CompOp	7 math math: ι_D₁_assoc, d₁_eq_zero, ι_D₁, d₁_eq', d₁_eq_zero', HomologicalComplex.unit_tensor_d₁, d₁_eq
d₂ 📖	CompOp	7 math math: ι_D₂, ι_D₂_assoc, d₂_eq, HomologicalComplex.tensor_unit_d₂, d₂_eq_zero, d₂_eq_zero', d₂_eq'

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.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup D₁ D₂	—	—
d₁_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel ComplexShape.π	d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.d HomologicalComplex.ιMapBifunctor	—	HomologicalComplex₂.d₁_eq
d₁_eq' 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel	d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp CategoryTheory.NatTrans.app CategoryTheory.Functor.map HomologicalComplex.d HomologicalComplex.ιMapBifunctorOrZero	—	HomologicalComplex₂.d₁_eq'
d₁_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel ComplexShape.next	d₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex₂.d₁_eq_zero
d₁_eq_zero' 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel	d₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex₂.d₁_eq_zero'
d₂_eq 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel ComplexShape.π	d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map HomologicalComplex.d HomologicalComplex.ιMapBifunctor	—	HomologicalComplex₂.d₂_eq
d₂_eq' 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel	d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.map HomologicalComplex.d HomologicalComplex.ιMapBifunctorOrZero	—	HomologicalComplex₂.d₂_eq'
d₂_eq_zero 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel ComplexShape.next	d₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex₂.d₂_eq_zero
d₂_eq_zero' 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.Rel	d₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex₂.d₂_eq_zero'
hom_ext 📖	—	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor	—	—	HomologicalComplex₂.total.hom_ext
hom_ext_iff 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor	—	hom_ext
ι_D₁ 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor D₁ d₁	—	HomologicalComplex₂.ι_D₁
ι_D₁_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor D₁ d₁	—	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 ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor D₂ d₂	—	HomologicalComplex₂.ι_D₂
ι_D₂_assoc 📖	mathematical	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.HasMapBifunctor ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.mapBifunctor HomologicalComplex.ιMapBifunctor D₂ d₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₂

---

← Back to Index