TotalComplex

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

Statistics

Metric	Count
Definitions D₁, D₂, HasTotal, d₁, d₂, total, map, mapIso, totalDesc, totalFunctor, ιTotal, ιTotalOrZero	12
Theorems D₁_D₁, D₁_D₁_assoc, D₁_D₂, D₁_D₂_assoc, D₁_shape, D₂_D₁, D₂_D₁_assoc, D₂_D₂, D₂_D₂_assoc, D₂_shape, XXIsoOfEq_hom_ιTotal, XXIsoOfEq_hom_ιTotal_assoc, XXIsoOfEq_inv_ιTotal, XXIsoOfEq_inv_ιTotal_assoc, d₁_eq, d₁_eq', d₁_eq_zero, d₁_eq_zero', d₂_eq, d₂_eq', d₂_eq_zero, d₂_eq_zero', hasTotal_of_iso, forget_map, hom_ext, hom_ext_iff, d₁_mapMap, d₁_mapMap_assoc, d₂_mapMap, d₂_mapMap_assoc, mapMap_D₁, mapMap_D₁_assoc, mapMap_D₂, mapMap_D₂_assoc, mapIso_hom, mapIso_inv, map_comp, map_comp_assoc, map_id, d₁_eq, d₁_eq', d₂_eq, d₂_eq', ιMapObj_D₁, ιMapObj_D₁_assoc, ιMapObj_D₂, ιMapObj_D₂_assoc, totalFunctor_map, totalFunctor_obj, total_d, ιTotalOrZero_eq, ιTotalOrZero_eq_zero, ιTotalOrZero_map, ιTotalOrZero_map_assoc, ιTotal_map, ιTotal_map_assoc, ι_D₁, ι_D₁_assoc, ι_D₂, ι_D₂_assoc, ι_totalDesc, ι_totalDesc_assoc	62
Total	74

HomologicalComplex₂

Definitions

Name	Category	Theorems
D₁ 📖	CompOp	26 math math: totalAux.ιMapObj_D₁, totalFlipIso_hom_f_D₁, D₁_D₁_assoc, total.mapAux.mapMap_D₁_assoc, D₁_D₁, D₂_D₁_assoc, ι_D₁_assoc, D₁_shape, totalFlipIsoX_hom_D₂_assoc, D₁_totalShift₂XIso_hom_assoc, D₁_totalShift₁XIso_hom_assoc, total.mapAux.mapMap_D₁, totalFlipIso_hom_f_D₂, D₁_totalShift₁XIso_hom, totalFlipIso_hom_f_D₁_assoc, totalFlipIsoX_hom_D₁, D₂_D₁, D₁_D₂_assoc, ι_D₁, total_d, totalFlipIsoX_hom_D₂, D₁_totalShift₂XIso_hom, totalAux.ιMapObj_D₁_assoc, D₁_D₂, totalFlipIsoX_hom_D₁_assoc, totalFlipIso_hom_f_D₂_assoc
D₂ 📖	CompOp	26 math math: totalFlipIso_hom_f_D₁, D₂_totalShift₁XIso_hom_assoc, D₂_totalShift₂XIso_hom_assoc, D₂_D₁_assoc, D₂_D₂, ι_D₂, totalAux.ιMapObj_D₂_assoc, totalFlipIsoX_hom_D₂_assoc, ι_D₂_assoc, total.mapAux.mapMap_D₂, totalAux.ιMapObj_D₂, D₂_shape, total.mapAux.mapMap_D₂_assoc, totalFlipIso_hom_f_D₂, D₂_totalShift₁XIso_hom, totalFlipIso_hom_f_D₁_assoc, totalFlipIsoX_hom_D₁, D₂_D₂_assoc, D₂_D₁, D₁_D₂_assoc, total_d, totalFlipIsoX_hom_D₂, D₂_totalShift₂XIso_hom, D₁_D₂, totalFlipIsoX_hom_D₁_assoc, totalFlipIso_hom_f_D₂_assoc
HasTotal 📖	MathDef	1 math math: flip_hasTotal_iff
d₁ 📖	CompOp	12 math math: totalAux.ιMapObj_D₁, d₁_eq_zero', ι_D₁_assoc, total.mapAux.d₁_mapMap, d₁_eq, totalAux.d₁_eq, d₁_eq_zero, ι_D₁, total.mapAux.d₁_mapMap_assoc, d₁_eq', totalAux.ιMapObj_D₁_assoc, totalAux.d₁_eq'
d₂ 📖	CompOp	13 math math: totalAux.d₂_eq, d₂_eq_zero, ι_D₂, totalAux.ιMapObj_D₂_assoc, ι_D₂_assoc, totalAux.d₂_eq', total.mapAux.d₂_mapMap_assoc, d₂_eq_zero', totalAux.ιMapObj_D₂, d₂_eq, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, total.mapAux.d₂_mapMap, d₂_eq'
total 📖	CompOp	64 math math: totalFlipIso_hom_f_D₁, totalShift₂Iso_hom_naturality_assoc, total.mapIso_hom, D₂_totalShift₁XIso_hom_assoc, D₂_totalShift₂XIso_hom_assoc, ιTotalOrZero_map_assoc, ιTotal_map, ι_totalShift₁Iso_hom_f_assoc, ι_D₁_assoc, ιTotal_totalFlipIso_f_inv_assoc, ι_totalShift₁Iso_inv_f, ι_totalDesc_assoc, ι_totalShift₂Iso_inv_f_assoc, ι_D₂, d₁_eq, XXIsoOfEq_hom_ιTotal_assoc, totalFlipIsoX_hom_D₂_assoc, ι_D₂_assoc, totalFunctor_obj, totalShift₁Iso_hom_totalShift₂Iso_hom, D₁_totalShift₂XIso_hom_assoc, ι_totalDesc, D₁_totalShift₁XIso_hom_assoc, ι_totalShift₁Iso_inv_f_assoc, ιTotal_totalFlipIso_f_hom_assoc, XXIsoOfEq_inv_ιTotal_assoc, total.mapIso_inv, ι_totalShift₂Iso_hom_f_assoc, totalFlipIso_hom_f_D₂, D₁_totalShift₁XIso_hom, D₂_totalShift₁XIso_hom, totalFlipIso_hom_f_D₁_assoc, XXIsoOfEq_inv_ιTotal, total.map_comp, totalFlipIsoX_hom_D₁, ιTotalOrZero_map, totalShift₁Iso_trans_totalShift₂Iso, d₂_eq, flip_totalFlipIso, total.map_comp_assoc, ι_totalShift₂Iso_inv_f, totalShift₂Iso_hom_naturality, ιTotal_totalFlipIso_f_hom, totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, totalShift₁Iso_hom_naturality_assoc, ι_D₁, ι_totalShift₂Iso_hom_f, total_d, XXIsoOfEq_hom_ιTotal, totalShift₁Iso_hom_naturality, d₂_eq', totalFlipIsoX_hom_D₂, d₁_eq', ιTotalOrZero_eq_zero, D₁_totalShift₂XIso_hom, D₂_totalShift₂XIso_hom, total.hom_ext_iff, totalFlipIsoX_hom_D₁_assoc, total.map_id, total.forget_map, ιTotal_map_assoc, totalFlipIso_hom_f_D₂_assoc, ι_totalShift₁Iso_hom_f, ιTotal_totalFlipIso_f_inv
totalDesc 📖	CompOp	2 math math: ι_totalDesc_assoc, ι_totalDesc
totalFunctor 📖	CompOp	2 math math: totalFunctor_obj, totalFunctor_map
ιTotal 📖	CompOp	28 math math: ιTotal_map, ι_totalShift₁Iso_hom_f_assoc, ι_D₁_assoc, ιTotal_totalFlipIso_f_inv_assoc, ι_totalShift₁Iso_inv_f, ι_totalDesc_assoc, ι_totalShift₂Iso_inv_f_assoc, ι_D₂, d₁_eq, XXIsoOfEq_hom_ιTotal_assoc, ι_D₂_assoc, ι_totalDesc, ι_totalShift₁Iso_inv_f_assoc, ιTotal_totalFlipIso_f_hom_assoc, XXIsoOfEq_inv_ιTotal_assoc, ι_totalShift₂Iso_hom_f_assoc, XXIsoOfEq_inv_ιTotal, d₂_eq, ι_totalShift₂Iso_inv_f, ιTotalOrZero_eq, ιTotal_totalFlipIso_f_hom, ι_D₁, ι_totalShift₂Iso_hom_f, XXIsoOfEq_hom_ιTotal, total.hom_ext_iff, ιTotal_map_assoc, ι_totalShift₁Iso_hom_f, ιTotal_totalFlipIso_f_inv
ιTotalOrZero 📖	CompOp	6 math math: ιTotalOrZero_map_assoc, ιTotalOrZero_map, ιTotalOrZero_eq, d₂_eq', d₁_eq', ιTotalOrZero_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
D₁_D₁ 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.GradedObject.mapObj_ext totalAux.ιMapObj_D₁_assoc CategoryTheory.Limits.comp_zero ComplexShape.next_π₁ ComplexShape.next_eq' totalAux.d₁_eq CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc totalAux.ιMapObj_D₁ CategoryTheory.Linear.comp_units_smul d_f_comp_d_f_assoc CategoryTheory.Limits.zero_comp smul_zero d₁_eq_zero D₁_shape
D₁_D₁_assoc 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₁_D₁
D₁_D₂ 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₁ D₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	D₂_D₁ neg_neg
D₁_D₂_assoc 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₁ D₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₁_D₂
D₁_shape 📖	mathematical	HasTotal ComplexShape.Rel	D₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.GradedObject.mapObj_ext totalAux.ιMapObj_D₁ CategoryTheory.Limits.comp_zero d₁_eq_zero' ComplexShape.rel_π₁ d₁_eq_zero
D₂_D₁ 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₂ D₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	CategoryTheory.GradedObject.mapObj_ext totalAux.ιMapObj_D₂_assoc CategoryTheory.Preadditive.comp_neg totalAux.ιMapObj_D₁_assoc ComplexShape.next_π₁ ComplexShape.next_eq' totalAux.d₁_eq CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc totalAux.ιMapObj_D₂ ComplexShape.next_π₂ totalAux.d₂_eq totalAux.ιMapObj_D₁ CategoryTheory.Linear.comp_units_smul smul_smul ComplexShape.ε₂_ε₁ neg_mul Units.neg_smul HomologicalComplex.Hom.comm_assoc d₂_eq_zero CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero smul_zero neg_zero d₁_eq_zero D₁_shape D₂_shape
D₂_D₁_assoc 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₂ D₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₂_D₁
D₂_D₂ 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.GradedObject.mapObj_ext totalAux.ιMapObj_D₂_assoc CategoryTheory.Limits.comp_zero ComplexShape.next_π₂ ComplexShape.next_eq' totalAux.d₂_eq CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc totalAux.ιMapObj_D₂ CategoryTheory.Linear.comp_units_smul HomologicalComplex.d_comp_d_assoc CategoryTheory.Limits.zero_comp smul_zero d₂_eq_zero D₂_shape
D₂_D₂_assoc 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π D₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' D₂_D₂
D₂_shape 📖	mathematical	HasTotal ComplexShape.Rel	D₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.GradedObject.mapObj_ext totalAux.ιMapObj_D₂ CategoryTheory.Limits.comp_zero d₂_eq_zero' ComplexShape.rel_π₂ d₂_eq_zero
XXIsoOfEq_hom_ιTotal 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total CategoryTheory.Iso.hom XXIsoOfEq ιTotal	—	CategoryTheory.Category.id_comp
XXIsoOfEq_hom_ιTotal_assoc 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Iso.hom XXIsoOfEq total ιTotal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XXIsoOfEq_hom_ιTotal
XXIsoOfEq_inv_ιTotal 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total CategoryTheory.Iso.inv XXIsoOfEq ιTotal	—	CategoryTheory.Category.id_comp
XXIsoOfEq_inv_ιTotal_assoc 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.Iso.inv XXIsoOfEq total ιTotal	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XXIsoOfEq_inv_ιTotal
d₁_eq 📖	mathematical	HasTotal ComplexShape.Rel ComplexShape.π	d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f HomologicalComplex.d ιTotal	—	totalAux.d₁_eq
d₁_eq' 📖	mathematical	HasTotal ComplexShape.Rel	d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f HomologicalComplex.d ιTotalOrZero	—	totalAux.d₁_eq'
d₁_eq_zero 📖	mathematical	HasTotal ComplexShape.Rel ComplexShape.next	d₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj toGradedObject ComplexShape.π CategoryTheory.Limits.HasZeroMorphisms.zero	—	shape_f CategoryTheory.Limits.zero_comp smul_zero
d₁_eq_zero' 📖	mathematical	HasTotal ComplexShape.Rel	d₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj toGradedObject ComplexShape.π CategoryTheory.Limits.HasZeroMorphisms.zero	—	totalAux.d₁_eq' CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero CategoryTheory.Limits.comp_zero smul_zero
d₂_eq 📖	mathematical	HasTotal ComplexShape.Rel ComplexShape.π	d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.CategoryStruct.comp HomologicalComplex.d ιTotal	—	totalAux.d₂_eq
d₂_eq' 📖	mathematical	HasTotal ComplexShape.Rel	d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.CategoryStruct.comp HomologicalComplex.d ιTotalOrZero	—	totalAux.d₂_eq'
d₂_eq_zero 📖	mathematical	HasTotal ComplexShape.Rel ComplexShape.next	d₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj toGradedObject ComplexShape.π CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologicalComplex.shape CategoryTheory.Limits.zero_comp smul_zero
d₂_eq_zero' 📖	mathematical	HasTotal ComplexShape.Rel	d₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj toGradedObject ComplexShape.π CategoryTheory.Limits.HasZeroMorphisms.zero	—	totalAux.d₂_eq' CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero CategoryTheory.Limits.comp_zero smul_zero
hasTotal_of_iso 📖	—	HasTotal	—	—	CategoryTheory.GradedObject.hasMap_of_iso
totalFunctor_map 📖	mathematical	HasTotal	CategoryTheory.Functor.map HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms totalFunctor total.map	—	—
totalFunctor_obj 📖	mathematical	HasTotal	CategoryTheory.Functor.obj HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms totalFunctor total	—	—
total_d 📖	mathematical	HasTotal	HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms total Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj toGradedObject ComplexShape.π AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup D₁ D₂	—	—
ιTotalOrZero_eq 📖	mathematical	HasTotal ComplexShape.π	ιTotalOrZero ιTotal	—	—
ιTotalOrZero_eq_zero 📖	mathematical	HasTotal	ιTotalOrZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
ιTotalOrZero_map 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotalOrZero HomologicalComplex.Hom.f total.map	—	CategoryTheory.GradedObject.ιMapObjOrZero_mapMap
ιTotalOrZero_map_assoc 📖	mathematical	HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotalOrZero HomologicalComplex.Hom.f total.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTotalOrZero_map
ιTotal_map 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal HomologicalComplex.Hom.f total.map	—	CategoryTheory.GradedObject.ι_mapMap
ιTotal_map_assoc 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal HomologicalComplex.Hom.f total.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTotal_map
ι_D₁ 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total CategoryTheory.GradedObject.mapObj toGradedObject ιTotal D₁ d₁	—	totalAux.ιMapObj_D₁
ι_D₁_assoc 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal CategoryTheory.GradedObject.mapObj toGradedObject D₁ d₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₁
ι_D₂ 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total CategoryTheory.GradedObject.mapObj toGradedObject ιTotal D₂ d₂	—	totalAux.ιMapObj_D₂
ι_D₂_assoc 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal CategoryTheory.GradedObject.mapObj toGradedObject D₂ d₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_D₂
ι_totalDesc 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal totalDesc	—	CategoryTheory.GradedObject.ι_descMapObj
ι_totalDesc_assoc 📖	mathematical	HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms total ιTotal totalDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_totalDesc

HomologicalComplex₂.total

Definitions

Name	Category	Theorems
map 📖	CompOp	17 math math: HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, mapIso_hom, HomologicalComplex₂.ιTotalOrZero_map_assoc, HomologicalComplex₂.ιTotal_map, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, mapIso_inv, map_comp, HomologicalComplex₂.ιTotalOrZero_map, map_comp_assoc, HomologicalComplex₂.totalShift₂Iso_hom_naturality, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, HomologicalComplex₂.totalShift₁Iso_hom_naturality, map_id, forget_map, HomologicalComplex₂.totalFunctor_map, HomologicalComplex₂.ιTotal_map_assoc
mapIso 📖	CompOp	3 math math: mapIso_hom, mapIso_inv, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_map 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects HomologicalComplex.forget HomologicalComplex₂.total map CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObject HomologicalComplex₂.toGradedObjectMap ComplexShape.π	—	—
hom_ext 📖	—	HomologicalComplex₂.HasTotal CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂.total HomologicalComplex₂.ιTotal	—	—	CategoryTheory.GradedObject.mapObj_ext
hom_ext_iff 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂.total HomologicalComplex₂.ιTotal	—	hom_ext
mapIso_hom 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.Iso.hom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex₂.total mapIso map HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms	—	—
mapIso_inv 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.Iso.inv HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomologicalComplex₂.total mapIso map HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms	—	—
map_comp 📖	mathematical	HomologicalComplex₂.HasTotal	map CategoryTheory.CategoryStruct.comp HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂.total	—	CategoryTheory.Functor.map_injective HomologicalComplex.instFaithfulGradedObjectForget CategoryTheory.GradedObject.mapMap_comp
map_comp_assoc 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex₂.total map HomologicalComplex₂ HomologicalComplex.instHasZeroMorphisms	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	HomologicalComplex₂.HasTotal	map CategoryTheory.CategoryStruct.id HomologicalComplex₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory HomologicalComplex HomologicalComplex.instHasZeroMorphisms HomologicalComplex₂.total	—	CategoryTheory.Functor.map_injective HomologicalComplex.instFaithfulGradedObjectForget CategoryTheory.GradedObject.mapMap_id

HomologicalComplex₂.total.mapAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d₁_mapMap 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject ComplexShape.π HomologicalComplex₂.d₁ CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex.Hom.f	—	HomologicalComplex₂.totalAux.d₁_eq' CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc CategoryTheory.GradedObject.ιMapObjOrZero_mapMap CategoryTheory.Linear.comp_units_smul HomologicalComplex₂.comm_f_assoc HomologicalComplex₂.d₁_eq_zero CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
d₁_mapMap_assoc 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject ComplexShape.π HomologicalComplex₂.d₁ CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex.Hom.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₁_mapMap
d₂_mapMap 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject ComplexShape.π HomologicalComplex₂.d₂ CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex.Hom.f	—	HomologicalComplex₂.totalAux.d₂_eq' CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.assoc CategoryTheory.GradedObject.ιMapObjOrZero_mapMap CategoryTheory.Linear.comp_units_smul HomologicalComplex.Hom.comm_assoc HomologicalComplex₂.d₂_eq_zero CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
d₂_mapMap_assoc 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject ComplexShape.π HomologicalComplex₂.d₂ CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex.Hom.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₂_mapMap
mapMap_D₁ 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex₂.D₁	—	CategoryTheory.GradedObject.mapObj_ext CategoryTheory.GradedObject.ι_mapMap_assoc HomologicalComplex₂.totalAux.ιMapObj_D₁ HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc d₁_mapMap
mapMap_D₁_assoc 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex₂.D₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMap_D₁
mapMap_D₂ 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex₂.D₂	—	CategoryTheory.GradedObject.mapObj_ext CategoryTheory.GradedObject.ι_mapMap_assoc HomologicalComplex₂.totalAux.ιMapObj_D₂ HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc d₂_mapMap
mapMap_D₂_assoc 📖	mathematical	HomologicalComplex₂.HasTotal	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.π CategoryTheory.GradedObject.mapMap HomologicalComplex₂.toGradedObjectMap HomologicalComplex₂.D₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapMap_D₂

HomologicalComplex₂.totalAux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d₁_eq 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.Rel ComplexShape.π	HomologicalComplex₂.d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f HomologicalComplex.d CategoryTheory.GradedObject.ιMapObj	—	d₁_eq' CategoryTheory.GradedObject.ιMapObjOrZero_eq
d₁_eq' 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.Rel	HomologicalComplex₂.d₁ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject ComplexShape.π Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₁ CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f HomologicalComplex.d CategoryTheory.GradedObject.ιMapObjOrZero	—	ComplexShape.next_eq'
d₂_eq 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.Rel ComplexShape.π	HomologicalComplex₂.d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.CategoryStruct.comp HomologicalComplex.d CategoryTheory.GradedObject.ιMapObj	—	d₂_eq' CategoryTheory.GradedObject.ιMapObjOrZero_eq
d₂_eq' 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.Rel	HomologicalComplex₂.d₂ Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms CategoryTheory.GradedObject.mapObj HomologicalComplex₂.toGradedObject ComplexShape.π Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup ComplexShape.ε₂ CategoryTheory.CategoryStruct.comp HomologicalComplex.d CategoryTheory.GradedObject.ιMapObjOrZero	—	ComplexShape.next_eq'
ιMapObj_D₁ 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.GradedObject.mapObj CategoryTheory.GradedObject.ιMapObj HomologicalComplex₂.D₁ HomologicalComplex₂.d₁	—	CategoryTheory.GradedObject.ι_descMapObj
ιMapObj_D₁_assoc 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.GradedObject.mapObj CategoryTheory.GradedObject.ιMapObj HomologicalComplex₂.D₁ HomologicalComplex₂.d₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapObj_D₁
ιMapObj_D₂ 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.GradedObject.mapObj CategoryTheory.GradedObject.ιMapObj HomologicalComplex₂.D₂ HomologicalComplex₂.d₂	—	CategoryTheory.GradedObject.ι_descMapObj
ιMapObj_D₂_assoc 📖	mathematical	HomologicalComplex₂.HasTotal ComplexShape.π	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex₂.toGradedObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.GradedObject.mapObj CategoryTheory.GradedObject.ιMapObj HomologicalComplex₂.D₂ HomologicalComplex₂.d₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapObj_D₂

---

← Back to Index